[Merged by Bors] - feat(RingTheory): classification of etale algebras over fields

Mathlib.lean

@@ -4361,6 +4361,7 @@ import Mathlib.RingTheory.EisensteinCriterion
 import Mathlib.RingTheory.EssentialFiniteness
 import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.Etale.Field
+import Mathlib.RingTheory.Etale.Pi
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Extension
 import Mathlib.RingTheory.Filtration

Mathlib/RingTheory/Etale/Field.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.RingTheory.Etale.Basic
+import Mathlib.RingTheory.Etale.Pi
 import Mathlib.RingTheory.Unramified.Field
 
 /-!
@@ -14,9 +14,14 @@ import Mathlib.RingTheory.Unramified.Field
 Let `K` be a field, `A` be a `K`-algebra and `L` be a field extension of `K`.
 
 - `Algebra.FormallyEtale.of_isSeparable`:
-    If `L` is separable over `K`, then `L` is formally etale over `K`.
+    If `L` is separable over `K`, then `L` is formally étale over `K`.
 - `Algebra.FormallyEtale.iff_isSeparable`:
-    If `L` is (essentially) of finite type over `K`, then `L/K` is etale iff `L/K` is separable.
+    If `L` is (essentially) of finite type over `K`, then `L/K` is étale iff `L/K` is separable.
+- `Algebra.FormallyEtale.iff_exists_algEquiv_prod`:
+    If `A` is (essentially) of finite type over `K`,
+    then `A/K` is étale iff `A` is a finite product of separable field extensions.
+- `Algebra.Etale.iff_exists_algEquiv_prod`:
+    `A/K` is étale iff `A` is a finite product of finite separable field extensions.
 
 ## References
 
@@ -27,7 +32,7 @@ Let `K` be a field, `A` be a `K`-algebra and `L` be a field extension of `K`.
 
 universe u
 
-variable (K L : Type u) [Field K] [Field L] [Algebra K L]
+variable (K L A : Type u) [Field K] [Field L] [CommRing A] [Algebra K L] [Algebra K A]
 
 open Algebra Polynomial
 
@@ -148,4 +153,61 @@ theorem iff_isSeparable [EssFiniteType K L] :
     FormallyEtale K L ↔ Algebra.IsSeparable K L :=
   ⟨fun _ ↦ FormallyUnramified.isSeparable K L, fun _ ↦ of_isSeparable K L⟩
 
+attribute [local instance]
+  IsArtinianRing.subtype_isMaximal_finite IsArtinianRing.fieldOfSubtypeIsMaximal in
+/--
+If `A` is an essentially of finite type algebra over a field `K`, then `A` is formally étale
+over `K` if and only if `A` is a finite product of separable field extensions.
+-/
+theorem iff_exists_algEquiv_prod [EssFiniteType K A] :
+    FormallyEtale K A ↔
+      ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (_ : ∀ i, Field (Ai i))
+        (_ : ∀ i, Algebra K (Ai i)) (_ : A ≃ₐ[K] Π i, Ai i),
+        ∀ i, Algebra.IsSeparable K (Ai i) := by
+  classical
+  constructor
+  · intro H
+    have := FormallyUnramified.finite_of_free K A
+    have := FormallyUnramified.isReduced_of_field K A
+    have : IsArtinianRing A := isArtinian_of_tower K inferInstance
+    letI : Fintype {I : Ideal A | I.IsMaximal} := (nonempty_fintype _).some
+    let v (i : {I : Ideal A | I.IsMaximal}) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)
+    let e : A ≃ₐ[K] _ := { __ := IsArtinianRing.equivPi A, commutes' := fun r ↦ rfl }
+    have := (FormallyEtale.iff_of_equiv e).mp inferInstance
+    rw [FormallyEtale.pi_iff] at this
+    exact ⟨_, inferInstance, _, _, _, e, fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩
+  · intro ⟨I, _, Ai, _, _, e, _⟩
+    rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]
+    have (i) : EssFiniteType K (Ai i) := by
+      letI := ((Pi.evalRingHom Ai i).comp e.toRingHom).toAlgebra
+      have : IsScalarTower K A (Ai i) :=
+        .of_algebraMap_eq fun r ↦ by simp [RingHom.algebraMap_toAlgebra]
+      have : Algebra.FiniteType A (Ai i) := .of_surjective inferInstance (Algebra.ofId _ _)
+        (RingHomSurjective.is_surjective (σ := Pi.evalRingHom Ai i).comp e.surjective)
+      exact EssFiniteType.comp K A (Ai i)
+    exact fun I ↦ (iff_isSeparable _ _).mpr inferInstance
+
 end Algebra.FormallyEtale
