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.

If S : ShortComplex C and [F.PreservesHomology], then there is an isomorphism S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology, which is part of the natural isomorphism homologyFunctorIso F between the functors F.mapShortComplex ⋙ homologyFunctor D and homologyFunctor C ⋙ F.

class CategoryTheory.Functor.PreservesHomology {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] (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

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

• preservesKernels ⦃X Y : C⦄ (f : X ⟶ Y) : Limits.PreservesLimit (Limits.parallelPair f 0) F

  the functor preserves kernels

• preservesCokernels ⦃X Y : C⦄ (f : X ⟶ Y) : Limits.PreservesColimit (Limits.parallelPair f 0) F

  the functor preserves cokernels

theorem CategoryTheory.Functor.PreservesHomology.preservesKernel {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] (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesHomology] {X Y : C} (f : X ⟶ Y) : Limits.PreservesLimit (Limits.parallelPair f 0) F

A functor which preserves homology preserves kernels.

theorem CategoryTheory.Functor.PreservesHomology.preservesCokernel {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] (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesHomology] {X Y : C} (f : X ⟶ Y) : Limits.PreservesColimit (Limits.parallelPair f 0) F

A functor which preserves homology preserves cokernels.

instance CategoryTheory.Functor.preservesHomologyOfExact {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] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : F.PreservesHomology

class CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

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.

• g : Limits.PreservesLimit (Limits.parallelPair S.g 0) F

  the functor preserves the kernel of S.g : S.X₂ ⟶ S.X₃.

• f' : Limits.PreservesColimit (Limits.parallelPair h.f' 0) F

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

instance CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preservesHomology {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesHomology] : h.IsPreservedBy F

theorem CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : Limits.PreservesLimit (Limits.parallelPair S.g 0) F

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

theorem CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf' {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : Limits.PreservesColimit (Limits.parallelPair h.f' 0) F

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

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.map {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (S.map F).LeftHomologyData

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_H {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).H = F.obj h.H

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_i {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).i = F.map h.i

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_π {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).π = F.map h.π

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_K {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} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).K = F.obj h.K

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_f' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).f' = F.map h.f'

noncomputable def CategoryTheory.ShortComplex.LeftHomologyMapData.map {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] : LeftHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

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

Equations

• ψ.map F = { φK := F.map ψ.φK, φH := F.map ψ.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] : (ψ.map F).φH = F.map ψ.φH

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] : (ψ.map F).φK = F.map ψ.φK

class CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

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

• f : Limits.PreservesColimit (Limits.parallelPair S.f 0) F

  the functor preserves the cokernel of S.f : S.X₁ ⟶ S.X₂.

• g' : Limits.PreservesLimit (Limits.parallelPair h.g' 0) F

  the functor preserves the kernel of h.g' : h.Q ⟶ S.X₃.

instance CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preservesHomology {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesHomology] : h.IsPreservedBy F

theorem CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : Limits.PreservesColimit (Limits.parallelPair S.f 0) F

When a right homology data is preserved by a functor F, this functor preserves the cokernel of S.f : S.X₁ ⟶ S.X₂.

theorem CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg' {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : Limits.PreservesLimit (Limits.parallelPair h.g' 0) F

When a right homology data h is preserved by a functor F, this functor preserves the kernel of h.g' : h.Q ⟶ S.X₃.

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.map {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (S.map F).RightHomologyData

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.map_p {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).p = F.map h.p

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.map_Q {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).Q = F.obj h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.map_ι {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).ι = F.map h.ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.map_H {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} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).H = F.obj h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.map_g' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] : (h.map F).g' = F.map h.g'

noncomputable def CategoryTheory.ShortComplex.RightHomologyMapData.map {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] : RightHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

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

Equations

• ψ.map F = { φQ := F.map ψ.φQ, φH := F.map ψ.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] : (ψ.map F).φQ = F.map ψ.φQ

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.map_φH {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] : (ψ.map F).φH = F.map ψ.φH

noncomputable def CategoryTheory.ShortComplex.HomologyData.map {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} (h : S.HomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] : (S.map F).HomologyData

When a homology data h of a short complex S is such that both h.left and h.right are preserved by a functor F, this is the induced homology data h.map F for the short complex S.map F.

Equations

