Homology of short complexes

In this file, we shall define the homology of short complexes S, i.e. diagrams f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0. We shall say that [S.HasHomology] when there exists h : S.HomologyData. A homology data for S consists of compatible left/right homology data left and right. The left homology data left involves an object left.H that is a cokernel of the canonical map S.X₁ ⟶ K where K is a kernel of g. On the other hand, the dual notion right.H is a kernel of the canonical morphism Q ⟶ S.X₃ when Q is a cokernel of f. The compatibility that is required involves an isomorphism left.H ≅ right.H which makes a certain pentagon commute. When such a homology data exists, S.homology shall be defined as h.left.H for a chosen h : S.HomologyData.

This definition requires very little assumption on the category (only the existence of zero morphisms). We shall prove that in abelian categories, all short complexes have homology data.

Note: This definition arose by the end of the Liquid Tensor Experiment which contained a structure has_homology which is quite similar to S.HomologyData. After the category ShortComplex C was introduced by J. Riou, A. Topaz suggested such a structure could be used as a basis for the definition of homology.

structure CategoryTheory.ShortComplex.HomologyData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : Type (max u v)

• left : CategoryTheory.ShortComplex.LeftHomologyData S

  a left homology data

• right : CategoryTheory.ShortComplex.RightHomologyData S

  a right homology data

• iso : s.left.H ≅ s.right.H

  the compatibility isomorphism relating the two dual notions of LeftHomologyData and RightHomologyData

• comm : CategoryTheory.CategoryStruct.comp s.left.π (CategoryTheory.CategoryStruct.comp s.iso.hom s.right.ι) = CategoryTheory.CategoryStruct.comp s.left.i s.right.p

  the pentagon relation expressing the compatibility of the left and right homology data

A homology data for a short complex consists of two compatible left and right homology data

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.comm_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : CategoryTheory.ShortComplex.HomologyData S) {Z : C} (h : self.right.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp self.left.π (CategoryTheory.CategoryStruct.comp self.iso.hom (CategoryTheory.CategoryStruct.comp self.right.ι h)) = CategoryTheory.CategoryStruct.comp self.left.i (CategoryTheory.CategoryStruct.comp self.right.p h)

structure CategoryTheory.ShortComplex.HomologyMapData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : Type v

• left : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left

  a left homology map data

• right : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right

  a right homology map data

A homology map data for a morphism φ : S₁ ⟶ S₂ where both S₁ and S₂ are equipped with homology data consists of left and right homology map data.

theorem CategoryTheory.ShortComplex.HomologyMapData.comm_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (h : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) {Z : C} (h : h₂.right.H ⟶ Z) : CategoryTheory.CategoryStruct.comp h.left.φH (CategoryTheory.CategoryStruct.comp h₂.iso.hom h) = CategoryTheory.CategoryStruct.comp h₁.iso.hom (CategoryTheory.CategoryStruct.comp h.right.φH h)

theorem CategoryTheory.ShortComplex.HomologyMapData.comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (h : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : CategoryTheory.CategoryStruct.comp h.left.φH h₂.iso.hom = CategoryTheory.CategoryStruct.comp h₁.iso.hom h.right.φH

instance CategoryTheory.ShortComplex.HomologyMapData.instSubsingletonHomologyMapData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} : Subsingleton (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)

instance CategoryTheory.ShortComplex.HomologyMapData.instInhabitedHomologyMapData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} : Inhabited (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)

instance CategoryTheory.ShortComplex.HomologyMapData.instUniqueHomologyMapData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} : Unique (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)

def CategoryTheory.ShortComplex.HomologyMapData.homologyMapData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂

A choice of the (unique) homology map data associated with a morphism φ : S₁ ⟶ S₂ where both short complexes S₁ and S₂ are equipped with homology data.

theorem CategoryTheory.ShortComplex.HomologyMapData.congr_left_φH {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} {γ₁ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂} {γ₂ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.left.φH = γ₂.left.φH

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).right = CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).left = CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).H

def CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.ShortComplex.HomologyData S

When the first map S.f is zero, this is the homology data on S given by any limit kernel fork of S.g

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofHasKernel_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.Limits.HasKernel S.g] : (CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).left = CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofHasKernel_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.Limits.HasKernel S.g] : (CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).right = CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofHasKernel_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.Limits.HasKernel S.g] : (CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf).H

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofHasKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.Limits.HasKernel S.g] : CategoryTheory.ShortComplex.HomologyData S

When the first map S.f is zero, this is the homology data on S given by the chosen kernel S.g

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).left = CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).H

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).right = CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc

def CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.ShortComplex.HomologyData S

