exact_of_g_is_cokernel — Mathlib

English

Cokernel-based condition yields exactness.

Русский

Условие через cokernel даёт точность.

LaTeX

$$$ IsColimit(CokernelCofork.ofπ S.g S.zero) \\Rightarrow S.Exact $$$

Lean4

theorem exact_of_g_is_cokernel (hS : IsColimit (CokernelCofork.ofπ S.g S.zero)) [S.HasHomology] : S.Exact :=
  by
  rw [exact_iff_mono_fromOpcycles]
  have : IsSplitMono S.fromOpcycles :=
    ⟨⟨{   retraction := hS.desc (CokernelCofork.ofπ S.pOpcycles S.f_pOpcycles)
          id := by
            rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
            exact Cofork.IsColimit.π_desc hS }⟩⟩
  infer_instance

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