feat(FieldTheory): add basic api's for relative algebraic closure (#1…

…6771)

Move the definition of `algebraicClosure` into a separated file (mimicing `seperableClosure` in file FieldTheory.SeperableClosure). Add APIs for `algebraicClosure`. Most are copied api's from `separableClosure`. Show that every algebraic intermediate extension is contained in the algebraic closure.



Co-authored-by: Junyan Xu <[email protected]>
Co-authored-by: Jiang Jiedong <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Junyan Xu <[email protected]>

Mathlib.lean

@@ -2791,6 +2791,7 @@ import Mathlib.Dynamics.TopologicalEntropy.Semiconj
 import Mathlib.FieldTheory.AbelRuffini
 import Mathlib.FieldTheory.AbsoluteGaloisGroup
 import Mathlib.FieldTheory.Adjoin
+import Mathlib.FieldTheory.AlgebraicClosure
 import Mathlib.FieldTheory.AxGrothendieck
 import Mathlib.FieldTheory.Cardinality
 import Mathlib.FieldTheory.ChevalleyWarning

Mathlib/FieldTheory/AlgebraicClosure.lean

@@ -0,0 +1,202 @@
+/-
+Copyright (c) 2024 Jiedong Jiang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu, Jiedong Jiang
+-/
+import Mathlib.FieldTheory.NormalClosure
+import Mathlib.FieldTheory.IsAlgClosed.Basic
+import Mathlib.FieldTheory.IntermediateField.Algebraic
+
+/-!
+# Relative Algebraic Closure
+
+In this file we construct the relative algebraic closure of a field extension.
+
+## Main Definitions
+
+- `algebraicClosure F E` is the relative algebraic closure (i.e. the maximal algebraic subextension)
+  of the field extension `E / F`, which is defined to be the integral closure of `F` in `E`.
+
+-/
+noncomputable section
+
+open Polynomial FiniteDimensional IntermediateField Field
+
+variable (F E : Type*) [Field F] [Field E] [Algebra F E]
+variable {K : Type*} [Field K] [Algebra F K]
+
+/--
+The *relative algebraic closure* of a field `F` in a field extension `E`,
+also called the *maximal algebraic subextension* of `E / F`,
+is defined to be the subalgebra `integralClosure F E`
+upgraded to an intermediate field (since `F` and `E` are both fields).
+This is exactly the intermediate field of `E / F` consisting of all integral/algebraic elements.
+-/
+def algebraicClosure : IntermediateField F E :=
+  Algebra.IsAlgebraic.toIntermediateField (integralClosure F E)
+
+variable {F E}
+
+/-- An element is contained in the algebraic closure of `F` in `E` if and only if
+it is an integral element. -/
+theorem mem_algebraicClosure_iff' {x : E} :
+    x ∈ algebraicClosure F E ↔ IsIntegral F x := Iff.rfl
+
+/-- An element is contained in the algebraic closure of `F` in `E` if and only if
+it is an algebraic element. -/
+theorem mem_algebraicClosure_iff {x : E} :
+    x ∈ algebraicClosure F E ↔ IsAlgebraic F x := isAlgebraic_iff_isIntegral.symm
+
+/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
+`algebraicClosure F K` if and only if `x` is contained in `algebraicClosure F E`. -/
+theorem map_mem_algebraicClosure_iff (i : E →ₐ[F] K) {x : E} :
+    i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E := by
+  simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]
+
+namespace algebraicClosure
+
+/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the preimage of
+`algebraicClosure F K` under the map `i` is equal to `algebraicClosure F E`. -/
+theorem comap_eq_of_algHom (i : E →ₐ[F] K) :
+    (algebraicClosure F K).comap i = algebraicClosure F E := by
+  ext x
+  exact map_mem_algebraicClosure_iff i
+
+/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `algebraicClosure F E`
+under the map `i` is contained in `algebraicClosure F K`. -/
+theorem map_le_of_algHom (i : E →ₐ[F] K) :
+    (algebraicClosure F E).map i ≤ algebraicClosure F K :=
+  map_le_iff_le_comap.2 (comap_eq_of_algHom i).ge
+
+variable (F) in
+/-- If `K / E / F` is a field extension tower, such that `K / E` has no non-trivial algebraic
+subextensions (this means that it is purely transcendental),
+then the image of `algebraicClosure F E` in `K` is equal to `algebraicClosure F K`. -/
+theorem map_eq_of_algebraicClosure_eq_bot [Algebra E K] [IsScalarTower F E K]
+    (h : algebraicClosure E K = ⊥) :
+    (algebraicClosure F E).map (IsScalarTower.toAlgHom F E K) = algebraicClosure F K := by
+  refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
+  obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
+    (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)
+  exact ⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩
+
+/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `algebraicClosure F E`
+under the map `i` is equal to `algebraicClosure F K`. -/
+theorem map_eq_of_algEquiv (i : E ≃ₐ[F] K) :
+    (algebraicClosure F E).map i = algebraicClosure F K :=
+  (map_le_of_algHom i.toAlgHom).antisymm
+    (fun x h ↦ ⟨_, (map_mem_algebraicClosure_iff i.symm).2 h, by simp⟩)
+
+/-- If `E` and `K` are isomorphic as `F`-algebras, then `algebraicClosure F E` and
+`algebraicClosure F K` are also isomorphic as `F`-algebras. -/
+def algEquivOfAlgEquiv (i : E ≃ₐ[F] K) :
+    algebraicClosure F E ≃ₐ[F] algebraicClosure F K :=
+  (intermediateFieldMap i _).trans (equivOfEq (map_eq_of_algEquiv i))
+
+alias AlgEquiv.algebraicClosure := algebraicClosure.algEquivOfAlgEquiv
+
+variable (F E K)
+
+/-- The algebraic closure of `F` in `E` is algebraic over `F`. -/
+instance isAlgebraic : Algebra.IsAlgebraic F (algebraicClosure F E) :=
+  ⟨fun x ↦
+    isAlgebraic_iff.mpr (IsAlgebraic.isIntegral (mem_algebraicClosure_iff.mp x.2)).isAlgebraic⟩
+
+/-- The algebraic closure of `F` in `E` is the integral closure of `F` in `E`. -/
+instance isIntegralClosure : IsIntegralClosure (algebraicClosure F E) F E :=
+  inferInstanceAs (IsIntegralClosure (integralClosure F E) F E)
+
+end algebraicClosure
+
+variable (F E K)
+
+/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
+if all of its elements are algebraic over `F`. -/
+theorem le_algebraicClosure' {L : IntermediateField F E} (hs : ∀ x : L, IsAlgebraic F x) :
+    L ≤ algebraicClosure F E := fun x h ↦ by
+  simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
+    Algebra.id.map_eq_id, RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩
+
+/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
+if it is algebraic over `F`. -/
+theorem le_algebraicClosure (L : IntermediateField F E) [Algebra.IsAlgebraic F L] :
+    L ≤ algebraicClosure F E := le_algebraicClosure' F E (Algebra.IsAlgebraic.isAlgebraic)
+
+/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
+if and only if it is algebraic over `F`. -/
+theorem le_algebraicClosure_iff (L : IntermediateField F E) :
+    L ≤ algebraicClosure F E ↔ Algebra.IsAlgebraic F L :=
+  ⟨fun h ↦ ⟨fun x ↦ by simpa only [IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
+    IntermediateField.algebraMap_apply,
+    Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, mem_algebraicClosure_iff] using h x.2⟩,
+    fun _ ↦ le_algebraicClosure _ _ _⟩
+
+namespace algebraicClosure
+
+/-- The algebraic closure in `E` of the algebraic closure of `F` in `E` is equal to itself. -/
+theorem algebraicClosure_eq_bot :
+    algebraicClosure (algebraicClosure F E) E = ⊥ :=
+  bot_unique fun x hx ↦ mem_bot.2
+    ⟨⟨x, isIntegral_trans x (mem_algebraicClosure_iff'.1 hx)⟩, rfl⟩
+
+/-- The normal closure in `E/F` of the algebraic closure of `F` in `E` is equal to itself. -/
+theorem normalClosure_eq_self :
+    normalClosure F (algebraicClosure F E) E = algebraicClosure F E :=
+  le_antisymm (normalClosure_le_iff.2 fun i ↦
+    haveI : Algebra.IsAlgebraic F i.fieldRange := (AlgEquiv.ofInjectiveField i).isAlgebraic
+    le_algebraicClosure F E _) (le_normalClosure _)
+
+end algebraicClosure
+
+/-- If `E / F` is a field extension and `E` is algebraically closed, then the algebraic closure
+of `F` in `E` is equal to `F` if and only if `F` is algebraically closed. -/
+theorem IsAlgClosed.algebraicClosure_eq_bot_iff [IsAlgClosed E] :
+    algebraicClosure F E = ⊥ ↔ IsAlgClosed F := by
+  refine ⟨fun h ↦ IsAlgClosed.of_exists_root _ fun p hmon hirr ↦ ?_,
+    fun _ ↦ IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic _⟩
+  obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne'
+  obtain ⟨x, rfl⟩ := h ▸ mem_algebraicClosure_iff'.2 (minpoly.ne_zero_iff.1 <|
+    ne_zero_of_dvd_ne_zero hmon.ne_zero (minpoly.dvd _ x hx))
+  exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩
+
+/-- `F(S) / F` is a algebraic extension if and only if all elements of `S` are
+algebraic elements. -/
+theorem IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic {S : Set E} :
+    Algebra.IsAlgebraic F (adjoin F S) ↔ ∀ x ∈ S, IsAlgebraic F x :=
+  ((le_algebraicClosure_iff F E _).symm.trans (adjoin_le_iff.trans <| forall_congr' <|
+    fun _ => Iff.imp Iff.rfl mem_algebraicClosure_iff))
+
+namespace algebraicClosure
+
+/-- If `E` is algebraically closed, then the algebraic closure of `F` in `E` is an absolute
+algebraic closure of `F`. -/
+instance isAlgClosure [IsAlgClosed E] : IsAlgClosure F (algebraicClosure F E) :=
+  ⟨(IsAlgClosed.algebraicClosure_eq_bot_iff _ E).mp (algebraicClosure_eq_bot F E),
+    isAlgebraic F E⟩
+
+/-- The algebraic closure of `F` in `E` is equal to `E` if and only if `E / F` is
+algebraic. -/
+theorem eq_top_iff : algebraicClosure F E = ⊤ ↔ Algebra.IsAlgebraic F E :=
+  ⟨fun h ↦ ⟨fun _ ↦ mem_algebraicClosure_iff.1 (h ▸ mem_top)⟩,
+    fun _ ↦ top_unique fun x _ ↦ mem_algebraicClosure_iff.2 (Algebra.IsAlgebraic.isAlgebraic x)⟩
+
+/-- If `K / E / F` is a field extension tower, then `algebraicClosure F K` is contained in
+`algebraicClosure E K`. -/
+theorem le_restrictScalars [Algebra E K] [IsScalarTower F E K] :
+    algebraicClosure F K ≤ (algebraicClosure E K).restrictScalars F :=
+  fun _ h ↦ mem_algebraicClosure_iff.2 <| IsAlgebraic.tower_top E (mem_algebraicClosure_iff.1 h)
+
+/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then
+`algebraicClosure F K` is equal to `algebraicClosure E K`. -/
+theorem eq_restrictScalars_of_isAlgebraic [Algebra E K] [IsScalarTower F E K]
+    [Algebra.IsAlgebraic F E] : algebraicClosure F K = (algebraicClosure E K).restrictScalars F :=
+  (algebraicClosure.le_restrictScalars F E K).antisymm fun _ h ↦
+    isIntegral_trans _ h
+
+/-- If `K / E / F` is a field extension tower, then `E` adjoin `algebraicClosure F K` is contained
+in `algebraicClosure E K`. -/
+theorem adjoin_le [Algebra E K] [IsScalarTower F E K] :
+    adjoin E (algebraicClosure F K) ≤ algebraicClosure E K :=
+  adjoin_le_iff.2 <| le_restrictScalars F E K
+
+end algebraicClosure