When the second map S.g is zero, this is the homology data on S given by any colimit cokernel cofork of S.f

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.Limits.HasCokernel S.f] : (CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).left = CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.Limits.HasCokernel S.f] : (CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).H

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.Limits.HasCokernel S.f] : (CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).right = CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel S hg

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofHasCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.Limits.HasCokernel S.f] : CategoryTheory.ShortComplex.HomologyData S

When the second map S.g is zero, this is the homology data on S given by the chosen cokernel S.f

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofZeros_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).left = CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofZeros_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).right = CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofZeros_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).H

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofZeros {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : CategoryTheory.ShortComplex.HomologyData S

When both S.f and S.g are zero, the middle object S.X₂ gives a homology data on S

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).left = CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).iso = h.iso

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).right = CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h.right

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HomologyData S₂

If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a homology data for S₁ induces a homology data for S₂. The inverse construction is ofEpiOfIsIsoOfMono'.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).right = CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h.right

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).left = CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).iso = h.iso

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HomologyData S₁

If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a homology data for S₂ induces a homology data for S₁. The inverse construction is ofEpiOfIsIsoOfMono.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_right_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.p = (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' (CategoryTheory.ShortComplex.opMap e.hom) (CategoryTheory.ShortComplex.RightHomologyData.op h.right)).i.unop

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).iso = h.iso

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_left_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.π = h.left.π

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_left_H {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.H = h.left.H

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_left_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.K = h.left.K

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_left_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.i = CategoryTheory.CategoryStruct.comp h.left.i e.hom.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_right_Q {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.Q = (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' (CategoryTheory.ShortComplex.opMap e.hom) (CategoryTheory.ShortComplex.RightHomologyData.op h.right)).K.unop

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_right_H {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.H = (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' (CategoryTheory.ShortComplex.opMap e.hom) (CategoryTheory.ShortComplex.RightHomologyData.op h.right)).H.unop

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIso_right_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.ι = (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' (CategoryTheory.ShortComplex.opMap e.hom) (CategoryTheory.ShortComplex.RightHomologyData.op h.right)).π.unop

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) : CategoryTheory.ShortComplex.HomologyData S₂

If e : S₁ ≅ S₂ is an isomorphism of short complexes and h₁ : HomologyData S₁, this is the homology data for S₂ deduced from the isomorphism.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.op_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyData.op h).iso = CategoryTheory.Iso.op h.iso

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.op_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyData.op h).left = CategoryTheory.ShortComplex.RightHomologyData.op h.right

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.op_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyData.op h).right = CategoryTheory.ShortComplex.LeftHomologyData.op h.left

def CategoryTheory.ShortComplex.HomologyData.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.HomologyData (CategoryTheory.ShortComplex.op S)

A homology data for a short complex S induces a homology data for S.op.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.unop_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyData.unop h).iso = CategoryTheory.Iso.unop h.iso

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.unop_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyData.unop h).left = CategoryTheory.ShortComplex.RightHomologyData.unop h.right

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.unop_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyData.unop h).right = CategoryTheory.ShortComplex.LeftHomologyData.unop h.left

def CategoryTheory.ShortComplex.HomologyData.unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.HomologyData (CategoryTheory.ShortComplex.unop S)

A homology data for a short complex S in the opposite category induces a homology data for S.unop.

class CategoryTheory.ShortComplex.HasHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : Prop

• condition : Nonempty (CategoryTheory.ShortComplex.HomologyData S)

  the condition that there exists a homology data

A short complex S has homology when there exists a S.HomologyData

noncomputable def CategoryTheory.ShortComplex.homologyData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.HomologyData S

A chosen S.HomologyData for a short complex S that has homology

theorem CategoryTheory.ShortComplex.HasHomology.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.HasHomology S

instance CategoryTheory.ShortComplex.instHasHomologyOppositeOppositeHasZeroMorphismsOppositeOp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.op S)

instance CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.HasLeftHomology S

instance CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.HasRightHomology S

instance CategoryTheory.ShortComplex.hasHomology_of_hasCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasCokernel f] : CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.mk f 0 (_ : CategoryTheory.CategoryStruct.comp f 0 = 0))

instance CategoryTheory.ShortComplex.hasHomology_of_hasKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {Y : C} {Z : C} (g : Y ⟶ Z) (X : C) [CategoryTheory.Limits.HasKernel g] : CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.mk 0 g (_ : CategoryTheory.CategoryStruct.comp 0 g = 0))

instance CategoryTheory.ShortComplex.hasHomology_of_zeros {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) (Z : C) : CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.mk 0 0 (_ : CategoryTheory.CategoryStruct.comp 0 0 = 0))

theorem CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HasHomology S₂

theorem CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HasHomology S₁

