refactor(FieldTheory/NormalClosure): change definition and add API (#6163)

This PR adds API and changes the definition of the normal closure of $F\leq K\leq L$ to be an intermediate field of L/F, rather than an intermediate field of L/K. For example, I think it would be more common to say that the normal closure of $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ is $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}$ rather than $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}(\sqrt[3]{2})$. This change also means that the normal closure goes from being a dependent function `(K : Type) → IntermediateField K L` to being a non-dependent function `Type → IntermediateField F L`, making it easier to compare across the Galois corespondence.

Supersedes leanprover-community/mathlib3#18971



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Author: tb65536

Mathlib/FieldTheory/IntermediateField.lean

@@ -423,6 +423,10 @@ theorem map_map {K L₁ L₂ L₃ : Type*} [Field K] [Field L₁] [Algebra K L
   SetLike.coe_injective <| Set.image_image _ _ _
 #align intermediate_field.map_map IntermediateField.map_map
 
+theorem map_mono (f : L →ₐ[K] L') {S T : IntermediateField K L} (h : S ≤ T) :
+    S.map f ≤ T.map f :=
+  SetLike.coe_mono (Set.image_subset f h)
+
 /-- Given an equivalence `e : L ≃ₐ[K] L'` of `K`-field extensions and an intermediate
 field `E` of `L/K`, `intermediate_field_equiv_map e E` is the induced equivalence
 between `E` and `E.map e` -/

Mathlib/FieldTheory/KrullTopology.lean

@@ -57,13 +57,6 @@ all intermediate fields `E` with `E/K` finite dimensional.
 
 open scoped Classical
 
-/-- Mapping intermediate fields along algebra equivalences preserves the partial order -/
-theorem IntermediateField.map_mono {K L M : Type*} [Field K] [Field L] [Field M] [Algebra K L]
-    [Algebra K M] {E1 E2 : IntermediateField K L} (e : L ≃ₐ[K] M) (h12 : E1 ≤ E2) :
-    E1.map e.toAlgHom ≤ E2.map e.toAlgHom :=
-  Set.image_subset e h12
-#align intermediate_field.map_mono IntermediateField.map_mono
-
 /-- Mapping intermediate fields along the identity does not change them -/
 theorem IntermediateField.map_id {K L : Type*} [Field K] [Field L] [Algebra K L]
     (E : IntermediateField K L) : E.map (AlgHom.id K L) = E :=

Mathlib/FieldTheory/NormalClosure.lean

@@ -5,6 +5,7 @@ Authors: Thomas Browning
 -/
 
 import Mathlib.FieldTheory.Normal
+import Mathlib.Order.Closure
 
 #align_import field_theory.normal from "leanprover-community/mathlib"@"9fb8964792b4237dac6200193a0d533f1b3f7423"
 /-!
@@ -22,16 +23,27 @@ variable (F K L : Type*) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F
   [IsScalarTower F K L]
 
 /-- The normal closure of `K` in `L`. -/
-noncomputable def normalClosure : IntermediateField K L :=
-  { (⨆ f : K →ₐ[F] L, f.fieldRange) with
-    algebraMap_mem' := fun r =>
-      le_iSup (fun f : K →ₐ[F] L => f.fieldRange) (IsScalarTower.toAlgHom F K L) ⟨r, rfl⟩ }
-#align normal_closure normalClosure
+noncomputable def normalClosure : IntermediateField F L :=
+  ⨆ f : K →ₐ[F] L, f.fieldRange
+
+lemma normalClosure_def : normalClosure F K L = ⨆ f : K →ₐ[F] L, f.fieldRange :=
+  rfl
+
+variable {F K L}
+
+lemma normalClosure_le_iff {K' : IntermediateField F L} :
+    normalClosure F K L ≤ K' ↔ ∀ f : K →ₐ[F] L, f.fieldRange ≤ K' :=
+  iSup_le_iff
+
+lemma AlgHom.fieldRange_le_normalClosure  (f : K →ₐ[F] L) : f.fieldRange ≤ normalClosure F K L :=
+  le_iSup AlgHom.fieldRange f
+
+variable (F K L)
 
 namespace normalClosure
 
 theorem restrictScalars_eq_iSup_adjoin [h : Normal F L] :
-    (normalClosure F K L).restrictScalars F = ⨆ x : K, adjoin F ((minpoly F x).rootSet L) := by
+    normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L) := by
   classical
   have hi : ∀ x : K, IsIntegral F x :=
     fun x ↦ (isIntegral_algebraMap_iff (algebraMap K L).injective).mp (h.isIntegral _)
@@ -71,12 +83,89 @@ instance is_finiteDimensional [FiniteDimensional F K] :
   haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f =>
     f.toLinearMap.finiteDimensional_range
   apply IntermediateField.finiteDimensional_iSup_of_finite
-#align normal_closure.is_finite_dimensional normalClosure.is_finiteDimensional
 
-instance isScalarTower : IsScalarTower F (normalClosure F K L) L :=
-  -- Porting note: the last argument here `(⨆ (f : K →ₐ[F] L), f.fieldRange).toSubalgebra`
-  -- was just written as `_` in mathlib3.
-  IsScalarTower.subalgebra' F L L (⨆ (f : K →ₐ[F] L), f.fieldRange).toSubalgebra
-#align normal_closure.is_scalar_tower normalClosure.isScalarTower
+noncomputable instance algebra : Algebra K (normalClosure F K L) :=
+  IntermediateField.algebra
+    { ⨆ f : K →ₐ[F] L, f.fieldRange with
+      algebraMap_mem' := fun r => (toAlgHom F K L).fieldRange_le_normalClosure ⟨r, rfl⟩ }
+
+instance : IsScalarTower F K (normalClosure F K L) := by
+  apply of_algebraMap_eq'
+  ext x
+  exact algebraMap_apply F K L x
+
+instance : IsScalarTower K (normalClosure F K L) L :=
+  of_algebraMap_eq' rfl
+
+lemma restrictScalars_eq :
+    (toAlgHom K (normalClosure F K L) L).fieldRange.restrictScalars F = normalClosure F K L :=
+  SetLike.ext' Subtype.range_val
 
 end normalClosure
+
+namespace IntermediateField
+
+variable {F L}
+variable (K K' : IntermediateField F L)
+
+lemma le_normalClosure : K ≤ normalClosure F K L :=
+K.fieldRange_val.symm.trans_le K.val.fieldRange_le_normalClosure
+
+lemma normalClosure_of_normal [Normal F K] : normalClosure F K L = K :=
+by simp only [normalClosure_def, AlgHom.fieldRange_of_normal, iSup_const]
+
+variable [Normal F L]
+
+lemma normalClosure_def' : normalClosure F K L = ⨆ f : L →ₐ[F] L, K.map f := by
+  refine' (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ _)) (iSup_le (fun f ↦ _)))
+  · exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)
+  · exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)
+
+lemma normalClosure_def'' : normalClosure F K L = ⨆ f : L ≃ₐ[F] L, K.map f := by
+  refine' (normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ _)) (iSup_le (fun f ↦ _)))
+  · exact le_iSup_of_le (f.restrictNormal' L)
+      (fun b ⟨a, h⟩ ↦ ⟨a, h.1, h.2 ▸ f.restrictNormal_commutes L a⟩)
+  · exact le_iSup_of_le f le_rfl
+
+lemma normalClosure_mono (h : K ≤ K') : normalClosure F K L ≤ normalClosure F K' L := by
+  rw [normalClosure_def', normalClosure_def']
+  exact iSup_mono (fun f ↦ map_mono f h)
+
+variable (F L)
+
+/-- `normalClosure` as a `ClosureOperator`. -/
+@[simps]
+noncomputable def closureOperator : ClosureOperator (IntermediateField F L) where
+  toFun := fun K ↦ normalClosure F K L
+  monotone' := fun K K' ↦ normalClosure_mono K K'
+  le_closure' := le_normalClosure
+  idempotent' := fun K ↦ normalClosure_of_normal (normalClosure F K L)
+
+variable {K : IntermediateField F L} {F L}
+
+lemma normal_iff_normalClosure_eq : Normal F K ↔ normalClosure F K L = K :=
+⟨@normalClosure_of_normal (K := K), fun h ↦ h ▸ normalClosure.normal F K L⟩
+
+lemma normal_iff_normalClosure_le : Normal F K ↔ normalClosure F K L ≤ K :=
+normal_iff_normalClosure_eq.trans (le_normalClosure K).le_iff_eq.symm
+
+lemma normal_iff_forall_fieldRange_le : Normal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange ≤ K :=
+by rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]
+
+lemma normal_iff_forall_map_le : Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ ≤ K :=
+by rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]
+
+lemma normal_iff_forall_map_le' : Normal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ ≤ K :=
+by rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]
+
+lemma normal_iff_forall_fieldRange_eq : Normal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange = K :=
+⟨@AlgHom.fieldRange_of_normal (E := K), normal_iff_forall_fieldRange_le.2 ∘ fun h σ ↦ (h σ).le⟩
+
+lemma normal_iff_forall_map_eq : Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ = K :=
+⟨fun h σ ↦ (K.fieldRange_val ▸ AlgHom.map_fieldRange K.val σ).trans
+  (normal_iff_forall_fieldRange_eq.1 h _), fun h ↦ normal_iff_forall_map_le.2 (fun σ ↦ (h σ).le)⟩
+
+lemma normal_iff_forall_map_eq' : Normal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ = K :=
+⟨fun h σ ↦ normal_iff_forall_map_eq.1 h σ, fun h ↦ normal_iff_forall_map_le'.2 (fun σ ↦ (h σ).le)⟩
+
+end IntermediateField