Mathlib/FieldTheory/IntermediateField/Algebraic.lean

@@ -15,7 +15,7 @@ import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 open Module
 
-variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
   {S : IntermediateField K L}
 
 theorem IntermediateField.coe_isIntegral_iff {R : Type*} [CommRing R] [Algebra R K] [Algebra R L]
@@ -33,11 +33,6 @@ def Subalgebra.IsAlgebraic.toIntermediateField {S : Subalgebra K L} (hS : S.IsAl
 abbrev Algebra.IsAlgebraic.toIntermediateField (S : Subalgebra K L) [Algebra.IsAlgebraic K S] :
     IntermediateField K L := (S.isAlgebraic_iff.mpr ‹_›).toIntermediateField
 
-/-- The algebraic closure of a field `K` in an extension `L`, the subalgebra `integralClosure K L`
-upgraded to an intermediate field (when `K` and `L` are both fields). -/
-def algebraicClosure : IntermediateField K L :=
-  Algebra.IsAlgebraic.toIntermediateField (integralClosure K L)
-
 namespace IntermediateField
 
 instance isAlgebraic_tower_bot [Algebra.IsAlgebraic K L] : Algebra.IsAlgebraic K S :=

Mathlib/FieldTheory/Minpoly/Basic.lean

@@ -58,6 +58,9 @@ theorem ne_zero [Nontrivial A] (hx : IsIntegral A x) : minpoly A x ≠ 0 :=
 theorem eq_zero (hx : ¬IsIntegral A x) : minpoly A x = 0 :=
   dif_neg hx
 
+theorem ne_zero_iff [Nontrivial A] : minpoly A x ≠ 0 ↔ IsIntegral A x :=
+  ⟨fun h => of_not_not <| eq_zero.mt h, ne_zero⟩
+
 theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
     minpoly A (f x) = minpoly A x := by
   simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,

Mathlib/RingTheory/Adjoin/Field.lean

@@ -116,6 +116,7 @@ end
 
 variable [Algebra K M] [IsScalarTower R K M] {x : M}
 
+/-- The `RingHom` version of `IsIntegral.minpoly_splits_tower_top`.  -/
 theorem IsIntegral.minpoly_splits_tower_top' (int : IsIntegral R x) {f : K →+* L}
     (h : Splits (f.comp <| algebraMap R K) (minpoly R x)) :
     Splits f (minpoly K x) :=

Mathlib/RingTheory/Algebraic.lean

@@ -296,6 +296,12 @@ alias ⟨IsAlgebraic.isIntegral, _⟩ := isAlgebraic_iff_isIntegral
 protected instance Algebra.IsAlgebraic.isIntegral [Algebra.IsAlgebraic K A] :
     Algebra.IsIntegral K A := Algebra.isAlgebraic_iff_isIntegral.mp ‹_›
 
+variable (K) in
+theorem Algebra.IsAlgebraic.of_isIntegralClosure (B C : Type*)
+    [CommRing B] [CommRing C] [Algebra K B] [Algebra K C] [Algebra B C]
+    [IsScalarTower K B C] [IsIntegralClosure B K C] : Algebra.IsAlgebraic K B :=
+  Algebra.isAlgebraic_iff_isIntegral.mpr (IsIntegralClosure.isIntegral_algebra K C)
+
 end Field
 
 section