Abelian categories have homology

In this file, it is shown that all short complexes S in abelian categories have terms of type S.HomologyData.

The strategy of the proof is to study the morphism kernel.ι S.g ≫ cokernel.π S.f. We show that there is a LeftHomologyData for S for which the H field consists of the coimage of kernel.ι S.g ≫ cokernel.π S.f, while there is a RightHomologyData for which the H is the image of kernel.ι S.g ≫ cokernel.π S.f. The fact that these left and right homology data are compatible (i.e. provide a HomologyData) is obtained by using the coimage-image isomorphism in abelian categories.

We also provide a constructor HomologyData.ofEpiMonoFactorisation which takes as an input an epi-mono factorization kf.pt ⟶ H ⟶ cc.pt of kf.ι ≫ cc.π where kf is a limit kernel fork of S.g and cc is a limit cokernel cofork of S.f.

noncomputable def CategoryTheory.ShortComplex.abelianImageToKernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Abelian.image S.f ⟶ Limits.kernel S.g

The canonical morphism Abelian.image S.f ⟶ kernel S.g for a short complex S in an abelian category.

@[simp]

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp S.abelianImageToKernel (Limits.kernel.ι S.g) = Abelian.image.ι S.f

@[simp]

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : S.X₂ ⟶ Z) : CategoryStruct.comp S.abelianImageToKernel (CategoryStruct.comp (Limits.kernel.ι S.g) h) = CategoryStruct.comp (Abelian.image.ι S.f) h

instance CategoryTheory.ShortComplex.instMonoAbelianImageToKernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Mono S.abelianImageToKernel

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp S.abelianImageToKernel (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)) = 0

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : Limits.cokernel S.f ⟶ Z) : CategoryStruct.comp S.abelianImageToKernel (CategoryStruct.comp (Limits.kernel.ι S.g) (CategoryStruct.comp (Limits.cokernel.π S.f) h)) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.ShortComplex.abelianImageToKernelIsKernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Limits.IsLimit (Limits.KernelFork.ofι S.abelianImageToKernel ⋯)

Abelian.image S.f is the kernel of kernel.ι S.g ≫ cokernel.π S.f

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.LeftHomologyData

The canonical LeftHomologyData of a short complex S in an abelian category, for which the H field is Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f).

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).π = Limits.cokernel.π (Limits.kernel.ι (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)))

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).K = Limits.kernel S.g

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).i = Limits.kernel.ι S.g

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).H = Abelian.coimage (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f))

noncomputable def CategoryTheory.ShortComplex.cokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Limits.cokernel S.f ⟶ Abelian.coimage S.g

The canonical morphism cokernel S.f ⟶ Abelian.coimage S.g for a short complex S in an abelian category.

@[simp]

theorem CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp (Limits.cokernel.π S.f) S.cokernelToAbelianCoimage = Abelian.coimage.π S.g

@[simp]

theorem CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : Abelian.coimage S.g ⟶ Z) : CategoryStruct.comp (Limits.cokernel.π S.f) (CategoryStruct.comp S.cokernelToAbelianCoimage h) = CategoryStruct.comp (Abelian.coimage.π S.g) h

instance CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Epi S.cokernelToAbelianCoimage

theorem CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)) S.cokernelToAbelianCoimage = 0

noncomputable def CategoryTheory.ShortComplex.cokernelToAbelianCoimageIsCokernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Limits.IsColimit (Limits.CokernelCofork.ofπ S.cokernelToAbelianCoimage ⋯)