+
+attribute [local instance]
+  IsArtinianRing.subtype_isMaximal_finite IsArtinianRing.fieldOfSubtypeIsMaximal in
+/--
+`A` is étale over a field `K` if and only if
+`A` is a finite product of finite separable field extensions.
+-/
+theorem Algebra.Etale.iff_exists_algEquiv_prod :
+    Etale K A ↔
+      ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (_ : ∀ i, Field (Ai i))
+        (_ : ∀ i, Algebra K (Ai i)) (_ : A ≃ₐ[K] Π i, Ai i),
+        ∀ i, Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i) := by
+  constructor
+  · intro H
+    obtain ⟨I, _, Ai, _, _, e, _⟩ := (FormallyEtale.iff_exists_algEquiv_prod K A).mp inferInstance
+    have := FormallyUnramified.finite_of_free K A
+    exact ⟨_, ‹_›, _, _, _, e, fun i ↦ ⟨.of_surjective ((LinearMap.proj i).comp e.toLinearMap)
+      ((Function.surjective_eval i).comp e.surjective), inferInstance⟩⟩
+  · intro ⟨I, _, Ai, _, _, e, H⟩
+    choose h₁ h₂ using H
+    have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective
+    refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩
+    exact (FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩

Mathlib/RingTheory/Etale/Pi.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.Smooth.Pi
+import Mathlib.RingTheory.Unramified.Pi
+import Mathlib.RingTheory.Etale.Basic
+
+/-!
+
+# Formal-étaleness of finite products of rings
+
+## Main result
+
+- `Algebra.FormallyEtale.pi_iff`: If `I` is finite, `Π i : I, A i` is `R`-formally-étale
+  if and only if each `A i` is `R`-formally-étale.
+
+-/
+
+universe u v
+
+namespace Algebra.FormallyEtale
+
+variable {R : Type (max u v)} {I : Type u} (A : I → Type (max u v))
+variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
+
+theorem pi_iff [Finite I] :
+    FormallyEtale R (Π i, A i) ↔ ∀ i, FormallyEtale R (A i) := by
+  simp_rw [FormallyEtale.iff_unramified_and_smooth, forall_and]
+  rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]
+
+instance [Finite I] [∀ i, FormallyEtale R (A i)] : FormallyEtale R (Π i, A i) :=
+  .of_unramified_and_smooth
+
+end Algebra.FormallyEtale

Mathlib/RingTheory/Smooth/Pi.lean

@@ -118,4 +118,7 @@ theorem pi_iff [Finite I] :
       rwa [mul_sub, ← map_mul, mul_comm, mul_assoc, (he.idem i).eq, he', ← map_mul, ← Pi.single_mul,
         one_mul, sub_eq_zero] at this
 
+instance [Finite I] [∀ i, FormallySmooth R (A i)] : FormallySmooth R (Π i, A i) :=
+  (pi_iff _).mpr ‹_›
+
 end Algebra.FormallySmooth

Mathlib/RingTheory/Unramified/Pi.lean

@@ -95,4 +95,7 @@ theorem pi_iff :
         Ideal.Quotient.mkₐ_eq_mk]
       exact Ideal.mem_map_of_mem (Ideal.Quotient.mk J') (hf (Pi.single x r))
 
+instance [∀ i, FormallyUnramified R (f i)] : FormallyUnramified R (Π i, f i) :=
+  (pi_iff _).mpr ‹_›
+
 end Algebra.FormallyUnramified