• h.map F = { left := h.left.map F, right := h.right.map F, iso := F.mapIso h.iso, comm := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.map_left {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} (h : S.HomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] : (h.map F).left = h.left.map F

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.map_iso {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} (h : S.HomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] : (h.map F).iso = F.mapIso h.iso

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.map_right {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} (h : S.HomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] : (h.map F).right = h.right.map F

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.map {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : HomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] : HomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

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

Equations

• ψ.map F = { left := ψ.left.map F, right := ψ.right.map F }

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.map_left {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : HomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] : (ψ.map F).left = ψ.left.map F

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.map_right {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₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : HomologyMapData φ h₁ h₂) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] : (ψ.map F).right = ψ.right.map F

theorem CategoryTheory.ShortComplex.map_leftRightHomologyComparison' {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] (hₗ : S.LeftHomologyData) (hᵣ : S.RightHomologyData) [hₗ.IsPreservedBy F] [hᵣ.IsPreservedBy F] : F.map (leftRightHomologyComparison' hₗ hᵣ) = leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)

class CategoryTheory.Functor.PreservesLeftHomologyOf {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) : Prop

A functor preserves the left homology of a short complex S if it preserves all the left homology data of S.

• isPreservedBy (h : S.LeftHomologyData) : h.IsPreservedBy F

  the functor preserves all the left homology data of the short complex

class CategoryTheory.Functor.PreservesRightHomologyOf {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) : Prop

A functor preserves the right homology of a short complex S if it preserves all the right homology data of S.

• isPreservedBy (h : S.RightHomologyData) : h.IsPreservedBy F

  the functor preserves all the right homology data of the short complex

instance CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) [F.PreservesHomology] : F.PreservesLeftHomologyOf S

instance CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) [F.PreservesHomology] : F.PreservesRightHomologyOf S

theorem CategoryTheory.Functor.PreservesLeftHomologyOf.mk' {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] (F : Functor C D) [F.PreservesZeroMorphisms] {S : ShortComplex C} (h : S.LeftHomologyData) [h.IsPreservedBy F] : F.PreservesLeftHomologyOf S

If a functor preserves a certain left homology data of a short complex S, then it preserves the left homology of S.

theorem CategoryTheory.Functor.PreservesRightHomologyOf.mk' {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] (F : Functor C D) [F.PreservesZeroMorphisms] {S : ShortComplex C} (h : S.RightHomologyData) [h.IsPreservedBy F] : F.PreservesRightHomologyOf S

If a functor preserves a certain right homology data of a short complex S, then it preserves the right homology of S.

instance CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves {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} (h₁ : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] : h₁.IsPreservedBy F

instance CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves {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} (h₂ : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] : h₂.IsPreservedBy F

instance CategoryTheory.ShortComplex.hasLeftHomology_of_preserves {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] : (S.map F).HasLeftHomology

instance CategoryTheory.ShortComplex.hasLeftHomology_of_preserves' {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] : (F.mapShortComplex.obj S).HasLeftHomology

instance CategoryTheory.ShortComplex.hasRightHomology_of_preserves {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.HasRightHomology] [F.PreservesRightHomologyOf S] : (S.map F).HasRightHomology

instance CategoryTheory.ShortComplex.hasRightHomology_of_preserves' {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.HasRightHomology] [F.PreservesRightHomologyOf S] : (F.mapShortComplex.obj S).HasRightHomology

instance CategoryTheory.ShortComplex.hasHomology_of_preserves {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] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] : (S.map F).HasHomology

instance CategoryTheory.ShortComplex.hasHomology_of_preserves' {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] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] : (F.mapShortComplex.obj S).HasHomology

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_cyclesMap' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F] : F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

theorem CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F] : F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

theorem CategoryTheory.ShortComplex.RightHomologyData.map_opcyclesMap' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hr₁ : S₁.RightHomologyData) (hr₂ : S₂.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] : F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

theorem CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hr₁ : S₁.RightHomologyData) (hr₂ : S₂.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] : F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

theorem CategoryTheory.ShortComplex.HomologyData.map_homologyMap' {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] : F.map (homologyMap' φ h₁ h₂) = homologyMap' (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

noncomputable def CategoryTheory.ShortComplex.mapCyclesIso {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] : (S.map F).cycles ≅ F.obj S.cycles

When a functor F preserves the left homology of a short complex S, this is the canonical isomorphism (S.map F).cycles ≅ F.obj S.cycles.

Equations

• S.mapCyclesIso F = (S.leftHomologyData.map F).cyclesIso

@[simp]

theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_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).hom (F.map S.iCycles) = (S.map F).iCycles

