exact_iff_mono_cokernel_desc — Mathlib

English

Exactness is detected by a mono cokernel-desc map.

Русский

Точность определяется моно-описателем cokernel.

LaTeX

$$$ S.Exact \\iff \\operatorname{Mono}(\\operatorname{cokernel.desc}(S.f,S.g,S.zero)) $$$

Lean4

theorem exact_iff_mono_cokernel_desc [S.HasHomology] [HasCokernel S.f] :
    S.Exact ↔ Mono (cokernel.desc S.f S.g S.zero) :=
  by
  rw [exact_iff_mono_fromOpcycles]
  refine (MorphismProperty.monomorphisms C).arrow_mk_iso_iff (Iso.symm ?_)
  exact Arrow.isoMk S.opcyclesIsoCokernel.symm (Iso.refl _) (by cat_disch)

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