Theorems · Theorem · commutative algebra

Algebra.FormallySmooth.iff_injective_lTensor_residueField

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : Algebra R S] (P : Algebra.Extension R S) [Algebra.FormallySmooth R P.Ring] [Module.Free P.Ring Ω[P.Ring⁄R]]
  [Module.Finite P.Ring Ω[P.Ring⁄R]],
  P.ker.FG →
    (Algebra.FormallySmooth R S ↔
      Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField S) P.cotangentComplex))

The Jacobian criterion for smoothness of local algebras. Suppose S is a local R-algebra, and 0 → I → P → S → 0 is 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.

Defined in

Mathlib.RingTheory.Smooth.Local

Cited by

1 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingIsLocalRingAlgebraAlgebra.FormallySmoothModule.FreeModule.Finite