exact_iff_epi — Mathlib

English

The exactness of S.unop is equivalent to the exactness of S.

Русский

Точность S.unop эквивалентна точности S.

LaTeX

$$$ S.unop.Exact \\iff S.Exact $$$

Lean4

theorem exact_iff_epi [HasZeroObject C] (hg : S.g = 0) : S.Exact ↔ Epi S.f :=
  by
  constructor
  · intro h
    have := h.hasHomology
    simp only [exact_iff_isZero_homology] at h
    haveI := S.isIso_iCycles hg
    haveI : Epi S.toCycles := epi_of_isZero_cokernel' _ S.homologyIsCokernel h
    rw [← S.toCycles_i]
    apply epi_comp
  · intro
    rw [(HomologyData.ofIsColimitCokernelCofork S hg _
          (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (0 : S.X₂ ⟶ 0) comp_zero) inferInstance
            (isZero_zero C))).exact_iff]
    exact isZero_zero C

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