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

This PR adds a couple useful lemmas regarding `field_range`. Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
leanprover-community · May 8, 2023 · d4437c6 · d4437c6
1 parent c596622
commit d4437c6
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 0 deletions.
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