Homology classes under a functor preserving homology

For a functor F preserving the left homology of a short complex S, Mathlib identifies the cycles and the homology of S.map F with the images under F of those of S, by ShortComplex.mapCyclesIso and ShortComplex.mapHomologyIso, and records how the first of them interacts with the inclusion of the cycles (ShortComplex.mapCyclesIso_hom_iCycles). This file records the companion statement for the class map: under the two identifications, the class map homologyπ of S.map F is the image under F of the class map of S (ShortComplex.homologyπ_comp_mapHomologyIso_hom).

This is what makes a homology class computed after applying F recognisable as the image of a class before applying it, for instance when a connecting map is constructed in an abelian category after forgetting structure from a non-abelian one.

@[simp]

theorem CategoryTheory.ShortComplex.mapCyclesIso_inv_comp_iCycles {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (S : ShortComplex C) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] : CategoryStruct.comp (S.mapCyclesIso F).inv (S.map F).iCycles = F.map S.iCycles

The inverse cycles identification carries the inclusion of cycles in the mapped complex to the image of the original inclusion.

@[simp]

theorem CategoryTheory.ShortComplex.mapCyclesIso_inv_comp_iCycles_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (S : ShortComplex C) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] {Z : D} (h : (S.map F).X₂ ⟶ Z) : CategoryStruct.comp (S.mapCyclesIso F).inv (CategoryStruct.comp (S.map F).iCycles h) = CategoryStruct.comp (F.map S.iCycles) h

The inverse cycles identification carries the inclusion of cycles in the mapped complex to the image of the original inclusion.

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_comp_mapHomologyIso_hom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (S : ShortComplex C) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] : CategoryStruct.comp (S.map F).homologyπ (S.mapHomologyIso F).hom = CategoryStruct.comp (S.mapCyclesIso F).hom (F.map S.homologyπ)

The class map commutes with a functor preserving homology. Under the identifications mapCyclesIso and mapHomologyIso, the class map of S.map F is the image under F of the class map of S.

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_comp_mapHomologyIso_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (S : ShortComplex C) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] {Z : D} (h : F.obj S.homology ⟶ Z) : CategoryStruct.comp (S.map F).homologyπ (CategoryStruct.comp (S.mapHomologyIso F).hom h) = CategoryStruct.comp (S.mapCyclesIso F).hom (CategoryStruct.comp (F.map S.homologyπ) h)

The class map commutes with a functor preserving homology. Under the identifications mapCyclesIso and mapHomologyIso, the class map of S.map F is the image under F of the class map of S.