@[simp]

theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_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 : F.obj S.X₂ ⟶ Z) : CategoryStruct.comp (S.mapCyclesIso F).hom (CategoryStruct.comp (F.map S.iCycles) h) = CategoryStruct.comp (S.map F).iCycles h

noncomputable def CategoryTheory.ShortComplex.mapLeftHomologyIso {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] : (S.map F).leftHomology ≅ F.obj S.leftHomology

When a functor F preserves the left homology of a short complex S, this is the canonical isomorphism (S.map F).leftHomology ≅ F.obj S.leftHomology.

Equations

• S.mapLeftHomologyIso F = (S.leftHomologyData.map F).leftHomologyIso

noncomputable def CategoryTheory.ShortComplex.mapOpcyclesIso {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.HasRightHomology] [F.PreservesRightHomologyOf S] : (S.map F).opcycles ≅ F.obj S.opcycles

When a functor F preserves the right homology of a short complex S, this is the canonical isomorphism (S.map F).opcycles ≅ F.obj S.opcycles.

Equations

• S.mapOpcyclesIso F = (S.rightHomologyData.map F).opcyclesIso

noncomputable def CategoryTheory.ShortComplex.mapRightHomologyIso {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.HasRightHomology] [F.PreservesRightHomologyOf S] : (S.map F).rightHomology ≅ F.obj S.rightHomology

When a functor F preserves the right homology of a short complex S, this is the canonical isomorphism (S.map F).rightHomology ≅ F.obj S.rightHomology.

Equations

• S.mapRightHomologyIso F = (S.rightHomologyData.map F).rightHomologyIso

noncomputable def CategoryTheory.ShortComplex.mapHomologyIso {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] : (S.map F).homology ≅ F.obj S.homology

When a functor F preserves the left homology of a short complex S, this is the canonical isomorphism (S.map F).homology ≅ F.obj S.homology.

Equations

• S.mapHomologyIso F = (S.homologyData.left.map F).homologyIso

noncomputable def CategoryTheory.ShortComplex.mapHomologyIso' {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.PreservesRightHomologyOf S] : (S.map F).homology ≅ F.obj S.homology

When a functor F preserves the right homology of a short complex S, this is the canonical isomorphism (S.map F).homology ≅ F.obj S.homology.

Equations

• S.mapHomologyIso' F = (S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm

theorem CategoryTheory.ShortComplex.LeftHomologyData.mapCyclesIso_eq {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} (hl : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] : S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm

theorem CategoryTheory.ShortComplex.LeftHomologyData.mapLeftHomologyIso_eq {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} (hl : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] : S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm

theorem CategoryTheory.ShortComplex.RightHomologyData.mapOpcyclesIso_eq {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} (hr : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] : S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm

theorem CategoryTheory.ShortComplex.RightHomologyData.mapRightHomologyIso_eq {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} (hr : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] : S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm

theorem CategoryTheory.ShortComplex.LeftHomologyData.mapHomologyIso_eq {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} (hl : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] : S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm

theorem CategoryTheory.ShortComplex.RightHomologyData.mapHomologyIso'_eq {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} (hr : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesRightHomologyOf S] : S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm

theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] : CategoryStruct.comp (cyclesMap (F.mapShortComplex.map φ)) (S₂.mapCyclesIso F).hom = CategoryStruct.comp (S₁.mapCyclesIso F).hom (F.map (cyclesMap φ))

theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.cycles ⟶ Z) : CategoryStruct.comp (cyclesMap (F.mapShortComplex.map φ)) (CategoryStruct.comp (S₂.mapCyclesIso F).hom h) = CategoryStruct.comp (S₁.mapCyclesIso F).hom (CategoryStruct.comp (F.map (cyclesMap φ)) h)

theorem CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] : CategoryStruct.comp (F.map (cyclesMap φ)) (S₂.mapCyclesIso F).inv = CategoryStruct.comp (S₁.mapCyclesIso F).inv (cyclesMap (F.mapShortComplex.map φ))

theorem CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : (S₂.map F).cycles ⟶ Z) : CategoryStruct.comp (F.map (cyclesMap φ)) (CategoryStruct.comp (S₂.mapCyclesIso F).inv h) = CategoryStruct.comp (S₁.mapCyclesIso F).inv (CategoryStruct.comp (cyclesMap (F.mapShortComplex.map φ)) h)

theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] : CategoryStruct.comp (leftHomologyMap (F.mapShortComplex.map φ)) (S₂.mapLeftHomologyIso F).hom = CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom (F.map (leftHomologyMap φ))

theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.leftHomology ⟶ Z) : CategoryStruct.comp (leftHomologyMap (F.mapShortComplex.map φ)) (CategoryStruct.comp (S₂.mapLeftHomologyIso F).hom h) = CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom (CategoryStruct.comp (F.map (leftHomologyMap φ)) h)

theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] : CategoryStruct.comp (F.map (leftHomologyMap φ)) (S₂.mapLeftHomologyIso F).inv = CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv (leftHomologyMap (F.mapShortComplex.map φ))

theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : (S₂.map F).leftHomology ⟶ Z) : CategoryStruct.comp (F.map (leftHomologyMap φ)) (CategoryStruct.comp (S₂.mapLeftHomologyIso F).inv h) = CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv (CategoryStruct.comp (leftHomologyMap (F.mapShortComplex.map φ)) h)

theorem CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] : CategoryStruct.comp (opcyclesMap (F.mapShortComplex.map φ)) (S₂.mapOpcyclesIso F).hom = CategoryStruct.comp (S₁.mapOpcyclesIso F).hom (F.map (opcyclesMap φ))

theorem CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : F.obj S₂.opcycles ⟶ Z) : CategoryStruct.comp (opcyclesMap (F.mapShortComplex.map φ)) (CategoryStruct.comp (S₂.mapOpcyclesIso F).hom h) = CategoryStruct.comp (S₁.mapOpcyclesIso F).hom (CategoryStruct.comp (F.map (opcyclesMap φ)) h)

theorem CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] : CategoryStruct.comp (F.map (opcyclesMap φ)) (S₂.mapOpcyclesIso F).inv = CategoryStruct.comp (S₁.mapOpcyclesIso F).inv (opcyclesMap (F.mapShortComplex.map φ))

theorem CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : (S₂.map F).opcycles ⟶ Z) : CategoryStruct.comp (F.map (opcyclesMap φ)) (CategoryStruct.comp (S₂.mapOpcyclesIso F).inv h) = CategoryStruct.comp (S₁.mapOpcyclesIso F).inv (CategoryStruct.comp (opcyclesMap (F.mapShortComplex.map φ)) h)

theorem CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] : CategoryStruct.comp (rightHomologyMap (F.mapShortComplex.map φ)) (S₂.mapRightHomologyIso F).hom = CategoryStruct.comp (S₁.mapRightHomologyIso F).hom (F.map (rightHomologyMap φ))

theorem CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : F.obj S₂.rightHomology ⟶ Z) : CategoryStruct.comp (rightHomologyMap (F.mapShortComplex.map φ)) (CategoryStruct.comp (S₂.mapRightHomologyIso F).hom h) = CategoryStruct.comp (S₁.mapRightHomologyIso F).hom (CategoryStruct.comp (F.map (rightHomologyMap φ)) h)

theorem CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] : CategoryStruct.comp (F.map (rightHomologyMap φ)) (S₂.mapRightHomologyIso F).inv = CategoryStruct.comp (S₁.mapRightHomologyIso F).inv (rightHomologyMap (F.mapShortComplex.map φ))

theorem CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : (S₂.map F).rightHomology ⟶ Z) : CategoryStruct.comp (F.map (rightHomologyMap φ)) (CategoryStruct.comp (S₂.mapRightHomologyIso F).inv h) = CategoryStruct.comp (S₁.mapRightHomologyIso F).inv (CategoryStruct.comp (rightHomologyMap (F.mapShortComplex.map φ)) h)

theorem CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] : CategoryStruct.comp (homologyMap (F.mapShortComplex.map φ)) (S₂.mapHomologyIso F).hom = CategoryStruct.comp (S₁.mapHomologyIso F).hom (F.map (homologyMap φ))

theorem CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.homology ⟶ Z) : CategoryStruct.comp (homologyMap (F.mapShortComplex.map φ)) (CategoryStruct.comp (S₂.mapHomologyIso F).hom h) = CategoryStruct.comp (S₁.mapHomologyIso F).hom (CategoryStruct.comp (F.map (homologyMap φ)) h)

theorem CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] : CategoryStruct.comp (F.map (homologyMap φ)) (S₂.mapHomologyIso F).inv = CategoryStruct.comp (S₁.mapHomologyIso F).inv (homologyMap (F.mapShortComplex.map φ))

