Theorems · Theorem · commutative algebra

Algebra.Extension.formallySmooth_iff_split_injection

∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (P : Algebra.Extension R A)
  [Algebra.FormallySmooth R P.Ring], Algebra.FormallySmooth R A ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

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.

Defined in

Mathlib.RingTheory.Smooth.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.FormallySmooth