theorem CategoryTheory.ShortComplex.hasHomology_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] : CategoryTheory.ShortComplex.HasHomology S₂

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.id_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyMapData.id h).left = CategoryTheory.ShortComplex.LeftHomologyMapData.id h.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.id_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : (CategoryTheory.ShortComplex.HomologyMapData.id h).right = CategoryTheory.ShortComplex.RightHomologyMapData.id h.right

def CategoryTheory.ShortComplex.HomologyMapData.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S) h h

The homology map data associated to the identity morphism of a short complex.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.zero_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : (CategoryTheory.ShortComplex.HomologyMapData.zero h₁ h₂).left = CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁.left h₂.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.zero_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : (CategoryTheory.ShortComplex.HomologyMapData.zero h₁ h₂).right = CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁.right h₂.right

def CategoryTheory.ShortComplex.HomologyMapData.zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : CategoryTheory.ShortComplex.HomologyMapData 0 h₁ h₂

The homology map data associated to the zero morphism between two short complexes.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.comp_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} {h₃ : CategoryTheory.ShortComplex.HomologyData S₃} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃) : (CategoryTheory.ShortComplex.HomologyMapData.comp ψ ψ').left = CategoryTheory.ShortComplex.LeftHomologyMapData.comp ψ.left ψ'.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.comp_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} {h₃ : CategoryTheory.ShortComplex.HomologyData S₃} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃) : (CategoryTheory.ShortComplex.HomologyMapData.comp ψ ψ').right = CategoryTheory.ShortComplex.RightHomologyMapData.comp ψ.right ψ'.right

def CategoryTheory.ShortComplex.HomologyMapData.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} {h₃ : CategoryTheory.ShortComplex.HomologyData S₃} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.comp φ φ') h₁ h₃

The composition of homology map data.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.op_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.HomologyMapData.op ψ).right = CategoryTheory.ShortComplex.LeftHomologyMapData.op ψ.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.op_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.HomologyMapData.op ψ).left = CategoryTheory.ShortComplex.RightHomologyMapData.op ψ.right

def CategoryTheory.ShortComplex.HomologyMapData.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.ShortComplex.opMap φ) (CategoryTheory.ShortComplex.HomologyData.op h₂) (CategoryTheory.ShortComplex.HomologyData.op h₁)

A homology map data for a morphism of short complexes induces a homology map data in the opposite category.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.unop_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.HomologyMapData.unop ψ).left = CategoryTheory.ShortComplex.RightHomologyMapData.unop ψ.right

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.unop_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.HomologyMapData.unop ψ).right = CategoryTheory.ShortComplex.LeftHomologyMapData.unop ψ.left

def CategoryTheory.ShortComplex.HomologyMapData.unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.ShortComplex.unopMap φ) (CategoryTheory.ShortComplex.HomologyData.unop h₂) (CategoryTheory.ShortComplex.HomologyData.unop h₁)

A homology map data for a morphism of short complexes in the opposite category induces a homology map data in the original category.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.ofZeros_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : (CategoryTheory.ShortComplex.HomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.ofZeros_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : (CategoryTheory.ShortComplex.HomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂

def CategoryTheory.ShortComplex.HomologyMapData.ofZeros {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : CategoryTheory.ShortComplex.HomologyMapData φ (CategoryTheory.ShortComplex.HomologyData.ofZeros S₁ hf₁ hg₁) (CategoryTheory.ShortComplex.HomologyData.ofZeros S₂ hf₂ hg₂)

When S₁.f, S₁.g, S₂.f and S₂.g are all zero, the action on homology of a morphism φ : S₁ ⟶ S₂ is given by the action φ.τ₂ on the middle objects.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm

def CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : CategoryTheory.ShortComplex.HomologyMapData φ (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)

When S₁.g and S₂.g are zero and we have chosen colimit cokernel coforks c₁ and c₂ for S₁.f and S₂.f respectively, the action on homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that φ.τ₂ ≫ c₂.π = c₁.π ≫ f.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g) (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g) (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)) : (CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g) (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g) (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)) : (CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm

def CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g) (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g) (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)) : CategoryTheory.ShortComplex.HomologyMapData φ (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁) (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)

When S₁.f and S₂.f are zero and we have chosen limit kernel forks c₁ and c₂ for S₁.g and S₂.g respectively, the action on homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι.

def CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg) (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc)

When both maps S.f and S.g of a short complex S are zero, this is the homology map data (for the identity of S) which relates the homology data ofZeros and ofIsColimitCokernelCofork.

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork hf hg c hc).right = CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork hf hg c hc).left = CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc

def CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc) (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg)

When both maps S.f and S.g of a short complex S are zero, this is the homology map data (for the identity of S) which relates the homology data HomologyData.ofIsLimitKernelFork and ofZeros .

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.ofEpiOfIsIsoOfMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HomologyMapData φ h (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h)

