English
The Jacobi–Zariski connecting morphism δ is exact with the base-change map, expressing that H1Cotangent maps into T ⊗S Ω[S/R] with kernel equal to the image of δ, yielding a precise exactness relation under base-change.
Русский
Соединяющее отображение δ образует точную последовательность вместе с отображением базового изменения, т.е. ядро отображения базового изменения равно образу δ.
LaTeX
$$$\\operatorname{Im}(\\delta) = \\ker(\\mathrm{mapBaseChange}_{R,S,T}).$$$
Lean4
/-- Given algebras `R → S → T`, `H¹(L_{T/R}) → H¹(L_{T/S}) → T ⊗[S] Ω[S/R]` is exact. -/
theorem exact_map_δ : Function.Exact (map R S T T) (δ R S T) :=
Generators.H1Cotangent.exact_map_δ' (Generators.self S T) (Generators.self R S) (Generators.self R T)
(Generators.defaultHom _ _)
