feat(field_theory/adjoin,normal): field_range lemmas (#18959)

tb65536 · tb65536 · commit d4437c68c8d3 · 2023-05-08T17:26:31.000Z
This PR adds a couple useful lemmas regarding `field_range`.



Co-authored-by: Thomas Browning &lt;tb65536@users.noreply.github.com&gt;
diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean
@@ -198,6 +198,14 @@ lemma _root_.alg_hom.map_field_range {K L : Type*} [field K] [field L] [algebra
   (f : E →ₐ[F] K) (g : K →ₐ[F] L) : f.field_range.map g = (g.comp f).field_range :=
 set_like.ext' (set.range_comp g f).symm
 
+lemma _root_.alg_hom.field_range_eq_top {K : Type*} [field K] [algebra F K] {f : E →ₐ[F] K} :
+  f.field_range = ⊤ ↔ function.surjective f :=
+set_like.ext'_iff.trans set.range_iff_surjective
+
+@[simp] lemma _root_.alg_equiv.field_range_eq_top {K : Type*} [field K] [algebra F K]
+  (f : E ≃ₐ[F] K) : (f : E →ₐ[F] K).field_range = ⊤ :=
+alg_hom.field_range_eq_top.mpr f.surjective
+
 end lattice
 
 section adjoin_def
diff --git a/src/field_theory/normal.lean b/src/field_theory/normal.lean
@@ -278,6 +278,15 @@ lemma alg_hom.restrict_normal_comp [normal F E] :
 alg_hom.ext (λ _, (algebra_map E K₃).injective
   (by simp only [alg_hom.comp_apply, alg_hom.restrict_normal_commutes]))
 
+lemma alg_hom.field_range_of_normal {E : intermediate_field F K} [normal F E] (f : E →ₐ[F] K) :
+  f.field_range = E :=
+begin
+  haveI : is_scalar_tower F E E := by apply_instance,
+  let g := f.restrict_normal' E,
+  rw [←show E.val.comp ↑g = f, from fun_like.ext_iff.mpr (f.restrict_normal_commutes E),
+    ←alg_hom.map_field_range, g.field_range_eq_top, ←E.val.field_range_eq_map, E.field_range_val],
+end
+
 /-- Restrict algebra isomorphism to a normal subfield -/
 def alg_equiv.restrict_normal [h : normal F E] : E ≃ₐ[F] E :=
 alg_hom.restrict_normal' χ.to_alg_hom E