This homology map data expresses compatibilities of the homology data constructed by HomologyData.ofEpiOfIsIsoOfMono

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.ofEpiOfIsIsoOfMono' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.HomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HomologyMapData φ (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h) h

This homology map data expresses compatibilities of the homology data constructed by HomologyData.ofEpiOfIsIsoOfMono'

noncomputable def CategoryTheory.ShortComplex.homology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : C

The homology of a short complex is the left.H field of a chosen homology data.

noncomputable def CategoryTheory.ShortComplex.leftHomologyIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.leftHomology S ≅ CategoryTheory.ShortComplex.homology S

When a short complex has homology, this is the canonical isomorphism S.leftHomology ≅ S.homology.

noncomputable def CategoryTheory.ShortComplex.rightHomologyIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.rightHomology S ≅ CategoryTheory.ShortComplex.homology S

When a short complex has homology, this is the canonical isomorphism S.rightHomology ≅ S.homology.

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.homologyIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.homology S ≅ h.H

When a short complex has homology, its homology can be computed using any left homology data.

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.homologyIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.homology S ≅ h.H

When a short complex has homology, its homology can be computed using any right homology data.

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.LeftHomologyData.homologyIso (CategoryTheory.ShortComplex.leftHomologyData S) = (CategoryTheory.ShortComplex.leftHomologyIso S).symm

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.RightHomologyData.homologyIso (CategoryTheory.ShortComplex.rightHomologyData S) = (CategoryTheory.ShortComplex.rightHomologyIso S).symm

def CategoryTheory.ShortComplex.homologyMap' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : h₁.left.H ⟶ h₂.left.H

Given a morphism φ : S₁ ⟶ S₂ of short complexes and homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced homology map h₁.left.H ⟶ h₁.left.H.

noncomputable def CategoryTheory.ShortComplex.homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.ShortComplex.homology S₁ ⟶ CategoryTheory.ShortComplex.homology S₂

The homology map S₁.homology ⟶ S₂.homology induced by a morphism S₁ ⟶ S₂ of short complexes.

theorem CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ = γ.left.φH

theorem CategoryTheory.ShortComplex.HomologyMapData.cyclesMap'_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.cyclesMap' φ h₁.left h₂.left = γ.left.φK

theorem CategoryTheory.ShortComplex.HomologyMapData.opcyclesMap'_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.opcyclesMap' φ h₁.right h₂.right = γ.right.φQ

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.ShortComplex.homologyMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).hom (CategoryTheory.CategoryStruct.comp γ.φH (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₂).inv)

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).hom γ.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.ShortComplex.homologyMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₁).hom (CategoryTheory.CategoryStruct.comp γ.φH (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).inv)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₁).hom γ.φH

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap'_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.id S) h h = CategoryTheory.CategoryStruct.id h.left.H

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.homology S)

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap'_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : CategoryTheory.ShortComplex.homologyMap' 0 h₁ h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.ShortComplex.homologyMap 0 = 0

theorem CategoryTheory.ShortComplex.homologyMap'_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) (h₃ : CategoryTheory.ShortComplex.HomologyData S₃) : CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂) (CategoryTheory.ShortComplex.homologyMap' φ₂ h₂ h₃)

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology S₃] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) : CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ₁) (CategoryTheory.ShortComplex.homologyMap φ₂)

@[simp]

theorem CategoryTheory.ShortComplex.homologyMapIso'_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : (CategoryTheory.ShortComplex.homologyMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.homologyMap' e.hom h₁ h₂

@[simp]

theorem CategoryTheory.ShortComplex.homologyMapIso'_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : (CategoryTheory.ShortComplex.homologyMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.homologyMap' e.inv h₂ h₁

def CategoryTheory.ShortComplex.homologyMapIso' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : h₁.left.H ≅ h₂.left.H

Given an isomorphism S₁ ≅ S₂ of short complexes and homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced homology isomorphism h₁.left.H ≅ h₁.left.H.

instance CategoryTheory.ShortComplex.isIso_homologyMap'_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂)

@[simp]

theorem CategoryTheory.ShortComplex.homologyMapIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : (CategoryTheory.ShortComplex.homologyMapIso e).inv = CategoryTheory.ShortComplex.homologyMap e.inv

@[simp]

theorem CategoryTheory.ShortComplex.homologyMapIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : (CategoryTheory.ShortComplex.homologyMapIso e).hom = CategoryTheory.ShortComplex.homologyMap e.hom

noncomputable def CategoryTheory.ShortComplex.homologyMapIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.ShortComplex.homology S₁ ≅ CategoryTheory.ShortComplex.homology S₂

The homology isomorphism S₁.homology ⟶ S₂.homology induced by an isomorphism S₁ ≅ S₂ of short complexes.

instance CategoryTheory.ShortComplex.isIso_homologyMap_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

