Theorems · Definition · category theory

CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        {kf : CategoryTheory.Limits.KernelFork S.g} →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} →
            CategoryTheory.Limits.IsLimit kf →
              CategoryTheory.Limits.IsColimit cc →
                {H : C} →
                  {π : kf.pt ⟶ H} →
                    {ι : H ⟶ cc.pt} →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
                            (CategoryTheory.Limits.Cofork.π cc) =
                          CategoryTheory.CategoryStruct.comp π ι →
                        [CategoryTheory.Epi π] → [CategoryTheory.Mono ι] → H ≅ S.homology

Let S be a short complex in an abelian category. Let kf be a limit kernel fork of S.g and cc a limit cokernel cofork of S.f. Let kf.pt ⟶ H ⟶ cc.pt be an epi-mono factorization of kf.ι ≫ cc.π : kf.pt ⟶ cc.pt, then H identifies to the homology of S.

Defined in

Mathlib.Algebra.Homology.ShortComplex.Abelian

Cited by

9 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.EpiCategoryTheory.Mono