feat(Mathlib/FieldTheory/IsSepClosed) separably closed field and sepa…

…rable closure - basic definition (#6285)

Main changes

- Add `IsSepClosed` and basic properties.
- Add `IsSepClosure` and basic properties.



Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -1893,6 +1893,7 @@ import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.FieldTheory.IsAlgClosed.Classification
 import Mathlib.FieldTheory.IsAlgClosed.Spectrum
+import Mathlib.FieldTheory.IsSepClosed
 import Mathlib.FieldTheory.KrullTopology
 import Mathlib.FieldTheory.Laurent
 import Mathlib.FieldTheory.Minpoly.Basic

Mathlib/FieldTheory/IsSepClosed.lean

@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2023 Jz Pan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jz Pan
+-/
+import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
+
+/-!
+# Separably Closed Field
+
+In this file we define the typeclass for separably closed fields and separable closures,
+and prove some of their properties.
+
+## Main Definitions
+
+- `IsSepClosed k` is the typeclass saying `k` is a separably closed field, i.e. every separable
+  polynomial in `k` splits.
+
+- `IsSepClosure k K` is the typeclass saying `K` is a separable closure of `k`, where `k` is a
+  field. This means that `K` is separably closed and separable over `k`.
+
+## Tags
+
+separable closure, separably closed
+
+## TODO
+
+- `IsSepClosed.lift` is a map from a separable extension `L` of `k`, into any separably
+  closed extension of `k`.
+
+- `IsSepClosed.equiv` is a proof that any two separable closures of the
+  same field are isomorphic.
+
+- If `K` is a separably closed field (or algebraically closed field) containing `k`, then all
+  elements of `K` which are separable over `k` form a separable closure of `k`.
+
+- Using the above result, construct a separable closure as a subfield of an algebraic closure.
+
+- If `k` is a perfect field, then its separable closure coincides with its algebraic closure.
+
+- An algebraic extension of a separably closed field is purely inseparable.
+
+- Maximal separable subextension ...
+
+-/
+
+universe u v w
+
+open scoped Classical BigOperators Polynomial
+
+open Polynomial
+
+variable (k : Type u) [Field k] (K : Type v) [Field K]
+
+/-- Typeclass for separably closed fields.
+
+To show `Polynomial.Splits p f` for an arbitrary ring homomorphism `f`,
+see `IsSepClosed.splits_codomain` and `IsSepClosed.splits_domain`.
+-/
+class IsSepClosed : Prop where
+  splits_of_separable : ∀ p : k[X], p.Separable → (p.Splits <| RingHom.id k)
+
+variable {k} {K}
+
+/-- Every separable polynomial splits in the field extension `f : k →+* K` if `K` is
+separably closed.
+
+See also `IsSepClosed.splits_domain` for the case where `k` is separably closed.
+-/
+theorem IsSepClosed.splits_codomain [IsSepClosed K] {f : k →+* K}
+    (p : k[X]) (h : p.Separable) : p.Splits f := by
+  convert IsSepClosed.splits_of_separable (p.map f) (Separable.map h); simp [splits_map_iff]
+
+/-- Every separable polynomial splits in the field extension `f : k →+* K` if `k` is
+separably closed.
+
+See also `IsSepClosed.splits_codomain` for the case where `k` is separably closed.
+-/
+theorem IsSepClosed.splits_domain [IsSepClosed k] {f : k →+* K}
+    (p : k[X]) (h : p.Separable) : p.Splits f :=
+  Polynomial.splits_of_splits_id _ <| IsSepClosed.splits_of_separable _ h
+
+namespace IsSepClosed
+
+theorem exists_root [IsSepClosed k] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
+    ∃ x, IsRoot p x :=
+  exists_root_of_splits _ (IsSepClosed.splits_of_separable p hsep) hp
+
+theorem exists_pow_nat_eq [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero (n : k)] :
+    ∃ z, z ^ n = x := by
+  have hn' : 0 < n := Nat.pos_of_ne_zero <| fun h => by
+    rw [h, Nat.cast_zero] at hn
+    exact hn.out rfl
+  have : degree (X ^ n - C x) ≠ 0 := by
+    rw [degree_X_pow_sub_C hn' x]
+    exact (WithBot.coe_lt_coe.2 hn').ne'
+  by_cases hx : x = 0
+  · exact ⟨0, by rw [hx, pow_eq_zero_iff hn']⟩
+  · obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx
+    use z
+    simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz
+
+theorem exists_eq_mul_self [IsSepClosed k] (x : k) [h2 : NeZero (2 : k)] : ∃ z, x = z * z := by
+  rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
+  exact ⟨z, sq z⟩
+
+theorem roots_eq_zero_iff [IsSepClosed k] {p : k[X]} (hsep : p.Separable) :
+    p.roots = 0 ↔ p = Polynomial.C (p.coeff 0) := by
+  refine' ⟨fun h => _, fun hp => by rw [hp, roots_C]⟩
+  cases' le_or_lt (degree p) 0 with hd hd
+  · exact eq_C_of_degree_le_zero hd
+  · obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep
+    rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
+    simp at hz
+
+theorem exists_eval₂_eq_zero [IsSepClosed K] (f : k →+* K)
+    (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
+    ∃ x, p.eval₂ f x = 0 :=
+  let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective f.injective])
+    (Separable.map hsep)
+  ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩
+
+variable (k)
+
+theorem exists_aeval_eq_zero [IsSepClosed K] [Algebra k K] (p : k[X])
+    (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x : K, aeval x p = 0 :=
+  exists_eval₂_eq_zero (algebraMap k K) p hp hsep
+
+theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → Separable p → ∃ x, p.eval x = 0) :
+    IsSepClosed k := by
+  refine ⟨fun p hsep ↦ Or.inr ?_⟩
+  intro q hq hdvd
+  simp only [map_id] at hdvd
+  have hlc : IsUnit (leadingCoeff q)⁻¹ := IsUnit.inv <| Ne.isUnit <|
+    leadingCoeff_ne_zero.2 <| Irreducible.ne_zero hq
+  have hsep' : Separable (q * C (leadingCoeff q)⁻¹) :=
+    Separable.mul (Separable.of_dvd hsep hdvd) ((separable_C _).2 hlc)
+    (by simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul]
+      using isCoprime_one_right (x := q))
+  have hirr' := hq
+  rw [← irreducible_mul_isUnit (isUnit_C.2 hlc)] at hirr'
+  obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) hirr' hsep'
+  exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root hirr' hx
+
+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}
+
+theorem algebraMap_surjective
+    [IsSepClosed k] [Algebra k K] [IsSeparable k K] :
+    Function.Surjective (algebraMap k K) := by
+  refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
+  have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (IsSeparable.isIntegral k x)
+  have hsep : (minpoly k x).Separable := IsSeparable.separable k x
+  have h : (minpoly k x).degree = 1 :=
+    degree_eq_one_of_irreducible k (minpoly.irreducible (IsSeparable.isIntegral k x)) hsep
+  have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
+  rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
+    add_eq_zero_iff_eq_neg] at this
+  exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
+
+end IsSepClosed
+
+variable (k) (K)
+
+/-- Typeclass for an extension being a separable closure. -/
+class IsSepClosure [Algebra k K] : Prop where
+  sep_closed : IsSepClosed K
+  separable : IsSeparable k K
+
+variable {k} {K}
+
+theorem isSepClosure_iff [Algebra k K] :
+    IsSepClosure k K ↔ IsSepClosed K ∧ IsSeparable k K :=
+  ⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩
+
+instance (priority := 100) IsSepClosure.normal [Algebra k K]
+    [IsSepClosure k K] : Normal k K :=
+  ⟨fun x => by apply IsIntegral.isAlgebraic; exact IsSepClosure.separable.isIntegral' x,
+    fun x => @IsSepClosed.splits_codomain _ _ _ _ (IsSepClosure.sep_closed k) _ _ (by
+      have : IsSeparable k K := IsSepClosure.separable
+      exact IsSeparable.separable k x)⟩