def CategoryTheory.ShortComplex.leftRightHomologyComparison' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : h₁.H ⟶ h₂.H

If a short complex S has both a left homology data h₁ and a right homology data h₂, this is the canonical morphism h₁.H ⟶ h₂.H.

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.ShortComplex.RightHomologyData.liftH h₂ (CategoryTheory.ShortComplex.LeftHomologyData.descH h₁ (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) = 0)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.descH h₁ (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) = 0)) (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) = 0)

@[simp]

theorem CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) {Z : C} (h : h₂.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) (CategoryTheory.CategoryStruct.comp h₂.ι h)) = CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp h₂.p h)

@[simp]

theorem CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h₂.ι) = CategoryTheory.CategoryStruct.comp h₁.i h₂.p

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.ShortComplex.LeftHomologyData.descH h₁ (CategoryTheory.ShortComplex.RightHomologyData.liftH h₂ (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) = 0)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) (CategoryTheory.ShortComplex.RightHomologyData.liftH h₂ (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) = 0)) = 0)

noncomputable def CategoryTheory.ShortComplex.leftRightHomologyComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.ShortComplex.HasRightHomology S] : CategoryTheory.ShortComplex.leftHomology S ⟶ CategoryTheory.ShortComplex.rightHomology S

If a short complex S has both a left and right homology, this is the canonical morphism S.leftHomology ⟶ S.rightHomology.

@[simp]

theorem CategoryTheory.ShortComplex.π_leftRightHomologyComparison_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.ShortComplex.HasRightHomology S] {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S) h)

@[simp]

theorem CategoryTheory.ShortComplex.π_leftRightHomologyComparison_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.ShortComplex.HasRightHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison S) (CategoryTheory.ShortComplex.rightHomologyι S)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.ShortComplex.pOpcycles S)

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₁' : CategoryTheory.ShortComplex.LeftHomologyData S₂) (h₂' : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : h₂'.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₁') (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₂ h₂') h)

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₁' : CategoryTheory.ShortComplex.LeftHomologyData S₂) (h₂' : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₁') (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) (CategoryTheory.ShortComplex.rightHomologyMap' φ h₂ h₂')

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₁' : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) (h₂' : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h₁') (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h₂' h₂))

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.ShortComplex.HasRightHomology S] (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.ShortComplex.leftRightHomologyComparison S = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h₁).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h₂).inv)

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.leftRightHomologyComparison' h.left h.right = h.iso.hom

instance CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h.left h.right)

instance CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S] (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)

instance CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison S)

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)] : (CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).right = h₂

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)] : (CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).iso = CategoryTheory.asIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)] : (CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).left = h₁

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)] : CategoryTheory.ShortComplex.HomologyData S

This is the homology data for a short complex S that is obtained from a left homology data h₁ and a right homology data h₂ when the comparison morphism leftRightHomologyComparison' h₁ h₂ : h₁.H ⟶ h₂.H is an isomorphism.

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) : CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h.left) (CategoryTheory.CategoryStruct.comp h.iso.hom (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h.right h₂))

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : h₂.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom h)

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).inv (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison_fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.rightHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison S) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S).inv h)

theorem CategoryTheory.ShortComplex.leftRightHomologyComparison_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.leftRightHomologyComparison S = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S).hom (CategoryTheory.ShortComplex.rightHomologyIso S).inv

theorem CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.RightHomologyData.homologyIso h.right = CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h.left ≪≫ h.iso

theorem CategoryTheory.ShortComplex.hasHomology_of_isIso_leftRightHomologyComparison' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)] : CategoryTheory.ShortComplex.HasHomology S

theorem CategoryTheory.ShortComplex.hasHomology_of_isIsoLeftRightHomologyComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.ShortComplex.HasRightHomology S] [h : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison S)] : CategoryTheory.ShortComplex.HasHomology S

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) {Z : C} (h : h₂.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₂).hom h)

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).hom (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₂).hom

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) {Z : C} (h : CategoryTheory.ShortComplex.homology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₂).inv h)

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).inv (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₂).inv

theorem CategoryTheory.ShortComplex.leftHomologyIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.homology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S₁).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S₂).hom h)

theorem CategoryTheory.ShortComplex.leftHomologyIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S₁).hom (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) (CategoryTheory.ShortComplex.leftHomologyIso S₂).hom

theorem CategoryTheory.ShortComplex.leftHomologyIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S₂).inv h)

theorem CategoryTheory.ShortComplex.leftHomologyIso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S₁).inv (CategoryTheory.ShortComplex.leftHomologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.leftHomologyIso S₂).inv

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : h₂.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₁).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom h)

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₁).hom (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : CategoryTheory.ShortComplex.homology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).inv h)

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₁).inv (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).inv

