# 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.

class CategoryTheory.Functor.PreservesHomology {C : Type u_1} {D : Type u_2} [] [] (F : ) :
Type (max (max (max u_1 u_2) u_3) u_4)
• preservesKernels : X Y : C⦄ → (f : X Y) →

the functor preserves kernels

• preservesCokernels : X Y : C⦄ → (f : X Y) →

the functor preserves cokernels

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

Instances
def CategoryTheory.Functor.PreservesHomology.preservesKernel {C : Type u_1} {D : Type u_2} [] [] (F : ) {X : C} {Y : C} (f : X Y) :

A functor which preserves homology preserves kernels.

Instances For
def CategoryTheory.Functor.PreservesHomology.preservesCokernel {C : Type u_1} {D : Type u_2} [] [] (F : ) {X : C} {Y : C} (f : X Y) :

A functor which preserves homology preserves cokernels.

Instances For
class CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy {C : Type u_1} {D : Type u_2} [] [] {S : } (F : ) :
Type (max (max (max u_1 u_2) u_3) u_4)
• the functor preserves the kernel of S.g : S.X₂ ⟶ S.X₃.

• the functor preserves the cokernel of h.f' : S.X₁ ⟶ h.K.

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

When a left homology data is preserved by a functor F, this functor preserves the kernel of S.g : S.X₂ ⟶ S.X₃.

Instances For

When a left homology data h is preserved by a functor F, this functor preserves the cokernel of h.f' : S.X₁ ⟶ h.K.

Instances For
@[simp]
@[simp]
@[simp]
@[simp]

When a left homology data h of a short complex S is preserved by a functor F, this is the induced left homology data h.map F for the short complex S.map F.

Instances For
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH {C : Type u_1} {D : Type u_2} [] [] {S₁ : } {S₂ : } {φ : S₁ S₂} (ψ : ) (F : ) :
= F.map ψ.φH
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK {C : Type u_1} {D : Type u_2} [] [] {S₁ : } {S₂ : } {φ : S₁ S₂} (ψ : ) (F : ) :
= F.map ψ.φK

Given a left homology map data ψ : LeftHomologyMapData φ h₁ h₂ such that both left homology data h₁ and h₂ are preserved by a functor F, this is the induced left homology map data for the morphism F.mapShortComplex.map φ.

Instances For