feat(FieldTheory/SeparableClosure): (relative) separable closure (lea…

…nprover-community#9338)

Main definitions:

- `separableClosure`: the (relative) separable closure of `E / F`, or called maximal separable subextension of `E / F`, is defined to be the intermediate field of `E / F` consisting of all separable elements.
- `Field.sepDegree F E`: the (infinite) separable degree `[E:F]_s` of an algebraic extension `E / F` of fields, defined to be the degree of `separableClosure F E / F`.
- `Field.insepDegree F E`: the (infinite) inseparable degree `[E:F]_i` of an algebraic extension `E / F` of fields, defined to be the degree of `E / separableClosure F E`.
- `Field.finInsepDegree F E`: the (finite) inseparable degree `[E:F]_i` of an algebraic extension `E / F` of fields, defined to be the degree of `E / separableClosure F E` as a natural number. It is zero if such field extension is not finite.

Main results:

- `le_separableClosure_iff`: an intermediate field of `E / F` is contained in the (relative) separable closure of `E / F` if and only if it is separable over `F`.
- `separableClosure.normalClosure_eq_self`: the normal closure of the (relative) separable closure of `E / F` is equal to itself.
- `separableClosure.normal`: the (relative) separable closure of a normal extension is normal.
- `separableClosure.isSepClosure`: the (relative) separable closure of a separably closed extension is a separable closure of the base field.
- `IntermediateField.isSeparable_adjoin_iff_separable`: `F(S) / F` is a separable extension if and only if all elements of `S` are separable elements.
- `separableClosure.eq_top_iff`: the (relative) separable closure of `E / F` is equal to `E` if and only if `E / F` is separable.

Mathlib.lean

@@ -2085,6 +2085,7 @@ import Mathlib.FieldTheory.PolynomialGaloisGroup
 import Mathlib.FieldTheory.PrimitiveElement
 import Mathlib.FieldTheory.RatFunc
 import Mathlib.FieldTheory.Separable
+import Mathlib.FieldTheory.SeparableClosure
 import Mathlib.FieldTheory.SeparableDegree
 import Mathlib.FieldTheory.SplittingField.Construction
 import Mathlib.FieldTheory.SplittingField.IsSplittingField

Mathlib/FieldTheory/Adjoin.lean

@@ -102,6 +102,10 @@ instance : CompleteLattice (IntermediateField F E) where
 instance : Inhabited (IntermediateField F E) :=
   ⟨⊤⟩
 
+instance : Unique (IntermediateField F F) :=
+  { inferInstanceAs (Inhabited (IntermediateField F F)) with
+    uniq := fun _ ↦ toSubalgebra_injective <| Subsingleton.elim _ _ }
+
 theorem coe_bot : ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E) := rfl
 #align intermediate_field.coe_bot IntermediateField.coe_bot
 

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -184,6 +184,15 @@ theorem algebraMap_surjective_of_isAlgebraic {k K : Type*} [Field k] [Ring K] [I
 
 end IsAlgClosed
 
+/-- If `k` is algebraically closed, `K / k` is a field extension, `L / k` is an intermediate field
+which is algebraic, then `L` is equal to `k`. A corollary of
+`IsAlgClosed.algebraMap_surjective_of_isAlgebraic`. -/
+theorem IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic {k K : Type*} [Field k] [Field K]
+    [IsAlgClosed k] [Algebra k K] (L : IntermediateField k K) (hf : Algebra.IsAlgebraic k L) :
+    L = ⊥ := bot_unique fun x hx ↦ by
+  obtain ⟨y, hy⟩ := IsAlgClosed.algebraMap_surjective_of_isAlgebraic hf ⟨x, hx⟩
+  exact ⟨y, congr_arg (algebraMap L K) hy⟩
+
 /-- Typeclass for an extension being an algebraic closure. -/
 class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K]
     [NoZeroSMulDivisors R K] : Prop where

Mathlib/FieldTheory/IsSepClosed.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jz Pan
 -/
 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
+import Mathlib.FieldTheory.Galois
 
 /-!
 # Separably Closed Field
@@ -29,15 +30,17 @@ and prove some of their properties.
 
 separable closure, separably closed
 
-## TODO
+## Related
+
+- `separableClosure`: maximal separable subextension of `K/k`, consisting of all elements of `K`
+  which are separable over `k`.
 
-- Maximal separable subextension of `K/k`, consisting of all elements of `K` which are separable
-  over `k`.
+- `separableClosure.isSepClosure`: if `K` is a separably closed field containing `k`, then the
+  maximal separable subextension of `K/k` is a separable closure of `k`.
 
-- If `K` is a separably closed field containing `k`, then the maximal separable subextension
-  of `K/k` is a separable closure of `k`.
+- In particular, a separable closure (`SeparableClosure`) exists.
 
-- In particular, a separable closure exists.
+## TODO
 
 - If `k` is a perfect field, then its separable closure coincides with its algebraic closure.
 
@@ -153,7 +156,7 @@ theorem degree_eq_one_of_irreducible [IsSepClosed k] {p : k[X]}
     (hp : Irreducible p) (hsep : p.Separable) : p.degree = 1 :=
   degree_eq_one_of_irreducible_of_splits hp (IsSepClosed.splits_codomain p hsep)
 
-variable {k}
+variable (K)
 
 theorem algebraMap_surjective
     [IsSepClosed k] [Algebra k K] [IsSeparable k K] :
@@ -170,6 +173,13 @@ theorem algebraMap_surjective
 
 end IsSepClosed
 
+/-- If `k` is separably closed, `K / k` is a field extension, `L / k` is an intermediate field
+which is separable, then `L` is equal to `k`. A corollary of `IsSepClosed.algebraMap_surjective`. -/
+theorem IntermediateField.eq_bot_of_isSepClosed_of_isSeparable [IsSepClosed k] [Algebra k K]
+    (L : IntermediateField k K) [IsSeparable k L] : L = ⊥ := bot_unique fun x hx ↦ by
+  obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩
+  exact ⟨y, congr_arg (algebraMap L K) hy⟩
+
 variable (k) (K)
 
 /-- Typeclass for an extension being a separable closure. -/
@@ -192,8 +202,9 @@ namespace IsSepClosure
 instance isSeparable [Algebra k K] [IsSepClosure k K] : IsSeparable k K :=
   IsSepClosure.separable
 
-instance (priority := 100) normal [Algebra k K] [IsSepClosure k K] : Normal k K :=
-  ⟨fun x ↦ (IsSeparable.isIntegral k x).isAlgebraic,
+instance (priority := 100) isGalois [Algebra k K] [IsSepClosure k K] : IsGalois k K where
+  to_isSeparable := IsSepClosure.separable
+  to_normal := ⟨fun x ↦ (IsSeparable.isIntegral k x).isAlgebraic,
     fun x ↦ (IsSepClosure.sep_closed k).splits_codomain _ (IsSeparable.separable k x)⟩
 
 end IsSepClosure