theorem CategoryTheory.ShortComplex.rightHomologyIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.homology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S₁).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S₂).hom h)

theorem CategoryTheory.ShortComplex.rightHomologyIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S₁).hom (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) (CategoryTheory.ShortComplex.rightHomologyIso S₂).hom

theorem CategoryTheory.ShortComplex.rightHomologyIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.rightHomology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S₂).inv h)

theorem CategoryTheory.ShortComplex.rightHomologyIso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S₁).inv (CategoryTheory.ShortComplex.rightHomologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.rightHomologyIso S₂).inv

class CategoryTheory.CategoryWithHomology (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop

• hasHomology : ∀ (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.HasHomology S

We shall say that a category C is a category with homology when all short complexes have homology.

instance CategoryTheory.ShortComplex.instCategoryWithHomologyOppositeOppositeHasZeroMorphismsOpposite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : CategoryTheory.CategoryWithHomology Cᵒᵖ

@[simp]

theorem CategoryTheory.ShortComplex.homologyFunctor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : ∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.homologyFunctor C).map f = CategoryTheory.ShortComplex.homologyMap f

@[simp]

theorem CategoryTheory.ShortComplex.homologyFunctor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.homologyFunctor C).obj S = CategoryTheory.ShortComplex.homology S

noncomputable def CategoryTheory.ShortComplex.homologyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C

The homology functor ShortComplex C ⥤ C for a category C with homology.

instance CategoryTheory.ShortComplex.isIso_homologyMap'_of_epi_of_isIso_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂)

theorem CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (h₁ : CategoryTheory.Epi φ.τ₁) (h₂ : CategoryTheory.IsIso φ.τ₂) (h₃ : CategoryTheory.Mono φ.τ₃) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

instance CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

instance CategoryTheory.ShortComplex.isIso_homologyFunctor_map_of_epi_of_isIso_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.CategoryWithHomology C] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.IsIso ((CategoryTheory.ShortComplex.homologyFunctor C).map φ)

instance CategoryTheory.ShortComplex.isIso_homologyMap_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.IsIso φ] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

noncomputable def CategoryTheory.ShortComplex.homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.cycles S ⟶ CategoryTheory.ShortComplex.homology S

The canonical morphism S.cycles ⟶ S.homology for a short complex S that has homology.

noncomputable def CategoryTheory.ShortComplex.homologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.homology S ⟶ CategoryTheory.ShortComplex.opcycles S

The canonical morphism S.homology ⟶ S.opcycles for a short complex S that has homology.

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) h

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.ShortComplex.leftHomologyIso S).inv = CategoryTheory.ShortComplex.leftHomologyπ S

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyIso_hom_comp_homologyι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) h

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyIso_hom_comp_homologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S).hom (CategoryTheory.ShortComplex.homologyι S) = CategoryTheory.ShortComplex.rightHomologyι S

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_comp_homologyπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.homology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_comp_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.ShortComplex.homologyπ S) = 0

@[simp]

theorem CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.fromOpcycles S) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.ShortComplex.fromOpcycles S) = 0

noncomputable def CategoryTheory.ShortComplex.homologyIsCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.ShortComplex.homologyπ S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.ShortComplex.homologyπ S) = 0))

The homology S.homology of a short complex is the cokernel of the morphism S.toCycles : S.X₁ ⟶ S.cycles.

noncomputable def CategoryTheory.ShortComplex.homologyIsKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.ShortComplex.homologyι S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.ShortComplex.fromOpcycles S) = 0))

The homology S.homology of a short complex is the kernel of the morphism S.fromOpcycles : S.opcycles ⟶ S.X₃.

instance CategoryTheory.ShortComplex.instEpiCyclesHasLeftHomology_of_hasHomologyHomologyHomologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.Epi (CategoryTheory.ShortComplex.homologyπ S)

instance CategoryTheory.ShortComplex.instMonoHomologyOpcyclesHasRightHomology_of_hasHomologyHomologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.Mono (CategoryTheory.ShortComplex.homologyι S)

noncomputable def CategoryTheory.ShortComplex.descHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : CategoryTheory.ShortComplex.cycles S ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) k = 0) : CategoryTheory.ShortComplex.homology S ⟶ A

Given a morphism k : S.cycles ⟶ A such that S.toCycles ≫ k = 0, this is the induced morphism S.homology ⟶ A.

noncomputable def CategoryTheory.ShortComplex.liftHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : A ⟶ CategoryTheory.ShortComplex.opcycles S) (hk : CategoryTheory.CategoryStruct.comp k (CategoryTheory.ShortComplex.fromOpcycles S) = 0) : A ⟶ CategoryTheory.ShortComplex.homology S

Given a morphism k : A ⟶ S.opcycles such that k ≫ S.fromOpcycles = 0, this is the induced morphism A ⟶ S.homology.