theorem CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : (S₂.map F).homology ⟶ Z) : CategoryStruct.comp (F.map (homologyMap φ)) (CategoryStruct.comp (S₂.mapHomologyIso F).inv h) = CategoryStruct.comp (S₁.mapHomologyIso F).inv (CategoryStruct.comp (homologyMap (F.mapShortComplex.map φ)) h)

theorem CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] : CategoryStruct.comp (homologyMap (F.mapShortComplex.map φ)) (S₂.mapHomologyIso' F).hom = CategoryStruct.comp (S₁.mapHomologyIso' F).hom (F.map (homologyMap φ))

theorem CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : F.obj S₂.homology ⟶ Z) : CategoryStruct.comp (homologyMap (F.mapShortComplex.map φ)) (CategoryStruct.comp (S₂.mapHomologyIso' F).hom h) = CategoryStruct.comp (S₁.mapHomologyIso' F).hom (CategoryStruct.comp (F.map (homologyMap φ)) h)

theorem CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality {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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] : CategoryStruct.comp (F.map (homologyMap φ)) (S₂.mapHomologyIso' F).inv = CategoryStruct.comp (S₁.mapHomologyIso' F).inv (homologyMap (F.mapShortComplex.map φ))

theorem CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality_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₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (F : Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : (S₂.map F).homology ⟶ Z) : CategoryStruct.comp (F.map (homologyMap φ)) (CategoryStruct.comp (S₂.mapHomologyIso' F).inv h) = CategoryStruct.comp (S₁.mapHomologyIso' F).inv (CategoryStruct.comp (homologyMap (F.mapShortComplex.map φ)) h)

theorem CategoryTheory.ShortComplex.mapHomologyIso'_eq_mapHomologyIso {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] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] : S.mapHomologyIso' F = S.mapHomologyIso F

noncomputable def CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F ⟶ G) : LeftHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)

Given a natural transformation τ : F ⟶ G between functors C ⥤ D which preserve the left homology of a short complex S, and a left homology data for S, this is the left homology map data for the morphism S.mapNatTrans τ obtained by evaluating τ.

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ = { φK := τ.app h.K, φH := τ.app h.H, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φH {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F ⟶ G) : (natTransApp h τ).φH = τ.app h.H

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φK {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F ⟶ G) : (natTransApp h τ).φK = τ.app h.K

noncomputable def CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F ⟶ G) : RightHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)

Given a natural transformation τ : F ⟶ G between functors C ⥤ D which preserve the right homology of a short complex S, and a right homology data for S, this is the right homology map data for the morphism S.mapNatTrans τ obtained by evaluating τ.

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ = { φQ := τ.app h.Q, φH := τ.app h.H, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φH {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F ⟶ G) : (natTransApp h τ).φH = τ.app h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φQ {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F ⟶ G) : (natTransApp h τ).φQ = τ.app h.Q

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.natTransApp {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F ⟶ G) : HomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)

Given a natural transformation τ : F ⟶ G between functors C ⥤ D which preserve the homology of a short complex S, and a homology data for S, this is the homology map data for the morphism S.mapNatTrans τ obtained by evaluating τ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F ⟶ G) : (natTransApp h τ).left = LeftHomologyMapData.natTransApp h.left τ

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F ⟶ G) : (natTransApp h τ).right = RightHomologyMapData.natTransApp h.right τ

theorem CategoryTheory.ShortComplex.homologyMap_mapNatTrans {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 G : Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] [S.HasHomology] (τ : F ⟶ G) : homologyMap (S.mapNatTrans τ) = CategoryStruct.comp (S.mapHomologyIso F).hom (CategoryStruct.comp (τ.app S.homology) (S.mapHomologyIso G).inv)

noncomputable def CategoryTheory.ShortComplex.cyclesFunctorIso {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] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels D] [Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (cyclesFunctor D) ≅ (cyclesFunctor C).comp F

The natural isomorphism F.mapShortComplex ⋙ cyclesFunctor D ≅ cyclesFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology.

Equations

• CategoryTheory.ShortComplex.cyclesFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapCyclesIso F) ⋯

noncomputable def CategoryTheory.ShortComplex.leftHomologyFunctorIso {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] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels D] [Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (leftHomologyFunctor D) ≅ (leftHomologyFunctor C).comp F

The natural isomorphism F.mapShortComplex ⋙ leftHomologyFunctor D ≅ leftHomologyFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology.

Equations

• CategoryTheory.ShortComplex.leftHomologyFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapLeftHomologyIso F) ⋯

