feat(FieldTheory/IsSepClosed): add IsSepClosed.lift and `IsSepClosu…

…re.equiv` (#6670)

- `IsSepClosed.lift` is a map from a separable extension `L` of `K`, into any separably closed extension `M` of `K`.

- `IsSepClosure.equiv` is a proof that any two separable closures of the
  same field are isomorphic.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -351,10 +351,9 @@ variable {K : Type u} [Field K] {L : Type v} {M : Type w} [Field L] [Algebra K L
 variable (K L M)
 
 /-- Less general version of `lift`. -/
-private noncomputable irreducible_def lift_aux : L →ₐ[K] M :=
-  (lift.SubfieldWithHom.maximalSubfieldWithHom K L M).emb.comp <|
-    (lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top (K := K) (L := L) (M := M) (hL := hL)).symm
-      ▸ Algebra.toTop
+private noncomputable irreducible_def lift_aux : L →ₐ[K] M := Classical.choice <|
+  IntermediateField.algHom_mk_adjoin_splits' (IntermediateField.adjoin_univ K L)
+    (fun x _ ↦ ⟨isAlgebraic_iff_isIntegral.1 (hL x), splits_codomain (minpoly K x)⟩)
 
 variable {R : Type u} [CommRing R]
 
@@ -425,19 +424,11 @@ variable [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L]
 /-- A (random) isomorphism between two algebraic closures of `R`. -/
 noncomputable def equiv : L ≃ₐ[R] M :=
   -- Porting note: added to replace local instance above
+  haveI : IsAlgClosed L := IsAlgClosure.alg_closed R
   haveI : IsAlgClosed M := IsAlgClosure.alg_closed R
-  let f : L →ₐ[R] M := IsAlgClosed.lift IsAlgClosure.algebraic
-  AlgEquiv.ofBijective f
-    ⟨RingHom.injective f.toRingHom, by
-      letI : Algebra L M := RingHom.toAlgebra f
-      letI : IsScalarTower R L M := IsScalarTower.of_algebraMap_eq <| by
-        simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_coe, AlgHom.commutes, forall_const]
-      letI : IsAlgClosed L := IsAlgClosure.alg_closed R
-      show Function.Surjective (algebraMap L M)
-      exact
-        IsAlgClosed.algebraMap_surjective_of_isAlgebraic
-          (Algebra.isAlgebraic_of_larger_base_of_injective
-            (NoZeroSMulDivisors.algebraMap_injective R _) IsAlgClosure.algebraic)⟩
+  AlgEquiv.ofBijective _ (IsAlgClosure.algebraic.algHom_bijective₂
+    (IsAlgClosed.lift IsAlgClosure.algebraic : L →ₐ[R] M)
+    (IsAlgClosed.lift IsAlgClosure.algebraic : M →ₐ[R] L)).1
 #align is_alg_closure.equiv IsAlgClosure.equiv
 
 end

Mathlib/FieldTheory/IsSepClosed.lean

@@ -19,29 +19,30 @@ and prove some of their properties.
 - `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`.
 
+- `IsSepClosed.lift` is a map from a separable extension `L` of `K`, into any separably
+  closed extension `M` of `K`.
+
+- `IsSepClosure.equiv` is a proof that any two separable closures of the
+  same field are isomorphic.
+
 ## 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`.
+- Maximal separable subextension of `K/k`, consisting of all elements of `K` which are separable
+  over `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`.
+- If `K` is a separably closed field containing `k`, then the maximal separable subextension
+  of `K/k` is a separable closure of `k`.
 
-- Using the above result, construct a separable closure as a subfield of an algebraic closure.
+- In particular, a separable closure exists.
 
 - 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
@@ -60,6 +61,10 @@ 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)
 
+/-- An algebraically closed field is also separably closed. -/
+instance IsSepClosed.of_isAlgClosed [IsAlgClosed k] : IsSepClosed k :=
+  ⟨fun p _ ↦ IsAlgClosed.splits p⟩
+
 variable {k} {K}
 
 /-- Every separable polynomial splits in the field extension `f : k →+* K` if `K` is
@@ -120,12 +125,14 @@ theorem exists_eval₂_eq_zero [IsSepClosed K] (f : k →+* K)
     (Separable.map hsep)
   ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩
 
-variable (k)
+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
 
+variable (k) {K}
+
 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 ?_⟩
