Documentation

Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Functors which preserves homology #

If F : C ⥤ D is a functor between categories with zero morphisms, we shall say that F preserves homology when F preserves both kernels and cokernels. This typeclass is named [F.PreservesHomology], and is automatically satisfied when F preserves both finite limits and finite colimits.

TODO: If S : ShortComplex C and [F.PreservesHomology], then there is an isomorphism S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology.

A functor preserves homology when it preserves both kernels and cokernels.

Instances

    A left homology data h of a short complex S is preserved by a functor F is F preserves the kernel of S.g : S.X₂ ⟶ S.X₃ and the cokernel of h.f' : S.X₁ ⟶ h.K.

    Instances