@[simp]

theorem CategoryTheory.ShortComplex.π_descHomology_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : CategoryTheory.ShortComplex.cycles S ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) k = 0) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.descHomology S k hk) h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.ShortComplex.π_descHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : CategoryTheory.ShortComplex.cycles S ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) k = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.ShortComplex.descHomology S k hk) = k

@[simp]

theorem CategoryTheory.ShortComplex.liftHomology_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : A ⟶ CategoryTheory.ShortComplex.opcycles S) (hk : CategoryTheory.CategoryStruct.comp k (CategoryTheory.ShortComplex.fromOpcycles S) = 0) {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftHomology S k hk) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.ShortComplex.liftHomology_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : A ⟶ CategoryTheory.ShortComplex.opcycles S) (hk : CategoryTheory.CategoryStruct.comp k (CategoryTheory.ShortComplex.fromOpcycles S) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftHomology S k hk) (CategoryTheory.ShortComplex.homologyι S) = k

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] {Z : C} (h : CategoryTheory.ShortComplex.homology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S₁) (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.ShortComplex.homologyπ S₂)

@[simp]

theorem CategoryTheory.ShortComplex.homologyι_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] {Z : C} (h : CategoryTheory.ShortComplex.opcycles S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h)

@[simp]

theorem CategoryTheory.ShortComplex.homologyι_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.homologyι S₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S₁) (CategoryTheory.ShortComplex.opcyclesMap φ)

@[simp]

theorem CategoryTheory.ShortComplex.homology_π_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S) h)

@[simp]

theorem CategoryTheory.ShortComplex.homology_π_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.ShortComplex.homologyι S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.ShortComplex.pOpcycles S)

noncomputable def CategoryTheory.ShortComplex.homologyIsoKernelDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Limits.HasCokernel S.f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : CategoryTheory.ShortComplex.homology S ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc S.f S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

The homology of a short complex S identifies to the kernel of the induced morphism cokernel S.f ⟶ S.X₃.

noncomputable def CategoryTheory.ShortComplex.homologyIsoCokernelLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : CategoryTheory.ShortComplex.homology S ≅ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

The homology of a short complex S identifies to the cokernel of the induced morphism S.X₁ ⟶ kernel S.g.

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : h.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom (CategoryTheory.CategoryStruct.comp h.π h)

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom h.π

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.homology S ⟶ Z) : CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) h)

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv (CategoryTheory.ShortComplex.homologyπ S)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_inv_comp_homologyι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) h) = CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h).inv h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_inv_comp_homologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).inv (CategoryTheory.ShortComplex.homologyι S) = CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h).inv

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : h.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).hom (CategoryTheory.CategoryStruct.comp h.ι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h).hom h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).hom h.ι = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h).hom

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S).inv h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).hom (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).inv = (CategoryTheory.ShortComplex.leftHomologyIso S).inv

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.homology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyIso S).hom h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).hom (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h).inv = (CategoryTheory.ShortComplex.leftHomologyIso S).hom

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.rightHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S).inv h

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).hom (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h).inv = (CategoryTheory.ShortComplex.rightHomologyIso S).inv

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.homology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyIso S).hom h

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h).hom (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h).inv = (CategoryTheory.ShortComplex.rightHomologyIso S).hom

theorem CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom (CategoryTheory.CategoryStruct.comp h₂.ι h)))) = CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp h₂.p h))

theorem CategoryTheory.ShortComplex.comp_homologyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso h₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.homologyIso h₂).hom h₂.ι))) = CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)

theorem CategoryTheory.ShortComplex.π_homologyMap_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.opcycles S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S₂) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S₁) (CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S₂) h))

theorem CategoryTheory.ShortComplex.π_homologyMap_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.ShortComplex.homologyι S₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S₁) (CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.ShortComplex.pOpcycles S₂))

noncomputable def CategoryTheory.ShortComplex.homologyOpIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.op S) ≅ Opposite.op (CategoryTheory.ShortComplex.homology S)

The canonical isomorphism S.op.homology ≅ Opposite.op S.homology when a short complex S has homology.

theorem CategoryTheory.ShortComplex.homologyMap'_op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) : (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂).op = CategoryTheory.CategoryStruct.comp h₂.iso.inv.op (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.ShortComplex.opMap φ) (CategoryTheory.ShortComplex.HomologyData.op h₂) (CategoryTheory.ShortComplex.HomologyData.op h₁)) h₁.iso.hom.op)

theorem CategoryTheory.ShortComplex.homologyMap_op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] : (CategoryTheory.ShortComplex.homologyMap φ).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyOpIso S₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ)) (CategoryTheory.ShortComplex.homologyOpIso S₁).hom)

