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} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : Type (max u v)

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

• left : S.LeftHomologyData

  a left homology data

• right : S.RightHomologyData

  a right homology data

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

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

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

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

@[simp]

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

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

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.

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

  a left homology map data

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

  a right homology map data

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

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

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

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

Equations

• CategoryTheory.ShortComplex.HomologyMapData.instInhabited = { default := { left := default, right := default } }

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

Equations

• CategoryTheory.ShortComplex.HomologyMapData.instUnique = Unique.mk' (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)

def CategoryTheory.ShortComplex.HomologyMapData.homologyMapData {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) : 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.

Equations

• CategoryTheory.ShortComplex.HomologyMapData.homologyMapData φ h₁ h₂ = default

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

Equations

• CategoryTheory.ShortComplex.HomologyData.ofIso e h = CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono e.hom h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• h.op = { left := h.right.op, right := h.left.op, iso := h.iso.op, comm := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• h.unop = { left := h.right.unop, right := h.left.unop, iso := h.iso.unop, comm := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

• condition : Nonempty S.HomologyData

  the condition that there exists a homology data

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

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

Equations

• S.homologyData = ⋯.some

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

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

instance CategoryTheory.ShortComplex.instHasHomologyUnopOfOpposite {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex Cᵒᵖ) [S.HasHomology] : S.unop.HasHomology

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

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

instance CategoryTheory.ShortComplex.hasHomology_of_hasCokernel {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (Z : C) [Limits.HasCokernel f] : { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.HasHomology

instance CategoryTheory.ShortComplex.hasHomology_of_hasKernel {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {Y Z : C} (g : Y ⟶ Z) (X : C) [Limits.HasKernel g] : { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := g, zero := ⋯ }.HasHomology

instance CategoryTheory.ShortComplex.hasHomology_of_zeros {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X Y Z : C) : { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := 0, zero := ⋯ }.HasHomology

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

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

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

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

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

Equations

• CategoryTheory.ShortComplex.HomologyMapData.id h = { left := CategoryTheory.ShortComplex.LeftHomologyMapData.id h.left, right := CategoryTheory.ShortComplex.RightHomologyMapData.id h.right }

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

The composition of homology map data.

Equations

• ψ.comp ψ' = { left := ψ.left.comp ψ'.left, right := ψ.right.comp ψ'.right }

@[simp]

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

@[simp]

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

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

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

Equations

• ψ.op = { left := ψ.right.op, right := ψ.left.op }

@[simp]

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

@[simp]

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

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

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

Equations

• ψ.unop = { left := ψ.right.unop, right := ψ.left.unop }

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.ofZeros {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : HomologyMapData φ (HomologyData.ofZeros S₁ hf₁ hg₁) (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.

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : Limits.CokernelCofork S.f) (hc : Limits.IsColimit c) : HomologyMapData (CategoryStruct.id S) (HomologyData.ofZeros S hf hg) (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.

Equations

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

noncomputable def CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : Limits.KernelFork S.g) (hc : Limits.IsLimit c) : HomologyMapData (CategoryStruct.id S) (HomologyData.ofIsLimitKernelFork S hf c hc) (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 .

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• S.homology = S.homologyData.left.H

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

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

Equations

• S.leftHomologyIso = CategoryTheory.ShortComplex.leftHomologyMapIso' (CategoryTheory.Iso.refl S) S.leftHomologyData S.homologyData.left

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

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

Equations

• S.rightHomologyIso = CategoryTheory.ShortComplex.rightHomologyMapIso' (CategoryTheory.Iso.refl S) S.rightHomologyData S.homologyData.right ≪≫ S.homologyData.iso.symm

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

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

Equations

• h.homologyIso = S.leftHomologyIso.symm ≪≫ h.leftHomologyIso

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

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

Equations

• h.homologyIso = S.rightHomologyIso.symm ≪≫ h.rightHomologyIso

@[simp]

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

@[simp]

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

def CategoryTheory.ShortComplex.homologyMap' {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) : 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.

Equations

• CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ h₁.left h₂.left

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

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

Equations

• CategoryTheory.ShortComplex.homologyMap φ = CategoryTheory.ShortComplex.homologyMap' φ S₁.homologyData S₂.homologyData

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

def CategoryTheory.ShortComplex.homologyMapIso' {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) : 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.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• CategoryTheory.ShortComplex.homologyMapIso e = { hom := CategoryTheory.ShortComplex.homologyMap e.hom, inv := CategoryTheory.ShortComplex.homologyMap e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

def CategoryTheory.ShortComplex.leftRightHomologyComparison' {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) : 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.

Equations

• CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = h₂.liftH (h₁.descH (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) ⋯) ⋯

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• S.leftRightHomologyComparison = CategoryTheory.ShortComplex.leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• hasHomology (S : ShortComplex C) : S.HasHomology

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

• S.homologyπ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ S.leftHomologyIso.hom

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

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

Equations

• S.homologyι = CategoryTheory.CategoryStruct.comp S.rightHomologyIso.inv S.rightHomologyι

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• S.homologyIsCokernel = S.leftHomologyIsCokernel.ofIsoColimit (CategoryTheory.Limits.Cofork.ext S.leftHomologyIso ⋯)

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

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

Equations

• S.homologyIsKernel = S.rightHomologyIsKernel.ofIsoLimit (CategoryTheory.Limits.Fork.ext S.rightHomologyIso ⋯)

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

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

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

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

Equations

• S.descHomology k hk = S.homologyIsCokernel.desc (CategoryTheory.Limits.CokernelCofork.ofπ k hk)

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

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

Equations

• S.liftHomology k hk = S.homologyIsKernel.lift (CategoryTheory.Limits.KernelFork.ofι k hk)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• S.homologyIsoKernelDesc = S.rightHomologyIso.symm ≪≫ S.rightHomologyIsoKernelDesc

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

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

Equations

• S.homologyIsoCokernelLift = S.leftHomologyIso.symm ≪≫ CategoryTheory.ShortComplex.leftHomologyIsoCokernelLift

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

Equations

• S.homologyOpIso = S.op.leftHomologyIso.symm ≪≫ S.leftHomologyOpIso ≪≫ S.rightHomologyIso.symm.op

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

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

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

theorem CategoryTheory.ShortComplex.homologyOpIso_hom_naturality_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] {Z : Cᵒᵖ} (h : Opposite.op S₁.homology ⟶ Z) : CategoryStruct.comp (homologyMap (opMap φ)) (CategoryStruct.comp S₁.homologyOpIso.hom h) = CategoryStruct.comp S₂.homologyOpIso.hom (CategoryStruct.comp (homologyMap φ).op h)

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

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

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

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

Equations

• CategoryTheory.ShortComplex.homologyFunctorOpNatIso C = CategoryTheory.NatIso.ofComponents (fun (S : (CategoryTheory.ShortComplex C)ᵒᵖ) => (Opposite.unop S).homologyOpIso.symm) ⋯

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

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

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

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

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

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

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

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

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

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

Equations

• S.asIsoHomologyπ hf = CategoryTheory.asIso S.homologyπ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• S.asIsoHomologyι hg = CategoryTheory.asIso S.homologyι

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Given a short complex S such that S.HasHomology, this is the canonical left homology data for S whose K and H fields are respectively S.cycles and S.homology.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.canonical_K {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).K = S.cycles

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.canonical_i {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).i = S.iCycles

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.canonical_π {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).π = S.homologyπ

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.canonical_H {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).H = S.homology

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.canonical_f' {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).f' = S.toCycles

Computation of the f' field of LeftHomologyData.canonical.

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

Given a short complex S such that S.HasHomology, this is the canonical right homology data for S whose Q and H fields are respectively S.opcycles and S.homology.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.canonical_p {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).p = S.pOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.canonical_Q {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).Q = S.opcycles

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.canonical_ι {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).ι = S.homologyι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.canonical_H {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).H = S.homology

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.canonical_g' {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).g' = S.fromOpcycles

Computation of the g' field of RightHomologyData.canonical.

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

Given a short complex S such that S.HasHomology, this is the canonical homology data for S whose left.K, left/right.H and right.Q fields are respectively S.cycles, S.homology and S.opcycles.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_left_i {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).left.i = S.iCycles

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_right_Q {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).right.Q = S.opcycles

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_iso_inv {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).iso.inv = CategoryStruct.id S.homology

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_right_ι {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).right.ι = S.homologyι

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_left_K {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).left.K = S.cycles

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_right_H {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).right.H = S.homology

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_left_H {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).left.H = S.homology

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_left_π {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).left.π = S.homologyπ

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_right_p {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).right.p = S.pOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.HomologyData.canonical_iso_hom {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] : (canonical S).iso.hom = CategoryStruct.id S.homology