Theorems · Definition · category theory

CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage

{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 ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)

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 image of S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles.

Defined in

Mathlib.Algebra.Homology.ShortComplex.Abelian

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.EpiCategoryTheory.Mono