From 417f344b6d5b5e820792c4a6ae79d6b8abae5053 Mon Sep 17 00:00:00 2001
From: Jz Pan <acme_pjz@hotmail.com>
Date: Mon, 8 Jan 2024 14:36:25 +0000
Subject: [PATCH] feat(FieldTheory/IsSepClosed): add some results on separable
 closure and perfect field (#9522)

- `IsSepClosure.isAlgClosure_of_perfectField`, `IsSepClosure.of_isAlgClosure_of_perfectField`: if `k` is a perfect field, then its separable closure coincides with its algebraic closure.
- `IsSepClosed.isAlgClosed_of_perfectField`: a separably closed perfect field is also algebraically closed.
- `Algebra.IsAlgebraic.[isSeparable_of_]perfectField`: if `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable and `L` is perfect.
---
 Mathlib/FieldTheory/IsSepClosed.lean | 38 ++++++++++++++++++++++++----
 Mathlib/FieldTheory/Perfect.lean     | 14 ++++++++++
 Mathlib/RingTheory/AdjoinRoot.lean   | 11 ++++++++
 3 files changed, 58 insertions(+), 5 deletions(-)

diff --git a/Mathlib/FieldTheory/IsSepClosed.lean b/Mathlib/FieldTheory/IsSepClosed.lean
index 76070f0d8a24d..f524489640618 100644
--- a/Mathlib/FieldTheory/IsSepClosed.lean
+++ b/Mathlib/FieldTheory/IsSepClosed.lean
@@ -26,6 +26,9 @@ and prove some of their properties.
 - `IsSepClosure.equiv` is a proof that any two separable closures of the
   same field are isomorphic.
 
+- `IsSepClosure.isAlgClosure_of_perfectField`, `IsSepClosure.of_isAlgClosure_of_perfectField`:
+  if `k` is a perfect field, then its separable closure coincides with its algebraic closure.
+
 ## Tags
 
 separable closure, separably closed
@@ -40,11 +43,8 @@ separable closure, separably closed
 
 - In particular, a separable closure (`SeparableClosure`) exists.
 
-## TODO
-
-- 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.
+- `Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed`: an algebraic extension of a separably
+  closed field is purely inseparable.
 
 -/
 
@@ -94,6 +94,13 @@ theorem exists_root [IsSepClosed k] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.S
     ∃ x, IsRoot p x :=
   exists_root_of_splits _ (IsSepClosed.splits_of_separable p hsep) hp
 
+variable (k) in
+/-- A separably closed perfect field is also algebraically closed. -/
+instance (priority := 100) isAlgClosed_of_perfectField [IsSepClosed k] [PerfectField k] :
+    IsAlgClosed k :=
+  IsAlgClosed.of_exists_root k fun p _ h ↦ exists_root p ((degree_pos_of_irreducible h).ne')
+    (PerfectField.separable_of_irreducible h)
+
 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
@@ -191,6 +198,27 @@ class IsSepClosure [Algebra k K] : Prop where
 instance IsSepClosure.self_of_isSepClosed [IsSepClosed k] : IsSepClosure k k :=
   ⟨by assumption, isSeparable_self k⟩
 
+/-- If `K` is perfect and is a separable closure of `k`,
+then it is also an algebraic closure of `k`. -/
+instance (priority := 100) IsSepClosure.isAlgClosure_of_perfectField_top
+    [Algebra k K] [IsSepClosure k K] [PerfectField K] : IsAlgClosure k K :=
+  haveI : IsSepClosed K := IsSepClosure.sep_closed k
+  ⟨inferInstance, IsSepClosure.separable.isAlgebraic⟩
+
+/-- If `k` is perfect, `K` is a separable closure of `k`,
+then it is also an algebraic closure of `k`. -/
+instance (priority := 100) IsSepClosure.isAlgClosure_of_perfectField
+    [Algebra k K] [IsSepClosure k K] [PerfectField k] : IsAlgClosure k K :=
+  have halg : Algebra.IsAlgebraic k K := IsSepClosure.separable.isAlgebraic
+  haveI := halg.perfectField; inferInstance
+
+/-- If `k` is perfect, `K` is an algebraic closure of `k`,
+then it is also a separable closure of `k`. -/
+instance (priority := 100) IsSepClosure.of_isAlgClosure_of_perfectField
+    [Algebra k K] [IsAlgClosure k K] [PerfectField k] : IsSepClosure k K :=
+  ⟨haveI := IsAlgClosure.alg_closed (R := k) (K := K); inferInstance,
+    (IsAlgClosure.algebraic (R := k) (K := K)).isSeparable_of_perfectField⟩
+
 variable {k} {K}
 
 theorem isSepClosure_iff [Algebra k K] :
diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean
index 826515c0be10b..860f9930a1e5f 100644
--- a/Mathlib/FieldTheory/Perfect.lean
+++ b/Mathlib/FieldTheory/Perfect.lean
@@ -24,6 +24,9 @@ prime characteristic.
    sense of Serre.
  * `PerfectField.ofCharZero`: all fields of characteristic zero are perfect.
  * `PerfectField.ofFinite`: all finite fields are perfect.
+ * `Algebra.IsAlgebraic.isSeparable_of_perfectField`, `Algebra.IsAlgebraic.perfectField`:
+   if `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable,
+   and `L` is also a perfect field.
 
 -/
 
@@ -218,3 +221,14 @@ instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K
   exact minpoly.degree_pos ha
 
 end PerfectField
+
+/-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable. -/
+theorem Algebra.IsAlgebraic.isSeparable_of_perfectField {K L : Type*} [Field K] [Field L]
+    [Algebra K L] [PerfectField K] (halg : Algebra.IsAlgebraic K L) : IsSeparable K L :=
+  ⟨fun x ↦ PerfectField.separable_of_irreducible <| minpoly.irreducible (halg x).isIntegral⟩
+
+/-- If `L / K` is an algebraic extension, `K` is a perfect field, then so is `L`. -/
+theorem Algebra.IsAlgebraic.perfectField {K L : Type*} [Field K] [Field L] [Algebra K L]
+    [PerfectField K] (halg : Algebra.IsAlgebraic K L) : PerfectField L := ⟨fun {f} hf ↦ by
+  obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral halg.isIntegral
+  exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h⟩
diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean
index b7a1a6927ebdf..1e562581c6d08 100644
--- a/Mathlib/RingTheory/AdjoinRoot.lean
+++ b/Mathlib/RingTheory/AdjoinRoot.lean
@@ -923,3 +923,14 @@ theorem quotientEquivQuotientMinpolyMap_symm_apply_mk (pb : PowerBasis R S) (I :
 #align power_basis.quotient_equiv_quotient_minpoly_map_symm_apply_mk PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk
 
 end PowerBasis
+
+/-- If `L / K` is an integral extension, `K` is a domain, `L` is a field, then any irreducible
+polynomial over `L` divides some monic irreducible polynomial over `K`. -/
+theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K L : Type*}
+    [CommRing K] [IsDomain K] [Field L] [Algebra K L] (H : Algebra.IsIntegral K L) {f : L[X]}
+    (hf : Irreducible f) : ∃ g : K[X], g.Monic ∧ Irreducible g ∧ f ∣ g.map (algebraMap K L) := by
+  haveI := Fact.mk hf
+  have h := hf.ne_zero
+  have h2 := isIntegral_trans H _ (AdjoinRoot.isIntegral_root h)
+  have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
+  exact ⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