English
An algebra is formally smooth if and only if its H1Cotangent module is projective and the subsingleton condition on H1Cotangent is satisfied; this connects to the projectivity of Ω[S/R] and the injectivity of kerCotangentToTensor.
Русский
Алгебра формально гладкая тогда и только тогда, когда модуль H1Cotangent является проективным, и выполнено условие подмножества на H1Cotangent; это соединяет проективность Ω[S/R] и инъективность kerCotangentToTensor.
LaTeX
$$$\\text{Algebra.FormallySmooth } R S \\iff (\\text{Subsingleton } \\mathrm{H1Cotangent}\\; R S) \\land (\\mathrm{Module.Projective}\\ S \\Omega[S/R])$$$
Lean4
/-- An algebra is formally smooth if and only if `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective.
-/
@[stacks 031J]
theorem 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)
change Function.Injective (Generators.self R S).toExtension.cotangentComplex ↔ _
rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
simp [H1Cotangent, Extension.H1Cotangent]
