isZero_X₂ — Mathlib

English

If an exact short complex S has vanishing f and g maps, then X₂ is a zero object.

Русский

Если точное короткое комплекс S имеет нулевые модули f и g, то X₂ является нулевым объектом.

LaTeX

$$$ \text{IsZero } S.X_2 \quad \text{given } S.Exact, \; S.f = 0, \; S.g = 0 $$$

Lean4

theorem isZero_X₂ (hS : S.Exact) (hf : S.f = 0) (hg : S.g = 0) : IsZero S.X₂ :=
  by
  have := hS.mono_g hf
  rw [IsZero.iff_id_eq_zero, ← cancel_mono S.g, hg, comp_zero, comp_zero]

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