noncomputable def CategoryTheory.ShortComplex.homologyFunctorOpNatIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : (CategoryTheory.ShortComplex.homologyFunctor C).op ≅ CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.opFunctor C) (CategoryTheory.ShortComplex.homologyFunctor Cᵒᵖ)

The natural isomorphism (homologyFunctor C).op ≅ opFunctor C ⋙ homologyFunctor Cᵒᵖ which relates the homology in C and in Cᵒᵖ.

theorem CategoryTheory.ShortComplex.liftCycles_homologyπ_eq_zero_of_boundary {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : A ⟶ S.X₂) (x : A ⟶ S.X₁) (hx : k = CategoryTheory.CategoryStruct.comp x S.f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k (_ : CategoryTheory.CategoryStruct.comp k S.g = 0)) (CategoryTheory.ShortComplex.homologyπ S) = 0

theorem CategoryTheory.ShortComplex.homologyι_descOpcycles_π_eq_zero_of_boundary_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp S.g x) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.descOpcycles S k (_ : CategoryTheory.CategoryStruct.comp S.f k = 0)) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.homologyι_descOpcycles_π_eq_zero_of_boundary {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [CategoryTheory.ShortComplex.HasHomology S] (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp S.g x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.ShortComplex.descOpcycles S k (_ : CategoryTheory.CategoryStruct.comp S.f k = 0)) = 0

theorem CategoryTheory.ShortComplex.isIso_homologyMap_of_isIso_cyclesMap_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (h₁ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)) (h₂ : CategoryTheory.Epi φ.τ₁) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

theorem CategoryTheory.ShortComplex.isIso_homologyMap_of_isIso_opcyclesMap_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (h₁ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)) (h₂ : CategoryTheory.Mono φ.τ₃) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

theorem CategoryTheory.ShortComplex.isZero_homology_of_isZero_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hS : CategoryTheory.Limits.IsZero S.X₂) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.Limits.IsZero (CategoryTheory.ShortComplex.homology S)

theorem CategoryTheory.ShortComplex.isIso_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyπ S)

theorem CategoryTheory.ShortComplex.isIso_homologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyι S)

@[simp]

theorem CategoryTheory.ShortComplex.asIsoHomologyπ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] : (CategoryTheory.ShortComplex.asIsoHomologyπ S hf).hom = CategoryTheory.ShortComplex.homologyπ S

noncomputable def CategoryTheory.ShortComplex.asIsoHomologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.cycles S ≅ CategoryTheory.ShortComplex.homology S

The canonical isomorphism S.cycles ≅ S.homology when S.f = 0.

@[simp]

theorem CategoryTheory.ShortComplex.asIsoHomologyπ_inv_comp_homologyπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.homology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.asIsoHomologyπ S hf).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) h) = h

@[simp]

theorem CategoryTheory.ShortComplex.asIsoHomologyπ_inv_comp_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.asIsoHomologyπ S hf).inv (CategoryTheory.ShortComplex.homologyπ S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.homology S)

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_comp_asIsoHomologyπ_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.cycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.asIsoHomologyπ S hf).inv h) = h

@[simp]

theorem CategoryTheory.ShortComplex.homologyπ_comp_asIsoHomologyπ_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ S) (CategoryTheory.ShortComplex.asIsoHomologyπ S hf).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.cycles S)

@[simp]

theorem CategoryTheory.ShortComplex.asIsoHomologyι_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] : (CategoryTheory.ShortComplex.asIsoHomologyι S hg).hom = CategoryTheory.ShortComplex.homologyι S

noncomputable def CategoryTheory.ShortComplex.asIsoHomologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.ShortComplex.homology S ≅ CategoryTheory.ShortComplex.opcycles S

The canonical isomorphism S.homology ≅ S.opcycles when S.g = 0.

@[simp]

theorem CategoryTheory.ShortComplex.asIsoHomologyι_inv_comp_homologyι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.asIsoHomologyι S hg).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) h) = h

@[simp]

theorem CategoryTheory.ShortComplex.asIsoHomologyι_inv_comp_homologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.asIsoHomologyι S hg).inv (CategoryTheory.ShortComplex.homologyι S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.opcycles S)

@[simp]

theorem CategoryTheory.ShortComplex.homologyι_comp_asIsoHomologyι_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] {Z : C} (h : CategoryTheory.ShortComplex.homology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.asIsoHomologyι S hg).inv h) = h

@[simp]

theorem CategoryTheory.ShortComplex.homologyι_comp_asIsoHomologyι_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.ShortComplex.HasHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι S) (CategoryTheory.ShortComplex.asIsoHomologyι S hg).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.homology S)

theorem CategoryTheory.ShortComplex.mono_homologyMap_of_mono_opcyclesMap' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (h : CategoryTheory.Mono (