feat(RingTheory): Jacobian criterion for smoothness of local algebras

Mathlib.lean

@@ -4631,6 +4631,7 @@ import Mathlib.RingTheory.SimpleRing.Field
 import Mathlib.RingTheory.SimpleRing.Matrix
 import Mathlib.RingTheory.Smooth.Basic
 import Mathlib.RingTheory.Smooth.Kaehler
+import Mathlib.RingTheory.Smooth.Local
 import Mathlib.RingTheory.Smooth.Pi
 import Mathlib.RingTheory.Smooth.StandardSmooth
 import Mathlib.RingTheory.Support

Mathlib/RingTheory/Smooth/Kaehler.lean

@@ -388,6 +388,26 @@ theorem Algebra.FormallySmooth.iff_split_injection :
   simp only [nonempty_subtype] at this
   rw [this, ← Algebra.FormallySmooth.iff_split_surjection _ hf]
 
+/--
+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'
+    (P : Algebra.Extension.{u} R S) [FormallySmooth R P.Ring] :
+    Algebra.FormallySmooth R S ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id := by
+  refine (Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_
+  let e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
+    { __ := AddEquiv.refl _, map_smul' r m := by ext1; simp; rfl }
+  constructor
+  · intro ⟨l, hl⟩
+    exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
+      LinearMap.ext (DFunLike.congr_fun hl : _)⟩
+  · intro ⟨l, hl⟩
+    exact ⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring,
+      LinearMap.ext (DFunLike.congr_fun hl : _)⟩
+
 include hf in
 /--
 Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`

Mathlib/RingTheory/Smooth/Local.lean

@@ -0,0 +1,37 @@
+/-
+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.LocalRing.Module
+import Mathlib.RingTheory.Smooth.Kaehler
+import Mathlib.RingTheory.TensorProduct.Free
+
+/-!
+# Formally smooth local algebras
+-/
+
+open TensorProduct IsLocalRing KaehlerDifferential
+
+/--
+The **Jacobian criterion** for smoothness of local algebras.
+Suppose `S` is a local `R`-algebra, and `0 → I → P → S → 0` be a presentation such that
+`P` is formally-smooth over `R`, `Ω[P⁄R]` is finite free over `P`,
+(typically satisfied when `P` is the localization of a polynomial ring of finite type)
+and `I` is finitely generated.
+Then `S` is formally smooth iff `k ⊗ₛ I/I² → k ⊗ₚ Ω[P/R]` is injective,
+where `k` is the residue field of `S`.
+-/
+theorem Algebra.FormallySmooth.iff_injective_lTensor_residueField {R S} [CommRing R]
+    [CommRing S] [IsLocalRing S] [Algebra R S] (P : Algebra.Extension R S)
+    [FormallySmooth R P.Ring]
+    [Module.Free P.Ring (Ω[P.Ring⁄R])] [Module.Finite P.Ring (Ω[P.Ring⁄R])]
+    (h' : P.ker.FG) :
+    Algebra.FormallySmooth R S ↔
+        Function.Injective (P.cotangentComplex.lTensor (ResidueField S)) := by
+  have : Module.Finite P.Ring P.Cotangent :=
+    have : Module.Finite P.Ring P.ker := ⟨(Submodule.fg_top _).mpr h'⟩
+    .of_surjective _ Extension.Cotangent.mk_surjective
+  have : Module.Finite S P.Cotangent := Module.Finite.of_restrictScalars_finite P.Ring _ _
+  rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
+    Algebra.FormallySmooth.iff_split_injection' P]