noncomputable def CategoryTheory.ShortComplex.opcyclesFunctorIso {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] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels D] [Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (opcyclesFunctor D) ≅ (opcyclesFunctor C).comp F

The natural isomorphism F.mapShortComplex ⋙ opcyclesFunctor D ≅ opcyclesFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology.

Equations

• CategoryTheory.ShortComplex.opcyclesFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapOpcyclesIso F) ⋯

noncomputable def CategoryTheory.ShortComplex.rightHomologyFunctorIso {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] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels D] [Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (rightHomologyFunctor D) ≅ (rightHomologyFunctor C).comp F

The natural isomorphism F.mapShortComplex ⋙ rightHomologyFunctor D ≅ rightHomologyFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology.

Equations

• CategoryTheory.ShortComplex.rightHomologyFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapRightHomologyIso F) ⋯

noncomputable def CategoryTheory.ShortComplex.homologyFunctorIso {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] (F : Functor C D) [F.PreservesZeroMorphisms] [CategoryWithHomology C] [CategoryWithHomology D] [F.PreservesHomology] : F.mapShortComplex.comp (homologyFunctor D) ≅ (homologyFunctor C).comp F

The natural isomorphism F.mapShortComplex ⋙ homologyFunctor D ≅ homologyFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology.

Equations

• CategoryTheory.ShortComplex.homologyFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapHomologyIso F) ⋯

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_map_iff {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {hl₁ : S₁.LeftHomologyData} {hl₂ : S₂.LeftHomologyData} (ψl : LeftHomologyMapData φ hl₁ hl₂) [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F] : QuasiIso (F.mapShortComplex.map φ) ↔ IsIso (F.map ψl.φH)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_map_iff {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {hr₁ : S₁.RightHomologyData} {hr₂ : S₂.RightHomologyData} (ψr : RightHomologyMapData φ hr₁ hr₂) [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] : QuasiIso (F.mapShortComplex.map φ) ↔ IsIso (F.map ψr.φH)

instance CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology {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] (F : Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] [QuasiIso φ] : QuasiIso (F.mapShortComplex.map φ)

theorem CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology {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] (F : Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] [F.ReflectsIsomorphisms] : QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ

instance CategoryTheory.ShortComplex.quasiIso_map_of_preservesRightHomology {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] (F : Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] [QuasiIso φ] : QuasiIso (F.mapShortComplex.map φ)

theorem CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesRightHomology {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] (F : Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] [F.ReflectsIsomorphisms] : QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ

theorem CategoryTheory.Functor.preservesLeftHomology_of_zero_f {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) (hf : S.f = 0) [Limits.PreservesLimit (Limits.parallelPair S.g 0) F] : F.PreservesLeftHomologyOf S

If a short complex S is such that S.f = 0 and that the kernel of S.g is preserved by a functor F, then F preserves the left homology of S.

theorem CategoryTheory.Functor.preservesRightHomology_of_zero_g {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) (hg : S.g = 0) [Limits.PreservesColimit (Limits.parallelPair S.f 0) F] : F.PreservesRightHomologyOf S

If a short complex S is such that S.g = 0 and that the cokernel of S.f is preserved by a functor F, then F preserves the right homology of S.

theorem CategoryTheory.Functor.preservesLeftHomology_of_zero_g {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) (hg : S.g = 0) [Limits.PreservesColimit (Limits.parallelPair S.f 0) F] : F.PreservesLeftHomologyOf S

If a short complex S is such that S.g = 0 and that the cokernel of S.f is preserved by a functor F, then F preserves the left homology of S.

theorem CategoryTheory.Functor.preservesRightHomology_of_zero_f {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] (F : Functor C D) [F.PreservesZeroMorphisms] (S : ShortComplex C) (hf : S.f = 0) [Limits.PreservesLimit (Limits.parallelPair S.g 0) F] : F.PreservesRightHomologyOf S

If a short complex S is such that S.f = 0 and that the kernel of S.g is preserved by a functor F, then F preserves the right homology of S.

theorem CategoryTheory.NatTrans.app_homology {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] {F G : Functor C D} (τ : F ⟶ G) (S : ShortComplex C) [S.HasHomology] [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] : τ.app S.homology = CategoryStruct.comp (S.mapHomologyIso F).inv (CategoryStruct.comp (ShortComplex.homologyMap (S.mapNatTrans τ)) (S.mapHomologyIso G).hom)