exact_iff_i_p_zero — Mathlib

English

Let h be a HomologyData; S is exact iff the composite h.left.i ≫ h.right.p is zero.

Русский

Пусть h — данные гомологии; S точен тогда, когда композиция h.left.i ≫ h.right.p равна нулю.

LaTeX

$$$\\mathrm{Exact}(S) \\iff h.left.i \\circ h.right.p = 0$$$

Lean4

theorem exact_iff_i_p_zero (h : S.HomologyData) : S.Exact ↔ h.left.i ≫ h.right.p = 0 :=
  by
  haveI := HasHomology.mk' h
  rw [h.left.exact_iff, ← h.comm]
  constructor
  · intro z
    rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]
  · intro eq
    simp only [IsZero.iff_id_eq_zero, ← cancel_mono h.iso.hom, id_comp, ← cancel_mono h.right.ι, ← cancel_epi h.left.π,
      eq, zero_comp, comp_zero]

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