@@ -170,15 +177,52 @@ class IsSepClosure [Algebra k K] : Prop where
   sep_closed : IsSepClosed K
   separable : IsSeparable k K
 
+/-- A separably closed field is its separable closure. -/
+instance IsSepClosure.self_of_isSepClosed [IsSepClosed k] : IsSepClosure k k :=
+  ⟨by assumption, isSeparable_self 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)⟩
+  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩
+
+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' x).isAlgebraic k,
+    fun x ↦ (IsSepClosure.sep_closed k).splits_codomain _ (IsSeparable.separable k x)⟩
+
+end IsSepClosure
+
+namespace IsSepClosed
+
+variable {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M]
+  [Algebra K M] [IsSepClosed M] [IsSeparable K L]
+
+/-- A (random) homomorphism from a separable extension L of K into a separably
+  closed extension M of K. -/
+noncomputable irreducible_def lift : L →ₐ[K] M := Classical.choice <|
+  IntermediateField.algHom_mk_adjoin_splits' (IntermediateField.adjoin_univ K L)
+    (fun x _ ↦ ⟨IsSeparable.isIntegral' x, splits_codomain _ (IsSeparable.separable K x)⟩)
+
+end IsSepClosed
+
+namespace IsSepClosure
+
+variable (K : Type u) [Field K] (L : Type v) (M : Type w) [Field L] [Field M]
+variable [Algebra K M] [IsSepClosure K M]
+variable [Algebra K L] [IsSepClosure K L]
+
+/-- A (random) isomorphism between two separable closures of `K`. -/
+noncomputable def equiv : L ≃ₐ[K] M :=
+  -- Porting note: added to replace local instance above
+  haveI : IsSepClosed L := IsSepClosure.sep_closed K
+  haveI : IsSepClosed M := IsSepClosure.sep_closed K
+  AlgEquiv.ofBijective _ (Normal.isAlgebraic'.algHom_bijective₂
+    (IsSepClosed.lift : L →ₐ[K] M) (IsSepClosed.lift : M →ₐ[K] L)).1
+
+end IsSepClosure

Mathlib/RingTheory/Algebraic.lean

@@ -281,11 +281,11 @@ theorem Algebra.isAlgebraic_trans (L_alg : IsAlgebraic K L) (A_alg : IsAlgebraic
 
 end CommRing
 
-section Field
+section NoZeroSMulDivisors
 
-variable [Field K] [Field L]
+variable [CommRing K] [Field L]
 
-variable [Algebra K L]
+variable [Algebra K L] [NoZeroSMulDivisors K L]
 
 theorem Algebra.IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] L) :
     Function.Bijective f := by
@@ -309,14 +309,11 @@ theorem Algebra.IsAlgebraic.bijective_of_isScalarTower (ha : Algebra.IsAlgebraic
   (ha.algHom_bijective₂ (IsScalarTower.toAlgHom K L R) f).2
 
 theorem Algebra.IsAlgebraic.bijective_of_isScalarTower' [Field R] [Algebra K R]
+    [NoZeroSMulDivisors K R]
     (ha : Algebra.IsAlgebraic K R) [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) :
     Function.Bijective f :=
   (ha.algHom_bijective₂ f (IsScalarTower.toAlgHom K L R)).1
 
-theorem AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ :=
-  (Algebra.isAlgebraic_of_finite K L).algHom_bijective ϕ
-#align alg_hom.bijective AlgHom.bijective
-
 variable (K L)
 
 /-- Bijection between algebra equivalences and algebra homomorphisms -/
@@ -334,6 +331,20 @@ noncomputable def Algebra.IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebr
   map_mul' _ _ := rfl
 #align algebra.is_algebraic.alg_equiv_equiv_alg_hom Algebra.IsAlgebraic.algEquivEquivAlgHom
 
+end NoZeroSMulDivisors
+
+section Field
+
+variable [Field K] [Field L]
+
+variable [Algebra K L]
+
+theorem AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ :=
+  (Algebra.isAlgebraic_of_finite K L).algHom_bijective ϕ
+#align alg_hom.bijective AlgHom.bijective
+
+variable (K L)
+
 /-- Bijection between algebra equivalences and algebra homomorphisms -/
 @[reducible]
 noncomputable def algEquivEquivAlgHom [FiniteDimensional K L] :