English
There is a well-defined map homInfinitesimal that assigns to two extensions P1, P2 a homomorphism between their infinitesimal extensions, compatible with the formal smoothness assumption and the tower R ⊂ P ⊂ S. The construction is functorial in P1, P2.
Русский
Существует задание homInfinitesimal, которое при двух расширениях P1, P2 дает гомоморфизм между их инфинитезимальным расширениям, совместимый с предположением формальной гладкости и цепочкой R ⊂ P ⊂ S. Конструкция функториальна по P1, P2.
LaTeX
$$$\\mathrm{homInfinitesimal}(P_1,P_2) : P_1.infinitesimal.Hom P_2.infinitesimal$$$
Lean4
/-- 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.
Also see `Algebra.Extension.formallySmooth_iff_split_injection`
for the version in terms of `Extension`.
-/
@[stacks 031I]
theorem iff_split_injection : Algebra.FormallySmooth R S ↔ ∃ l, l ∘ₗ (kerCotangentToTensor R P S) = LinearMap.id :=
by
have := (retractionKerCotangentToTensorEquivSection (R := R) hf).nonempty_congr
simp only [nonempty_subtype] at this
rw [this, ← Algebra.FormallySmooth.iff_split_surjection _ hf]
