feat(RingTheory/Smooth): formally smooth iff H¹(L_{R/S}) = 0 and Ω_{S/R} is projective (#17905)

Author: erdOne

Mathlib/RingTheory/Smooth/Kaehler.lean

@@ -3,7 +3,10 @@ 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.Kaehler.Basic
+import Mathlib.RingTheory.Kaehler.CotangentComplex
+import Mathlib.RingTheory.Smooth.Basic
+import Mathlib.Algebra.Module.Projective
+import Mathlib.Tactic.StacksAttribute
 
 /-!
 # Relation of smoothness and `Ω[S⁄R]`
@@ -14,13 +17,32 @@ import Mathlib.RingTheory.Kaehler.Basic
   Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
   there is a one-to-one correspondence between `P`-linear retractions of `I →ₗ[P] S ⊗[P] Ω[P/R]`
   and algebra homomorphism sections of `f`.
+- `retractionKerCotangentToTensorEquivSection`:
+  Given a surjective algebra homomorphism `f : P →ₐ[R] S` with kernel `I`,
+  there is a one-to-one correspondence between `P`-linear retractions of `I/I² →ₗ[P] S ⊗[P] Ω[P/R]`
+  and algebra homomorphism sections of `f‾ : P/I² → S`.
+- `Algebra.FormallySmooth.iff_split_injection`:
+  Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
+  with kernel `I` (typically a presentation `R[X] → S`),
+  `S` is formally smooth iff the `P`-linear map `I/I² → S ⊗[P] Ω[P⁄R]` is split injective.
+- `Algebra.FormallySmooth.iff_injective_and_projective`:
+  Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
+  with kernel `I` (typically a presentation `R[X] → S`),
+  then `S` is formally smooth iff `Ω[S/R]` is projective and `I/I² → S ⊗[P] Ω[P⁄R]` is injective.
+- `Algebra.FormallySmooth.iff_subsingleton_and_projective`:
+  An algebra is formally smooth if and only if `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective.
 
 ## Future projects
 
-- Show that relative smooth iff `H¹(L_{S/R}) = 0` and `Ω[S/R]` is projective.
 - Show that being smooth is local on stalks.
 - Show that being formally smooth is Zariski-local (very hard).
 
+## References
+
+- https://stacks.math.columbia.edu/tag/00TH
+- [B. Iversen, *Generic Local Structure of the Morphisms in Commutative Algebra*][iversen]
+
+
 -/
 
 universe u
@@ -198,7 +220,6 @@ end ofRetraction
 
 variable [Algebra R S] [IsScalarTower R P S]
 variable (hf' : (RingHom.ker (algebraMap P S)) ^ 2 = ⊥) (hf : Surjective (algebraMap P S))
-include hf' hf
 
 /--
 Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
@@ -224,3 +245,205 @@ def retractionKerToTensorEquivSection :
     simp only [this, Algebra.algebraMap_eq_smul_one, ← smul_tmul', LinearMapClass.map_smul,
       SetLike.val_smul, smul_eq_mul, sub_zero]
   right_inv g := by ext s; obtain ⟨s, rfl⟩ := hf s; simp
+
+variable (R P S) in
+/--
+Given a tower of algebras `S/P/R`, with `I = ker(P → S)`,
+this is the `R`-derivative `P/I² → S ⊗[P] Ω[P⁄R]` given by `[x] ↦ 1 ⊗ D x`.
+-/
+noncomputable
+def derivationQuotKerSq :
+    Derivation R (P ⧸ (RingHom.ker (algebraMap P S) ^ 2)) (S ⊗[P] Ω[P⁄R]) := by
+  letI := Submodule.liftQ ((RingHom.ker (algebraMap P S) ^ 2).restrictScalars R)
+    (((mk P S _ 1).restrictScalars R).comp (KaehlerDifferential.D R P).toLinearMap)
+  refine ⟨this ?_, ?_, ?_⟩
+  · rintro x hx
+    simp only [Submodule.restrictScalars_mem, pow_two] at hx
+    simp only [LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
+      Derivation.coeFn_coe, Function.comp_apply, mk_apply]
+    refine Submodule.smul_induction_on hx ?_ ?_
+    · intro x hx y hy
+      simp only [smul_eq_mul, Derivation.leibniz, tmul_add, ← smul_tmul, Algebra.smul_def,
+        mul_one, RingHom.mem_ker.mp hx, RingHom.mem_ker.mp hy, zero_tmul, zero_add]
+    · intro x y hx hy; simp only [map_add, hx, hy, tmul_add, zero_add]
+  · show (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0; simp
+  · intro a b
+    obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective _ a
+    obtain ⟨b, rfl⟩ := Submodule.Quotient.mk_surjective _ b
+    show (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P (a * b) =
+      Ideal.Quotient.mk _ a • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P b) +
+      Ideal.Quotient.mk _ b • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P a)
+    simp only [← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul,
+      Derivation.leibniz, tmul_add, tmul_smul]
+
+@[simp]
+lemma derivationQuotKerSq_mk (x : P) :
+    derivationQuotKerSq R P S x = 1 ⊗ₜ .D R P x := rfl
+
+variable (R P S) in
+/--
+Given a tower of algebras `S/P/R`, with `I = ker(P → S)` and `Q := P/I²`,
+there is an isomorphism of `S`-modules `S ⊗[Q] Ω[Q/R] ≃ S ⊗[P] Ω[P/R]`.
+-/
+noncomputable
+def tensorKaehlerQuotKerSqEquiv :
+    S ⊗[P ⧸ (RingHom.ker (algebraMap P S) ^ 2)] Ω[(P ⧸ (RingHom.ker (algebraMap P S) ^ 2))⁄R] ≃ₗ[S]
+      S ⊗[P] Ω[P⁄R] :=
+  letI f₁ := (derivationQuotKerSq R P S).liftKaehlerDifferential
+  letI f₂ := AlgebraTensorModule.lift ((LinearMap.ringLmapEquivSelf S S _).symm f₁)
+  letI f₃ := KaehlerDifferential.map R R P (P ⧸ (RingHom.ker (algebraMap P S) ^ 2))
+  letI f₄ := ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S _ 1).restrictScalars P).comp f₃
+  letI f₅ := AlgebraTensorModule.lift ((LinearMap.ringLmapEquivSelf S S _).symm f₄)
+  { __ := f₂
+    invFun := f₅
+    left_inv := by
+      suffices f₅.comp f₂ = LinearMap.id from LinearMap.congr_fun this
+      ext a
+      obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a
+      simp [f₁, f₂, f₃, f₄, f₅]
+    right_inv := by
+      suffices f₂.comp f₅ = LinearMap.id from LinearMap.congr_fun this
+      ext a
+      simp [f₁, f₂, f₃, f₄, f₅] }
+
+@[simp]
+lemma tensorKaehlerQuotKerSqEquiv_tmul_D (s t) :
+    tensorKaehlerQuotKerSqEquiv R P S (s ⊗ₜ .D _ _ (Ideal.Quotient.mk _ t)) = s ⊗ₜ .D _ _ t := by
+  show s • (derivationQuotKerSq R P S).liftKaehlerDifferential (.D _ _ (Ideal.Quotient.mk _ t)) = _
+  simp [smul_tmul']
+
+@[simp]
+lemma tensorKaehlerQuotKerSqEquiv_symm_tmul_D (s t) :
+    (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ .D _ _ t) =
+      s ⊗ₜ .D _ _ (Ideal.Quotient.mk _ t) := by
+  apply (tensorKaehlerQuotKerSqEquiv R P S).injective
+  simp
+
+/--
+Given a surjective algebra homomorphism `f : P →ₐ[R] S` with kernel `I`,
+there is a one-to-one correspondence between `P`-linear retractions of `I/I² →ₗ[P] S ⊗[P] Ω[P/R]`
+and algebra homomorphism sections of `f‾ : P/I² → S`.
+-/
+noncomputable
+def retractionKerCotangentToTensorEquivSection :
+    { l // l ∘ₗ (kerCotangentToTensor R P S) = LinearMap.id } ≃
+      { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S } := by
+  let P' := P ⧸ (RingHom.ker (algebraMap P S) ^ 2)
+  have h₁ : Surjective (algebraMap P' S) := Function.Surjective.of_comp (g := algebraMap P P') hf
+  have h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥ := by
+    rw [RingHom.algebraMap_toAlgebra, AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
+  let e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] (RingHom.ker (algebraMap P' S)) :=
+    (Ideal.cotangentEquivIdeal _).trans ((LinearEquiv.ofEq _ _
+      (IsScalarTower.toAlgHom R P S).ker_kerSquareLift.symm).restrictScalars P)
+  let e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] :=
+    (tensorKaehlerQuotKerSqEquiv R P S).restrictScalars P
+  have H : kerCotangentToTensor R P S =
+      e₂.toLinearMap ∘ₗ (kerToTensor R P' S ).restrictScalars P ∘ₗ e₁.toLinearMap := by
+    ext x
+    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
+    exact (tensorKaehlerQuotKerSqEquiv_tmul_D 1 x.1).symm
+  refine Equiv.trans ?_ (retractionKerToTensorEquivSection (R := R) h₂ h₁)
+  refine ⟨fun ⟨l, hl⟩ ↦ ⟨⟨(e₁.toLinearMap ∘ₗ l ∘ₗ e₂.toLinearMap).toAddMonoidHom, ?_⟩, ?_⟩,
+    fun ⟨l, hl⟩ ↦ ⟨e₁.symm.toLinearMap ∘ₗ l.restrictScalars P ∘ₗ e₂.symm.toLinearMap, ?_⟩, ?_, ?_⟩
+  · rintro x y
+    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+    simp only [← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul]
+    exact (e₁.toLinearMap ∘ₗ l ∘ₗ e₂.toLinearMap).map_smul x y
+  · ext1 x
+    rw [H] at hl
+    obtain ⟨x, rfl⟩ := e₁.surjective x
+    exact DFunLike.congr_arg e₁ (LinearMap.congr_fun hl x)
+  · ext x
+    rw [H]
+    apply e₁.injective
+    simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_restrictScalars,
+      Function.comp_apply, LinearEquiv.symm_apply_apply, LinearMap.id_coe, id_eq,
+      LinearEquiv.apply_symm_apply]
+    exact LinearMap.congr_fun hl (e₁ x)
+  · intro f
+    ext x
+    simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
+      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
+      LinearEquiv.coe_coe, LinearMap.coe_mk, AddHom.coe_coe, LinearMap.toAddMonoidHom_coe,
+      LinearEquiv.apply_symm_apply, LinearEquiv.symm_apply_apply]
+  · intro f
+    ext x
+    simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
+      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
+      LinearMap.coe_mk, AddHom.coe_coe, LinearMap.toAddMonoidHom_coe, LinearEquiv.coe_coe,
+      LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply]
+
+variable [Algebra.FormallySmooth R P]
+
+include hf in
+/--
+Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
+with kernel `I` (typically a presentation `R[X] → S`),
+`S` is formally smooth iff the `P`-linear map `I/I² → S ⊗[P] Ω[P⁄R]` is split injective.
+-/
+@[stacks 031I]
+theorem Algebra.FormallySmooth.iff_split_injection :
+    Algebra.FormallySmooth R S ↔ ∃ l, l ∘ₗ (kerCotangentToTensor R P S) = LinearMap.id := by
+  have := (retractionKerCotangentToTensorEquivSection (R := R) hf).nonempty_congr
+  simp only [nonempty_subtype] at this
+  rw [this, ← Algebra.FormallySmooth.iff_split_surjection _ hf]
+
+include hf in
+/--
+Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
+with kernel `I` (typically a presentation `R[X] → S`),
+then `S` is formally smooth iff `I/I² → S ⊗[P] Ω[S⁄R]` is injective and
+`S ⊗[P] Ω[P⁄R] → Ω[S⁄R]` is split surjective.
+-/
+theorem Algebra.FormallySmooth.iff_injective_and_split :
+    Algebra.FormallySmooth R S ↔ Function.Injective (kerCotangentToTensor R P S) ∧
+      ∃ l, (KaehlerDifferential.mapBaseChange R P S) ∘ₗ l = LinearMap.id := by
+  rw [Algebra.FormallySmooth.iff_split_injection hf]
+  refine (and_iff_right (KaehlerDifferential.mapBaseChange_surjective R _ _ hf)).symm.trans ?_
+  refine Iff.trans (((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae'
+    (g := (KaehlerDifferential.mapBaseChange R P S).restrictScalars P)).out 1 0)
+    (and_congr Iff.rfl ?_)
+  rw [(LinearMap.extendScalarsOfSurjectiveEquiv hf).surjective.exists]
+  simp only [LinearMap.ext_iff, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
+    Function.comp_apply, LinearMap.extendScalarsOfSurjective_apply, LinearMap.id_coe, id_eq]
+
+private theorem Algebra.FormallySmooth.iff_injective_and_projective' :
+    letI : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
+    Algebra.FormallySmooth R S ↔
+        Function.Injective (kerCotangentToTensor R (MvPolynomial S R) S) ∧
+        Module.Projective S (Ω[S⁄R]) := by
+  letI : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
+  have : Function.Surjective (algebraMap (MvPolynomial S R) S) :=
+    fun x ↦ ⟨.X x, MvPolynomial.aeval_X _ _⟩
+  rw [Algebra.FormallySmooth.iff_injective_and_split this,
+    ← Module.Projective.iff_split_of_projective]
+  exact KaehlerDifferential.mapBaseChange_surjective _ _ _ this
+
+instance : Module.Projective P (Ω[P⁄R]) :=
+  (Algebra.FormallySmooth.iff_injective_and_projective'.mp ‹_›).2
+
+include hf in
+/--
+Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
+with kernel `I` (typically a presentation `R[X] → S`),
+then `S` is formally smooth iff `I/I² → S ⊗[P] Ω[P⁄R]` is injective and `Ω[S/R]` is projective.
+-/
+theorem Algebra.FormallySmooth.iff_injective_and_projective :
+    Algebra.FormallySmooth R S ↔
+        Function.Injective (kerCotangentToTensor R P S) ∧ Module.Projective S (Ω[S⁄R]) := by
+  rw [Algebra.FormallySmooth.iff_injective_and_split hf,
+    ← Module.Projective.iff_split_of_projective]
+  exact KaehlerDifferential.mapBaseChange_surjective _ _ _ hf
+
+/--
+An algebra is formally smooth if and only if `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective.
+-/
+@[stacks 031J]
+theorem Algebra.FormallySmooth.iff_subsingleton_and_projective :
+    Algebra.FormallySmooth R S ↔
+        Subsingleton (Algebra.H1Cotangent R S) ∧ Module.Projective S (Ω[S⁄R]) := by
+  refine (Algebra.FormallySmooth.iff_injective_and_projective
+    (Generators.self R S).algebraMap_surjective).trans (and_congr ?_ Iff.rfl)
+  show Function.Injective (Generators.self R S).cotangentComplex ↔ _
+  rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
+  rfl

scripts/noshake.json

@@ -311,6 +311,7 @@
   "Mathlib.Tactic.Attr.Register": ["Lean.Meta.Tactic.Simp.SimpTheorems"],
   "Mathlib.Tactic.ArithMult": ["Mathlib.Tactic.ArithMult.Init"],
   "Mathlib.Tactic.Algebraize": ["Mathlib.Algebra.Algebra.Tower"],
+  "Mathlib.RingTheory.Smooth.Kaehler": ["Mathlib.Tactic.StacksAttribute"],
   "Mathlib.RingTheory.PowerSeries.Basic":
   ["Mathlib.Algebra.CharP.Defs", "Mathlib.Tactic.MoveAdd"],
   "Mathlib.RingTheory.PolynomialAlgebra": ["Mathlib.Data.Matrix.DMatrix"],