exact₀ — Mathlib

English

For any morphism f, the short complex obtained from composing with f and its differential is exact.

Русский

Для любого морфизма f полученная короткая точная последовательность из композиции с f и ее дифференциалом эксемна.

LaTeX

$$$\forall f:X\to Y,\; (ShortComplex.mk (d f) f (by simp)).Exact$$$

Lean4

theorem exact₀ {Z : C} (P : ProjectiveResolution Z) : (ShortComplex.mk _ _ P.complex_d_comp_π_f_zero).Exact :=
  ShortComplex.exact_of_g_is_cokernel _ P.isColimitCokernelCofork

Похожие утверждения