Abelian.coimage S.g is the cokernel of kernel.ι S.g ≫ cokernel.π S.f

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofAbelian {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.RightHomologyData

The canonical RightHomologyData of a short complex S in an abelian category, for which the H field is Abelian.image (kernel.ι S.g ≫ cokernel.π S.f).

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).H = Abelian.image (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f))

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).p = Limits.cokernel.π S.f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).ι = Limits.kernel.ι (Limits.cokernel.π (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)))

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).Q = Limits.cokernel S.f

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofAbelian {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.HomologyData

The canonical HomologyData of a short complex S in an abelian category.

instance CategoryTheory.categoryWithHomology_of_abelian {C : Type u} [Category.{v, u} C] [Abelian C] : CategoryWithHomology C

instance CategoryTheory.ShortComplex.instIsNormalMonoCategory {C : Type u} [Category.{v, u} C] [Abelian C] : IsNormalMonoCategory (ShortComplex C)

instance CategoryTheory.ShortComplex.instIsNormalEpiCategory {C : Type u} [Category.{v, u} C] [Abelian C] : IsNormalEpiCategory (ShortComplex C)

noncomputable instance CategoryTheory.ShortComplex.instAbelian {C : Type u} [Category.{v, u} C] [Abelian C] : Abelian (ShortComplex C)

noncomputable def CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.homology ≅ Limits.image (CategoryStruct.comp S.iCycles S.pOpcycles)

The homology of a short complex S in an abelian category identifies to the image of S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles.

@[simp]

theorem CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom (Limits.image.ι (CategoryStruct.comp S.iCycles S.pOpcycles)) = S.homologyι

@[simp]

theorem CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : S.opcycles ⟶ Z) : CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom (CategoryStruct.comp (Limits.image.ι (CategoryStruct.comp S.iCycles S.pOpcycles)) h) = CategoryStruct.comp S.homologyι h

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : H ≅ Limits.image (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.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : CategoryStruct.comp (isoImage S hkf hcc fac).hom (Limits.image.ι (CategoryStruct.comp S.iCycles S.pOpcycles)) = CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] {Z : C} (h : S.opcycles ⟶ Z) : CategoryStruct.comp (isoImage S hkf hcc fac).hom (CategoryStruct.comp (Limits.image.ι (CategoryStruct.comp S.iCycles S.pOpcycles)) h) = CategoryStruct.comp ι (CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [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.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : CategoryStruct.comp π (isoHomology S hkf hcc fac).hom = CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom S.homologyπ

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] {Z : C} (h : S.homology ⟶ Z) : CategoryStruct.comp π (CategoryStruct.comp (isoHomology S hkf hcc fac).hom h) = CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom (CategoryStruct.comp S.homologyπ h)

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : CategoryStruct.comp (isoHomology S hkf hcc fac).inv ι = CategoryStruct.comp S.homologyι (S.isoOpcyclesOfIsColimit hcc).inv

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] {Z : C} (h : cc.pt ⟶ Z) : CategoryStruct.comp (isoHomology S hkf hcc fac).inv (CategoryStruct.comp ι h) = CategoryStruct.comp S.homologyι (CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).inv h)

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} (hkf : Limits.IsLimit kf) : hkf.lift (Limits.KernelFork.ofι S.f ⋯) = CategoryStruct.comp S.toCycles (S.isoCyclesOfIsLimit hkf).inv

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {cc : Limits.CokernelCofork S.f} (hcc : Limits.IsColimit cc) : hcc.desc (Limits.CokernelCofork.ofπ S.g ⋯) = CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom S.fromOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : CategoryStruct.comp S.homologyπ (isoHomology S hkf hcc fac).inv = CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv π

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] {Z : C} (h : H ⟶ Z) : CategoryStruct.comp S.homologyπ (CategoryStruct.comp (isoHomology S hkf hcc fac).inv h) = CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv (CategoryStruct.comp π h)

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : CategoryStruct.comp (isoHomology S hkf hcc fac).hom S.homologyι = CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] {Z : C} (h : S.opcycles ⟶ Z) : CategoryStruct.comp (isoHomology S hkf hcc fac).hom (CategoryStruct.comp S.homologyι h) = CategoryStruct.comp ι (CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : S.LeftHomologyData

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. This is the left homology data expressing H as the homology of S.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_H {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (leftHomologyData S hkf hcc fac).H = H

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_K {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (leftHomologyData S hkf hcc fac).K = kf.pt

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_i {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (leftHomologyData S hkf hcc fac).i = Limits.Fork.ι kf

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_π {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (leftHomologyData S hkf hcc fac).π = π

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : S.RightHomologyData

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. This is the right homology data expressing H as the homology of S.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_p {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (rightHomologyData S hkf hcc fac).p = Limits.Cofork.π cc

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_H {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (rightHomologyData S hkf hcc fac).H = H

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (rightHomologyData S hkf hcc fac).ι = ι

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_Q {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (rightHomologyData S hkf hcc fac).Q = cc.pt

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : S.HomologyData

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. This is the homology data expressing H as the homology of S.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_right {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (ofEpiMonoFactorisation S hkf hcc fac).right = ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_iso {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (ofEpiMonoFactorisation S hkf hcc fac).iso = Iso.refl (ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).H

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_left {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {kf : Limits.KernelFork S.g} {cc : Limits.CokernelCofork S.f} (hkf : Limits.IsLimit kf) (hcc : Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryStruct.comp (Limits.Fork.ι kf) (Limits.Cofork.π cc) = CategoryStruct.comp π ι) [Epi π] [Mono ι] : (ofEpiMonoFactorisation S hkf hcc fac).left = ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac