feat(RingTheory/Smooth): Correspondence between square-zero lifts and…

… retractions of the conormal sequence. (#14138)

Co-authored-by: Andrew Yang <[email protected]>

Mathlib.lean

@@ -3912,6 +3912,7 @@ import Mathlib.RingTheory.RootsOfUnity.Lemmas
 import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.SimpleModule
 import Mathlib.RingTheory.Smooth.Basic
+import Mathlib.RingTheory.Smooth.Kaehler
 import Mathlib.RingTheory.Smooth.StandardSmooth
 import Mathlib.RingTheory.Support
 import Mathlib.RingTheory.SurjectiveOnStalks

Mathlib/RingTheory/Ideal/Cotangent.lean

@@ -98,6 +98,16 @@ theorem to_quotient_square_comp_toCotangent :
 theorem toCotangent_to_quotient_square (x : I) :
     I.cotangentToQuotientSquare (I.toCotangent x) = (I ^ 2).mkQ x := rfl
 
+lemma Cotangent.smul_eq_zero_of_mem {I : Ideal R}
+    {x} (hx : x ∈ I) (m : I.Cotangent) : x • m = 0 := by
+  obtain ⟨m, rfl⟩ := Ideal.toCotangent_surjective _ m
+  rw [← map_smul, Ideal.toCotangent_eq_zero, pow_two]
+  exact Ideal.mul_mem_mul hx m.2
+
+lemma isTorsionBySet_cotangent :
+    Module.IsTorsionBySet R I.Cotangent I :=
+  fun m x ↦ m.smul_eq_zero_of_mem x.2
+
 /-- `I ⧸ I ^ 2` as an ideal of `R ⧸ I ^ 2`. -/
 def cotangentIdeal (I : Ideal R) : Ideal (R ⧸ I ^ 2) :=
   Submodule.map (Quotient.mk (I ^ 2)|>.toSemilinearMap) I
@@ -163,6 +173,14 @@ theorem _root_.AlgHom.ker_kerSquareLift (f : A →ₐ[R] B) :
   · intro x hx; obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x; exact ⟨x, hx, rfl⟩
   · rintro _ ⟨x, hx, rfl⟩; exact hx
 
+instance Algebra.kerSquareLift : Algebra (R ⧸ (RingHom.ker (algebraMap R A) ^ 2)) A :=
+  (Algebra.ofId R A).kerSquareLift.toAlgebra
+
+instance [Algebra A B] [IsScalarTower R A B] :
+    IsScalarTower R (A ⧸ (RingHom.ker (algebraMap A B) ^ 2)) B :=
+  IsScalarTower.of_algebraMap_eq'
+    (IsScalarTower.toAlgHom R A B).kerSquareLift.comp_algebraMap.symm
+
 /-- The quotient ring of `I ⧸ I ^ 2` is `R ⧸ I`. -/
 def quotCotangent : (R ⧸ I ^ 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I := by
   refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_

Mathlib/RingTheory/Smooth/Kaehler.lean

@@ -0,0 +1,210 @@
+/-
+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
+
+/-!
+# Relation of smoothness and `Ω[S⁄R]`
+
+## Main results
+
+- `retractionKerToTensorEquivSection`:
+  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`.
+
+## 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).
+
+-/
+
+universe u
+
+open TensorProduct KaehlerDifferential
+
+open Function (Surjective)
+
+variable {R P S : Type u} [CommRing R] [CommRing P] [CommRing S]
+variable [Algebra R S] [Algebra R P] [Algebra P S] [IsScalarTower R P S]
+variable (hf : Surjective (algebraMap P S)) (hf' : (RingHom.ker (algebraMap P S)) ^ 2 = ⊥)
+
+section ofSection
+
+-- Suppose we have a section (as alghom) of `P →ₐ[R] S`.
+variable (g : S →ₐ[R] P) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S)
+
+/--
+Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
+and a section `g : S →ₐ[R] P` (as an algebra homomorphism),
+we get an `R`-derivation `P → I` via `x ↦ x - g (f x)`.
+-/
+@[simps]
+def derivationOfSectionOfKerSqZero (f : P →ₐ[R] S) (hf' : (RingHom.ker f) ^ 2 = ⊥) (g : S →ₐ[R] P)
+    (hg : f.comp g = AlgHom.id R S) : Derivation R P (RingHom.ker f) where
+  toFun x := ⟨x - g (f x), by
+    simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f x)⟩
+  map_add' x y := by simp only [map_add, AddSubmonoid.mk_add_mk, Subtype.mk.injEq]; ring
+  map_smul' x y := by
+    ext
+    simp only [Algebra.smul_def, _root_.map_mul, ← IsScalarTower.algebraMap_apply,
+      AlgHom.commutes, RingHom.id_apply, Submodule.coe_smul_of_tower]
+    ring
+  map_one_eq_zero' := by simp only [LinearMap.coe_mk, AddHom.coe_mk, _root_.map_one, sub_self,
+    AddSubmonoid.mk_eq_zero]
+  leibniz' a b := by
+    have : (a - g (f a)) * (b - g (f b)) = 0 := by
+      rw [← Ideal.mem_bot, ← hf', pow_two]
+      apply Ideal.mul_mem_mul
+      · simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f a)
+      · simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f b)
+    ext
+    rw [← sub_eq_zero]
+    conv_rhs => rw [← neg_zero, ← this]
+    simp only [LinearMap.coe_mk, AddHom.coe_mk, _root_.map_mul, SetLike.mk_smul_mk, smul_eq_mul,
+      mul_sub, AddSubmonoid.mk_add_mk, sub_mul, neg_sub]
+    ring
+
+lemma isScalarTower_of_section_of_ker_sqZero :
+    letI := g.toRingHom.toAlgebra; IsScalarTower P S (RingHom.ker (algebraMap P S)) := by
+  letI := g.toRingHom.toAlgebra
+  constructor
+  intro p s m
+  ext
+  show g (p • s) * m = p * (g s * m)
+  simp only [Algebra.smul_def, _root_.map_mul, mul_assoc, mul_left_comm _ (g s)]
+  congr 1
+  rw [← sub_eq_zero, ← Ideal.mem_bot, ← hf', pow_two, ← sub_mul]
+  refine Ideal.mul_mem_mul ?_ m.2
+  simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg (algebraMap P S p)
+
+/--
+Given a surjective algebra hom `f : P →ₐ[R] S` with square-zero kernel `I`,
+and a section `g : S →ₐ[R] P` (as algebra homs),
+we get a retraction of the injection `I → S ⊗[P] Ω[P/R]`.
+-/
+noncomputable
+def retractionOfSectionOfKerSqZero : S ⊗[P] Ω[P⁄R] →ₗ[P] RingHom.ker (algebraMap P S) :=
+  letI := g.toRingHom.toAlgebra
+  haveI := isScalarTower_of_section_of_ker_sqZero hf' g hg
+  letI f : _ →ₗ[P] RingHom.ker (algebraMap P S) := (derivationOfSectionOfKerSqZero
+    (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential
+  (f.liftBaseChange S).restrictScalars P
+
+@[simp]
+lemma retractionOfSectionOfKerSqZero_tmul_D (s : S) (t : P) :
+    retractionOfSectionOfKerSqZero hf' g hg (s ⊗ₜ .D _ _ t) =
+      g s * t - g s * g (algebraMap _ _ t) := by
+  letI := g.toRingHom.toAlgebra
+  haveI := isScalarTower_of_section_of_ker_sqZero hf' g hg
+  simp only [retractionOfSectionOfKerSqZero, AlgHom.toRingHom_eq_coe, LinearMap.coe_restrictScalars,
+    LinearMap.liftBaseChange_tmul, SetLike.val_smul_of_tower]
+  erw [Derivation.liftKaehlerDifferential_comp_D]
+  exact mul_sub (g s) t (g (algebraMap P S t))
+
+lemma retractionOfSectionOfKerSqZero_comp_kerToTensor :
+    (retractionOfSectionOfKerSqZero hf' g hg).comp (kerToTensor R P S) = LinearMap.id := by
+  ext x; simp [(RingHom.mem_ker _).mp x.2]
+
+end ofSection
+
+section ofRetraction
+
+variable (l : S ⊗[P] Ω[P⁄R] →ₗ[P] RingHom.ker (algebraMap P S))
+variable (hl : l.comp (kerToTensor R P S) = LinearMap.id)
+
+-- suppose we have a (set-theoretic) section
+variable (σ : S → P) (hσ : ∀ x, algebraMap P S (σ x) = x)
+
+lemma sectionOfRetractionKerToTensorAux_prop (x y) (h : algebraMap P S x = algebraMap P S y) :
+    x - l (1 ⊗ₜ .D _ _ x) = y - l (1 ⊗ₜ .D _ _ y) := by
+  rw [sub_eq_iff_eq_add, sub_add_comm, ← sub_eq_iff_eq_add, ← Submodule.coe_sub,
+    ← map_sub, ← tmul_sub, ← map_sub]
+  exact congr_arg Subtype.val (LinearMap.congr_fun hl.symm ⟨x - y, by simp [RingHom.mem_ker, h]⟩)
+
+/--
+Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.
+Let `σ` be an arbitrary (set-theoretic) section of `f`.
+Suppose we have a retraction `l` of the injection `I →ₗ[P] S ⊗[P] Ω[P/R]`, then
+`x ↦ σ x - l (1 ⊗ D (σ x))` is an algebra homomorphism and a section to `f`.
+-/
+noncomputable
+def sectionOfRetractionKerToTensorAux : S →ₐ[R] P where
+  toFun x := σ x - l (1 ⊗ₜ .D _ _ (σ x))
+  map_one' := by simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 1) 1 (by simp [hσ])]
+  map_mul' a b := by
+    have (x y) : (l x).1 * (l y).1 = 0 := by
+      rw [← Ideal.mem_bot, ← hf', pow_two]; exact Ideal.mul_mem_mul (l x).2 (l y).2
+    simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a * b)) (σ a * σ b) (by simp [hσ]),
+      Derivation.leibniz, tmul_add, tmul_smul, map_add, map_smul, AddSubmonoid.coe_add, this,
+      Submodule.coe_toAddSubmonoid, SetLike.val_smul, smul_eq_mul, mul_sub, sub_mul, sub_zero]
+    ring
+  map_add' a b := by
+    simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a + b)) (σ a + σ b) (by simp [hσ]),
+      map_add, tmul_add, AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid, add_sub_add_comm]
+  map_zero' := by simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 0) 0 (by simp [hσ])]
+  commutes' r := by
+    simp [sectionOfRetractionKerToTensorAux_prop l hl
+      (σ (algebraMap R S r)) (algebraMap R P r) (by simp [hσ, ← IsScalarTower.algebraMap_apply])]
+
+lemma sectionOfRetractionKerToTensorAux_algebraMap (x : P) :
+    sectionOfRetractionKerToTensorAux hf' l hl σ hσ (algebraMap P S x) = x - l (1 ⊗ₜ .D _ _ x) :=
+  sectionOfRetractionKerToTensorAux_prop l hl _ x (by simp [hσ])
+
+lemma toAlgHom_comp_sectionOfRetractionKerToTensorAux :
+    (IsScalarTower.toAlgHom R P S).comp
+      (sectionOfRetractionKerToTensorAux hf' l hl σ hσ) = AlgHom.id _ _ := by
+  ext x
+  obtain ⟨x, rfl⟩ := hf x
+  simp [sectionOfRetractionKerToTensorAux_algebraMap, (RingHom.mem_ker _).mp]
+
+/--
+Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.
+Suppose we have a retraction `l` of the injection `I →ₗ[P] S ⊗[P] Ω[P/R]`, then
+`x ↦ σ x - l (1 ⊗ D (σ x))` is an algebra homomorphism and a section to `f`,
+where `σ` is an arbitrary (set-theoretic) section of `f`
+-/
+noncomputable def sectionOfRetractionKerToTensor : S →ₐ[R] P :=
+  sectionOfRetractionKerToTensorAux hf' l hl _ (fun x ↦ (hf x).choose_spec)
+
+@[simp]
+lemma sectionOfRetractionKerToTensor_algebraMap (x : P) :
+    sectionOfRetractionKerToTensor hf hf' l hl (algebraMap P S x) = x - l (1 ⊗ₜ .D _ _ x) :=
+  sectionOfRetractionKerToTensorAux_algebraMap hf' l hl _ _ x
+
+@[simp]
+lemma toAlgHom_comp_sectionOfRetractionKerToTensor :
+    (IsScalarTower.toAlgHom R P S).comp
+      (sectionOfRetractionKerToTensor hf hf' l hl) = AlgHom.id _ _ :=
+  toAlgHom_comp_sectionOfRetractionKerToTensorAux hf _ _ _ _ _
+
+end ofRetraction
+
+/--
+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`.
+-/
+noncomputable
+def retractionKerToTensorEquivSection :
+    { l // l ∘ₗ (kerToTensor R P S) = LinearMap.id } ≃
+      { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S } where
+  toFun l := ⟨_, toAlgHom_comp_sectionOfRetractionKerToTensor hf hf' _ l.2⟩
+  invFun g := ⟨_, retractionOfSectionOfKerSqZero_comp_kerToTensor hf' _ g.2⟩
+  left_inv l := by
+    ext s p
+    obtain ⟨s, rfl⟩ := hf s
+    have (x y) : (l.1 x).1 * (l.1 y).1 = 0 := by
+      rw [← Ideal.mem_bot, ← hf', pow_two]; exact Ideal.mul_mem_mul (l.1 x).2 (l.1 y).2
+    simp only [AlgebraTensorModule.curry_apply,
+      Derivation.coe_comp, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Derivation.coeFn_coe,
+      Function.comp_apply, curry_apply, retractionOfSectionOfKerSqZero_tmul_D,
+      sectionOfRetractionKerToTensor_algebraMap, ← mul_sub, sub_sub_cancel]
+    rw [sub_mul]
+    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