From 17ab30b2f1d096e41d84dc9b522c6f14be5f7743 Mon Sep 17 00:00:00 2001
From: tb65536 <tb65536@uw.edu>
Date: Tue, 30 Aug 2022 00:38:43 +0000
Subject: [PATCH] feat(field_theory/normal): Define the normal closure (#16144)

This PR adds the definition of the normal closure, and proves that the normal closure is finite-dimensional and normal.
---
 src/field_theory/normal.lean | 63 ++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/src/field_theory/normal.lean b/src/field_theory/normal.lean
index 297b7620d247f..5e104283fa2ec 100644
--- a/src/field_theory/normal.lean
+++ b/src/field_theory/normal.lean
@@ -219,6 +219,12 @@ begin
   exact polynomial.splits_comp_of_splits _ (inclusion hE).to_ring_hom this,
 end
 
+variables {F K} {L : Type*} [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L]
+
+@[simp] lemma restrict_scalars_normal {E : intermediate_field K L} :
+  normal F (E.restrict_scalars F) ↔ normal F E :=
+iff.rfl
+
 end intermediate_field
 
 variables {F} {K} {K₁ K₂ K₃:Type*} [field K₁] [field K₂] [field K₃]
@@ -375,3 +381,60 @@ begin
 end
 
 end lift
+
+section normal_closure
+
+open intermediate_field
+
+variables (F K) (L : Type*) [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L]
+
+/-- The normal closure of `K` in `L`. -/
+noncomputable! def normal_closure : intermediate_field K L :=
+{ algebra_map_mem' := λ r, le_supr (λ f : K →ₐ[F] L, f.field_range)
+    (is_scalar_tower.to_alg_hom F K L) ⟨r, rfl⟩,
+  .. (⨆ f : K →ₐ[F] L, f.field_range).to_subfield }
+
+namespace normal_closure
+
+lemma restrict_scalars_eq_supr_adjoin [h : normal F L] :
+  (normal_closure F K L).restrict_scalars F = ⨆ x : K, adjoin F ((minpoly F x).root_set L) :=
+begin
+  refine le_antisymm (supr_le _) (supr_le (λ x, adjoin_le_iff.mpr (λ y hy, _))),
+  { rintros f _ ⟨x, rfl⟩,
+    refine le_supr (λ x, adjoin F ((minpoly F x).root_set L)) x
+      (subset_adjoin F ((minpoly F x).root_set L) _),
+    rw [polynomial.mem_root_set, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
+        polynomial.aeval_alg_hom_apply, minpoly.aeval, map_zero],
+    exact minpoly.ne_zero ((is_integral_algebra_map_iff (algebra_map K L).injective).mp
+      (h.is_integral (algebra_map K L x))) },
+  { rw [polynomial.root_set, finset.mem_coe, multiset.mem_to_finset] at hy,
+    let g := (alg_hom_adjoin_integral_equiv F ((is_integral_algebra_map_iff
+      (algebra_map K L).injective).mp (h.is_integral (algebra_map K L x)))).symm ⟨y, hy⟩,
+    refine le_supr (λ f : K →ₐ[F] L, f.field_range)
+      ((g.lift_normal L).comp (is_scalar_tower.to_alg_hom F K L))
+      ⟨x, (g.lift_normal_commutes L (adjoin_simple.gen F x)).trans _⟩,
+    rw [algebra.id.map_eq_id, ring_hom.id_apply],
+    apply power_basis.lift_gen },
+end
+
+instance normal [h : normal F L] : normal F (normal_closure F K L) :=
+let ϕ := algebra_map K L in begin
+  rw [←intermediate_field.restrict_scalars_normal, restrict_scalars_eq_supr_adjoin],
+  apply intermediate_field.normal_supr F L _,
+  intro x,
+  apply normal.of_is_splitting_field (minpoly F x),
+  exact adjoin_root_set_is_splitting_field ((minpoly.eq_of_algebra_map_eq ϕ.injective
+    ((is_integral_algebra_map_iff ϕ.injective).mp (h.is_integral (ϕ x))) rfl).symm ▸ h.splits _),
+end
+
+instance is_finite_dimensional [finite_dimensional F K] :
+  finite_dimensional F (normal_closure F K L) :=
+begin
+  haveI : ∀ f : K →ₐ[F] L, finite_dimensional F f.field_range :=
+  λ f, f.to_linear_map.finite_dimensional_range,
+  apply intermediate_field.finite_dimensional_supr_of_finite,
+end
+
+end normal_closure
+
+end normal_closure