Right Homology of short complexes

In this file, we define the dual notions to those defined in Algebra.Homology.ShortComplex.LeftHomology. In particular, if S : ShortComplex C is a short complex consisting of two composable maps f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0, we define h : S.RightHomologyData to be the datum of morphisms p : X₂ ⟶ Q and ι : H ⟶ Q such that Q identifies to the cokernel of f and H to the kernel of the induced map g' : Q ⟶ X₃.

When such a S.RightHomologyData exists, we shall say that [S.HasRightHomology] and we define S.rightHomology to be the H field of a chosen right homology data. Similarly, we define S.opcycles to be the Q field.

In Homology.lean, when S has two compatible left and right homology data (i.e. they give the same H up to a canonical isomorphism), we shall define [S.HasHomology] and S.homology.

structure CategoryTheory.ShortComplex.RightHomologyData {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : Type (max u_1 u_2)

A right homology data for a short complex S consists of morphisms p : S.X₂ ⟶ Q and ι : H ⟶ Q such that p identifies Q with the cokernel of f : S.X₁ ⟶ S.X₂, and that ι identifies H with the kernel of the induced map g' : Q ⟶ S.X₃

• Q : C

  a choice of cokernel of S.f : S.X₁ ⟶ S.X₂

• H : C

  a choice of kernel of the induced morphism S.g' : S.Q ⟶ X₃

• p : S.X₂ ⟶ self.Q

  the projection from S.X₂

• ι : self.H ⟶ self.Q

  the inclusion of the (right) homology in the chosen cokernel of S.f

• wp : CategoryStruct.comp S.f self.p = 0

  the cokernel condition for p

• hp : Limits.IsColimit (Limits.CokernelCofork.ofπ self.p ⋯)

  p : S.X₂ ⟶ Q is a cokernel of S.f : S.X₁ ⟶ S.X₂

• wι : CategoryStruct.comp self.ι (self.hp.desc (Limits.CokernelCofork.ofπ S.g ⋯)) = 0

  the kernel condition for ι

• hι : Limits.IsLimit (Limits.KernelFork.ofι self.ι ⋯)

  ι : H ⟶ Q is a kernel of S.g' : Q ⟶ S.X₃

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : S.RightHomologyData

The chosen cokernels and kernels of the limits API give a RightHomologyData

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : (ofHasCokernelOfHasKernel S).H = Limits.kernel (Limits.cokernel.desc S.f S.g ⋯)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : (ofHasCokernelOfHasKernel S).Q = Limits.cokernel S.f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : (ofHasCokernelOfHasKernel S).p = Limits.cokernel.π S.f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : (ofHasCokernelOfHasKernel S).ι = Limits.kernel.ι (Limits.cokernel.desc S.f S.g ⋯)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.wι_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (self : S.RightHomologyData) {Z : C} (h : (Limits.CokernelCofork.ofπ S.g ⋯).pt ⟶ Z) : CategoryStruct.comp self.ι (CategoryStruct.comp (self.hp.desc (Limits.CokernelCofork.ofπ S.g ⋯)) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.wp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (self : S.RightHomologyData) {Z : C} (h : self.Q ⟶ Z) : CategoryStruct.comp S.f (CategoryStruct.comp self.p h) = CategoryStruct.comp 0 h

instance CategoryTheory.ShortComplex.RightHomologyData.instEpiP {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : Epi h.p

instance CategoryTheory.ShortComplex.RightHomologyData.instMonoι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : Mono h.ι

def CategoryTheory.ShortComplex.RightHomologyData.descQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) : h.Q ⟶ A

Any morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism Q ⟶ A

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.p_descQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) : CategoryStruct.comp h.p (h.descQ k hk) = k

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) {Z : C} (h✝ : A ⟶ Z) : CategoryStruct.comp h.p (CategoryStruct.comp (h.descQ k hk) h✝) = CategoryStruct.comp k h✝

def CategoryTheory.ShortComplex.RightHomologyData.descH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) : h.H ⟶ A

The morphism from the (right) homology attached to a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0.

def CategoryTheory.ShortComplex.RightHomologyData.g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : h.Q ⟶ S.X₃

The morphism h.Q ⟶ S.X₃ induced by S.g : S.X₂ ⟶ S.X₃ and the fact that h.Q is a cokernel of S.f : S.X₁ ⟶ S.X₂.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.p_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : CategoryStruct.comp h.p h.g' = S.g

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Z : C} (h✝ : S.X₃ ⟶ Z) : CategoryStruct.comp h.p (CategoryStruct.comp h.g' h✝) = CategoryStruct.comp S.g h✝

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ι_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : CategoryStruct.comp h.ι h.g' = 0

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ι_g'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Z : C} (h✝ : S.X₃ ⟶ Z) : CategoryStruct.comp h.ι (CategoryStruct.comp h.g' h✝) = CategoryStruct.comp 0 h✝

theorem CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = CategoryStruct.comp S.g x) : CategoryStruct.comp h.ι (h.descQ k ⋯) = 0

theorem CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = CategoryStruct.comp S.g x) {Z : C} (h✝ : A ⟶ Z) : CategoryStruct.comp h.ι (CategoryStruct.comp (h.descQ k ⋯) h✝) = CategoryStruct.comp 0 h✝

def CategoryTheory.ShortComplex.RightHomologyData.hι' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : Limits.IsLimit (Limits.KernelFork.ofι h.ι ⋯)

For h : S.RightHomologyData, this is a restatement of h.hι, saying that ι : h.H ⟶ h.Q is a kernel of h.g' : h.Q ⟶ S.X₃.

def CategoryTheory.ShortComplex.RightHomologyData.liftH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : A ⟶ h.Q) (hk : CategoryStruct.comp k h.g' = 0) : A ⟶ h.H

The morphism A ⟶ H induced by a morphism k : A ⟶ Q such that k ≫ g' = 0

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.liftH_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : A ⟶ h.Q) (hk : CategoryStruct.comp k h.g' = 0) : CategoryStruct.comp (h.liftH k hk) h.ι = k

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.liftH_ι_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : A ⟶ h.Q) (hk : CategoryStruct.comp k h.g' = 0) {Z : C} (h✝ : h.Q ⟶ Z) : CategoryStruct.comp (h.liftH k hk) (CategoryStruct.comp h.ι h✝) = CategoryStruct.comp k h✝

theorem CategoryTheory.ShortComplex.RightHomologyData.isIso_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) (hf : S.f = 0) : IsIso h.p

theorem CategoryTheory.ShortComplex.RightHomologyData.isIso_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) (hg : S.g = 0) : IsIso h.ι

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_ι {C : Type u_1} [Category.{u_2, u_1} 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).ι = Limits.Fork.ι c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_Q {C : Type u_1} [Category.{u_2, u_1} 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).Q = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_p {C : Type u_1} [Category.{u_2, u_1} 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).p = CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_H {C : Type u_1} [Category.{u_2, u_1} 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).H = c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_g' {C : Type u_1} [Category.{u_2, u_1} 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).g' = S.g

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasKernel S.g] (hf : S.f = 0) : (ofHasKernel S hf).Q = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasKernel S.g] (hf : S.f = 0) : (ofHasKernel S hf).p = CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasKernel S.g] (hf : S.f = 0) : (ofHasKernel S hf).ι = Limits.kernel.ι S.g

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [Limits.HasKernel S.g] (hf : S.f = 0) : (ofHasKernel S hf).H = Limits.kernel S.g

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q {C : Type u_1} [Category.{u_2, u_1} 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).Q = c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H {C : Type u_1} [Category.{u_2, u_1} 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).H = c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_p {C : Type u_1} [Category.{u_2, u_1} 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).p = Limits.Cofork.π c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ι {C : Type u_1} [Category.{u_2, u_1} 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).ι = CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_g' {C : Type u_1} [Category.{u_2, u_1} 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).g' = 0

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

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

def CategoryTheory.ShortComplex.RightHomologyData.ofZeros {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : S.RightHomologyData

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (ofZeros S hf hg).p = CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (ofZeros S hf hg).Q = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (ofZeros S hf hg).H = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (ofZeros S hf hg).ι = CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) : (ofZeros S hf hg).g' = 0

def CategoryTheory.ShortComplex.RightHomologyData.copy {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H) : S.RightHomologyData

Given a right homology data h of a short complex S, we can construct another right homology data by choosing another cokernel and kernel that are isomorphic to the ones in h.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.copy_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H) : (h.copy eQ eH).Q = Q'

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.copy_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H) : (h.copy eQ eH).p = CategoryStruct.comp h.p eQ.inv

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.copy_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H) : (h.copy eQ eH).ι = CategoryStruct.comp eH.hom (CategoryStruct.comp h.ι eQ.inv)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.copy_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H) : (h.copy eQ eH).H = H'

class CategoryTheory.ShortComplex.HasRightHomology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : Prop

A short complex S has right homology when there exists a S.RightHomologyData

• condition : Nonempty S.RightHomologyData

noncomputable def CategoryTheory.ShortComplex.rightHomologyData {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.RightHomologyData

A chosen S.RightHomologyData for a short complex S that has right homology

theorem CategoryTheory.ShortComplex.HasRightHomology.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : S.HasRightHomology

instance CategoryTheory.ShortComplex.HasRightHomology.of_hasCokernel_of_hasKernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : S.HasRightHomology

instance CategoryTheory.ShortComplex.HasRightHomology.of_hasKernel {C : Type u_1} [Category.{u_2, u_1} 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 := ⋯ }.HasRightHomology

instance CategoryTheory.ShortComplex.HasRightHomology.of_hasCokernel {C : Type u_1} [Category.{u_2, u_1} 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 := ⋯ }.HasRightHomology

instance CategoryTheory.ShortComplex.HasRightHomology.of_zeros {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (X Y Z : C) : { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := 0, zero := ⋯ }.HasRightHomology

def CategoryTheory.ShortComplex.RightHomologyData.op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : S.op.LeftHomologyData

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.op_i {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : h.op.i = h.p.op

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.op_K {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : h.op.K = Opposite.op h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.op_π {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : h.op.π = h.ι.op

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.op_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : h.op.H = Opposite.op h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.op_f' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : h.op.f' = h.g'.op

def CategoryTheory.ShortComplex.RightHomologyData.unop {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : S.unop.LeftHomologyData

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.unop_π {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : h.unop.π = h.ι.unop

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.unop_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : h.unop.H = Opposite.unop h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.unop_K {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : h.unop.K = Opposite.unop h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.unop_i {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : h.unop.i = h.p.unop

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.unop_f' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : h.unop.f' = h.g'.unop

def CategoryTheory.ShortComplex.LeftHomologyData.op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : S.op.RightHomologyData

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : h.op.Q = Opposite.op h.K

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : h.op.ι = h.π.op

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : h.op.p = h.i.op

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : h.op.H = Opposite.op h.H

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : h.op.g' = h.f'.op

def CategoryTheory.ShortComplex.LeftHomologyData.unop {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : S.unop.RightHomologyData

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : h.unop.ι = h.π.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : h.unop.p = h.i.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : h.unop.Q = Opposite.unop h.K

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : h.unop.H = Opposite.unop h.H

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : h.unop.g' = h.f'.unop

instance CategoryTheory.ShortComplex.instHasRightHomologyOppositeOpOfHasLeftHomology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} [S.HasLeftHomology] : S.op.HasRightHomology

instance CategoryTheory.ShortComplex.instHasLeftHomologyOppositeOpOfHasRightHomology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} [S.HasRightHomology] : S.op.HasLeftHomology

theorem CategoryTheory.ShortComplex.hasLeftHomology_iff_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : S.HasLeftHomology ↔ S.op.HasRightHomology

theorem CategoryTheory.ShortComplex.hasRightHomology_iff_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : S.HasRightHomology ↔ S.op.HasLeftHomology

theorem CategoryTheory.ShortComplex.hasLeftHomology_iff_unop {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex Cᵒᵖ) : S.HasLeftHomology ↔ S.unop.HasRightHomology

theorem CategoryTheory.ShortComplex.hasRightHomology_iff_unop {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex Cᵒᵖ) : S.HasRightHomology ↔ S.unop.HasLeftHomology

structure CategoryTheory.ShortComplex.RightHomologyMapData {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : Type u_2

Given right homology data h₁ and h₂ for two short complexes S₁ and S₂, a RightHomologyMapData for a morphism φ : S₁ ⟶ S₂ consists of a description of the induced morphisms on the Q (opcycles) and H (right homology) fields of h₁ and h₂.

• φQ : h₁.Q ⟶ h₂.Q

  the induced map on opcycles

• φH : h₁.H ⟶ h₂.H

  the induced map on right homology

• commp : CategoryStruct.comp h₁.p self.φQ = CategoryStruct.comp φ.τ₂ h₂.p

  commutation with p

• commg' : CategoryStruct.comp self.φQ h₂.g' = CategoryStruct.comp h₁.g' φ.τ₃

  commutation with g'

• commι : CategoryStruct.comp self.φH h₂.ι = CategoryStruct.comp h₁.ι self.φQ

  commutation with ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.commι_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (self : RightHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryStruct.comp self.φH (CategoryStruct.comp h₂.ι h) = CategoryStruct.comp h₁.ι (CategoryStruct.comp self.φQ h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.commp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (self : RightHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryStruct.comp h₁.p (CategoryStruct.comp self.φQ h) = CategoryStruct.comp φ.τ₂ (CategoryStruct.comp h₂.p h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.commg'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (self : RightHomologyMapData φ h₁ h₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryStruct.comp self.φQ (CategoryStruct.comp h₂.g' h) = CategoryStruct.comp h₁.g' (CategoryStruct.comp φ.τ₃ h)

def CategoryTheory.ShortComplex.RightHomologyMapData.zero {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : RightHomologyMapData 0 h₁ h₂

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.zero_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (zero h₁ h₂).φQ = 0

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.zero_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (zero h₁ h₂).φH = 0

def CategoryTheory.ShortComplex.RightHomologyMapData.id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : RightHomologyMapData (CategoryStruct.id S) h h

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.id_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : (id h).φH = CategoryStruct.id h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.id_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : (id h).φQ = CategoryStruct.id h.Q

def CategoryTheory.ShortComplex.RightHomologyMapData.comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) : RightHomologyMapData (CategoryStruct.comp φ φ') h₁ h₃

The composition of right homology map data.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.comp_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) : (ψ.comp ψ').φH = CategoryStruct.comp ψ.φH ψ'.φH

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) : (ψ.comp ψ').φQ = CategoryStruct.comp ψ.φQ ψ'.φQ

instance CategoryTheory.ShortComplex.RightHomologyMapData.instSubsingleton {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : Subsingleton (RightHomologyMapData φ h₁ h₂)

instance CategoryTheory.ShortComplex.RightHomologyMapData.instInhabited {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : Inhabited (RightHomologyMapData φ h₁ h₂)

instance CategoryTheory.ShortComplex.RightHomologyMapData.instUnique {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : Unique (RightHomologyMapData φ h₁ h₂)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φH = γ₂.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φQ = γ₂.φQ

def CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros {C : Type u_1} [Category.{u_2, u_1} 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) : RightHomologyMapData φ (RightHomologyData.ofZeros S₁ hf₁ hg₁) (RightHomologyData.ofZeros S₂ hf₂ hg₂)

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φH {C : Type u_1} [Category.{u_2, u_1} 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₂).φH = φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φQ {C : Type u_1} [Category.{u_2, u_1} 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₂).φQ = φ.τ₂

def CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork {C : Type u_1} [Category.{u_2, u_1} 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₂)) : RightHomologyMapData φ (RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁) (RightHomologyData.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 right 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₂.ι.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φH {C : Type u_1} [Category.{u_2, u_1} 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).φH = f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φQ {C : Type u_1} [Category.{u_2, u_1} 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).φQ = φ.τ₂

def CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork {C : Type u_1} [Category.{u_2, u_1} 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) : RightHomologyMapData φ (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (RightHomologyData.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 right homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that φ.τ₂ ≫ c₂.π = c₁.π ≫ f.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φH {C : Type u_1} [Category.{u_2, u_1} 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).φH = f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φQ {C : Type u_1} [Category.{u_2, u_1} 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).φQ = f

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH {C : Type u_1} [Category.{u_2, u_1} 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 S hf hg c hc).φH = Limits.Fork.ι c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φQ {C : Type u_1} [Category.{u_2, u_1} 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 S hf hg c hc).φQ = CategoryStruct.id (RightHomologyData.ofIsLimitKernelFork S hf c hc).Q

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : Limits.CokernelCofork S.f) (hc : Limits.IsColimit c) : (compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH = Limits.Cofork.π c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : Limits.CokernelCofork S.f) (hc : Limits.IsColimit c) : (compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φQ = Limits.Cofork.π c

noncomputable def CategoryTheory.ShortComplex.rightHomology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : C

The right homology of a short complex, given by the H field of a chosen right homology data.

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyData_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.rightHomologyData.H = S.rightHomology

noncomputable def CategoryTheory.ShortComplex.opcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : C

The "opcycles" of a short complex, given by the Q field of a chosen right homology data. This is the dual notion to cycles.

noncomputable def CategoryTheory.ShortComplex.rightHomologyι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.rightHomology ⟶ S.opcycles

The canonical map S.rightHomology ⟶ S.opcycles.

noncomputable def CategoryTheory.ShortComplex.pOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.X₂ ⟶ S.opcycles

The projection S.X₂ ⟶ S.opcycles.

noncomputable def CategoryTheory.ShortComplex.fromOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.opcycles ⟶ S.X₃

The canonical map S.opcycles ⟶ X₃.

@[simp]

theorem CategoryTheory.ShortComplex.f_pOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : CategoryStruct.comp S.f S.pOpcycles = 0

@[simp]

theorem CategoryTheory.ShortComplex.f_pOpcycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {Z : C} (h : S.opcycles ⟶ Z) : CategoryStruct.comp S.f (CategoryStruct.comp S.pOpcycles h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.p_fromOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : CategoryStruct.comp S.pOpcycles S.fromOpcycles = S.g

@[simp]

theorem CategoryTheory.ShortComplex.p_fromOpcycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {Z : C} (h : S.X₃ ⟶ Z) : CategoryStruct.comp S.pOpcycles (CategoryStruct.comp S.fromOpcycles h) = CategoryStruct.comp S.g h

instance CategoryTheory.ShortComplex.instEpiPOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : Epi S.pOpcycles

instance CategoryTheory.ShortComplex.instMonoRightHomologyι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : Mono S.rightHomologyι

theorem CategoryTheory.ShortComplex.rightHomology_ext_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {A : C} (f₁ f₂ : A ⟶ S.rightHomology) : f₁ = f₂ ↔ CategoryStruct.comp f₁ S.rightHomologyι = CategoryStruct.comp f₂ S.rightHomologyι

theorem CategoryTheory.ShortComplex.rightHomology_ext {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {A : C} (f₁ f₂ : A ⟶ S.rightHomology) (h : CategoryStruct.comp f₁ S.rightHomologyι = CategoryStruct.comp f₂ S.rightHomologyι) : f₁ = f₂

theorem CategoryTheory.ShortComplex.opcycles_ext_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {A : C} (f₁ f₂ : S.opcycles ⟶ A) : f₁ = f₂ ↔ CategoryStruct.comp S.pOpcycles f₁ = CategoryStruct.comp S.pOpcycles f₂

theorem CategoryTheory.ShortComplex.opcycles_ext {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {A : C} (f₁ f₂ : S.opcycles ⟶ A) (h : CategoryStruct.comp S.pOpcycles f₁ = CategoryStruct.comp S.pOpcycles f₂) : f₁ = f₂

theorem CategoryTheory.ShortComplex.isIso_pOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) : IsIso S.pOpcycles

noncomputable def CategoryTheory.ShortComplex.opcyclesIsoX₂ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) : S.opcycles ≅ S.X₂

When S.f = 0, this is the canonical isomorphism S.opcycles ≅ S.X₂ induced by S.pOpcycles.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) : (S.opcyclesIsoX₂ hf).inv = S.pOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_inv_hom_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) : CategoryStruct.comp S.pOpcycles (S.opcyclesIsoX₂ hf).hom = CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_inv_hom_id_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) {Z : C} (h : S.X₂ ⟶ Z) : CategoryStruct.comp S.pOpcycles (CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom h) = h

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_hom_inv_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) : CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom S.pOpcycles = CategoryStruct.id S.opcycles

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_hom_inv_id_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) {Z : C} (h : S.opcycles ⟶ Z) : CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom (CategoryStruct.comp S.pOpcycles h) = h

theorem CategoryTheory.ShortComplex.isIso_rightHomologyι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) : IsIso S.rightHomologyι

noncomputable def CategoryTheory.ShortComplex.opcyclesIsoRightHomology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) : S.opcycles ≅ S.rightHomology

When S.g = 0, this is the canonical isomorphism S.opcycles ≅ S.rightHomology induced by S.rightHomologyι.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) : (S.opcyclesIsoRightHomology hg).inv = S.rightHomologyι

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv_hom_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) : CategoryStruct.comp S.rightHomologyι (S.opcyclesIsoRightHomology hg).hom = CategoryStruct.id S.rightHomology

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv_hom_id_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) {Z : C} (h : S.rightHomology ⟶ Z) : CategoryStruct.comp S.rightHomologyι (CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom h) = h

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_hom_inv_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) : CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom S.rightHomologyι = CategoryStruct.id S.opcycles

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_hom_inv_id_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) {Z : C} (h : S.opcycles ⟶ Z) : CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom (CategoryStruct.comp S.rightHomologyι h) = h

def CategoryTheory.ShortComplex.rightHomologyMapData {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : RightHomologyMapData φ h₁ h₂

The (unique) right homology map data associated to a morphism of short complexes that are both equipped with right homology data.

def CategoryTheory.ShortComplex.rightHomologyMap' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : h₁.H ⟶ h₂.H

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

def CategoryTheory.ShortComplex.opcyclesMap' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : h₁.Q ⟶ h₂.Q

Given a morphism φ : S₁ ⟶ S₂ of short complexes and right homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced morphism h₁.K ⟶ h₁.K on opcycles.

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : CategoryStruct.comp h₁.p (opcyclesMap' φ h₁ h₂) = CategoryStruct.comp φ.τ₂ h₂.p

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C} (h : h₂.Q ⟶ Z) : CategoryStruct.comp h₁.p (CategoryStruct.comp (opcyclesMap' φ h₁ h₂) h) = CategoryStruct.comp φ.τ₂ (CategoryStruct.comp h₂.p h)

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : CategoryStruct.comp (opcyclesMap' φ h₁ h₂) h₂.g' = CategoryStruct.comp h₁.g' φ.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_g'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryStruct.comp (opcyclesMap' φ h₁ h₂) (CategoryStruct.comp h₂.g' h) = CategoryStruct.comp h₁.g' (CategoryStruct.comp φ.τ₃ h)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_naturality' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : CategoryStruct.comp (rightHomologyMap' φ h₁ h₂) h₂.ι = CategoryStruct.comp h₁.ι (opcyclesMap' φ h₁ h₂)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_naturality'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C} (h : h₂.Q ⟶ Z) : CategoryStruct.comp (rightHomologyMap' φ h₁ h₂) (CategoryStruct.comp h₂.ι h) = CategoryStruct.comp h₁.ι (CategoryStruct.comp (opcyclesMap' φ h₁ h₂) h)

noncomputable def CategoryTheory.ShortComplex.rightHomologyMap {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) : S₁.rightHomology ⟶ S₂.rightHomology

The (right) homology map S₁.rightHomology ⟶ S₂.rightHomology induced by a morphism S₁ ⟶ S₂ of short complexes.

noncomputable def CategoryTheory.ShortComplex.opcyclesMap {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) : S₁.opcycles ⟶ S₂.opcycles

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

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) : CategoryStruct.comp S₁.pOpcycles (opcyclesMap φ) = CategoryStruct.comp φ.τ₂ S₂.pOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) {Z : C} (h : S₂.opcycles ⟶ Z) : CategoryStruct.comp S₁.pOpcycles (CategoryStruct.comp (opcyclesMap φ) h) = CategoryStruct.comp φ.τ₂ (CategoryStruct.comp S₂.pOpcycles h)

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcycles_naturality {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) : CategoryStruct.comp (opcyclesMap φ) S₂.fromOpcycles = CategoryStruct.comp S₁.fromOpcycles φ.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcycles_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryStruct.comp (opcyclesMap φ) (CategoryStruct.comp S₂.fromOpcycles h) = CategoryStruct.comp S₁.fromOpcycles (CategoryStruct.comp φ.τ₃ h)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_naturality {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) : CategoryStruct.comp (rightHomologyMap φ) S₂.rightHomologyι = CategoryStruct.comp S₁.rightHomologyι (opcyclesMap φ)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] (φ : S₁ ⟶ S₂) {Z : C} (h : S₂.opcycles ⟶ Z) : CategoryStruct.comp (rightHomologyMap φ) (CategoryStruct.comp S₂.rightHomologyι h) = CategoryStruct.comp S₁.rightHomologyι (CategoryStruct.comp (opcyclesMap φ) h)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) : rightHomologyMap' φ h₁ h₂ = γ.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) : opcyclesMap' φ h₁ h₂ = γ.φQ

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : rightHomologyMap' (CategoryStruct.id S) h h = CategoryStruct.id h.H

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) : opcyclesMap' (CategoryStruct.id S) h h = CategoryStruct.id h.Q

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : rightHomologyMap (CategoryStruct.id S) = CategoryStruct.id S.rightHomology

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : opcyclesMap (CategoryStruct.id S) = CategoryStruct.id S.opcycles

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_zero {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : rightHomologyMap' 0 h₁ h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_zero {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : opcyclesMap' 0 h₁ h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_zero {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S₁ S₂ : ShortComplex C) [S₁.HasRightHomology] [S₂.HasRightHomology] : rightHomologyMap 0 = 0

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_zero {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S₁ S₂ : ShortComplex C) [S₁.HasRightHomology] [S₂.HasRightHomology] : opcyclesMap 0 = 0

theorem CategoryTheory.ShortComplex.rightHomologyMap'_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) : rightHomologyMap' (CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryStruct.comp (rightHomologyMap' φ₁ h₁ h₂) (rightHomologyMap' φ₂ h₂ h₃)

theorem CategoryTheory.ShortComplex.rightHomologyMap'_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) {Z : C} (h : h₃.H ⟶ Z) : CategoryStruct.comp (rightHomologyMap' (CategoryStruct.comp φ₁ φ₂) h₁ h₃) h = CategoryStruct.comp (rightHomologyMap' φ₁ h₁ h₂) (CategoryStruct.comp (rightHomologyMap' φ₂ h₂ h₃) h)

theorem CategoryTheory.ShortComplex.opcyclesMap'_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) : opcyclesMap' (CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryStruct.comp (opcyclesMap' φ₁ h₁ h₂) (opcyclesMap' φ₂ h₂ h₃)

theorem CategoryTheory.ShortComplex.opcyclesMap'_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) {Z : C} (h : h₃.Q ⟶ Z) : CategoryStruct.comp (opcyclesMap' (CategoryStruct.comp φ₁ φ₂) h₁ h₃) h = CategoryStruct.comp (opcyclesMap' φ₁ h₁ h₂) (CategoryStruct.comp (opcyclesMap' φ₂ h₂ h₃) h)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] [S₃.HasRightHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) : rightHomologyMap (CategoryStruct.comp φ₁ φ₂) = CategoryStruct.comp (rightHomologyMap φ₁) (rightHomologyMap φ₂)

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasRightHomology] [S₂.HasRightHomology] [S₃.HasRightHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) : opcyclesMap (CategoryStruct.comp φ₁ φ₂) = CategoryStruct.comp (opcyclesMap φ₁) (opcyclesMap φ₂)

def CategoryTheory.ShortComplex.rightHomologyMapIso' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : h₁.H ≅ h₂.H

An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the H fields of right homology data of S₁ and S₂.

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso'_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (rightHomologyMapIso' e h₁ h₂).inv = rightHomologyMap' e.inv h₂ h₁

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso'_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (rightHomologyMapIso' e h₁ h₂).hom = rightHomologyMap' e.hom h₁ h₂

instance CategoryTheory.ShortComplex.isIso_rightHomologyMap'_of_isIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [IsIso φ] (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : IsIso (rightHomologyMap' φ h₁ h₂)

def CategoryTheory.ShortComplex.opcyclesMapIso' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : h₁.Q ≅ h₂.Q

An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the Q fields of right homology data of S₁ and S₂.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso'_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (opcyclesMapIso' e h₁ h₂).hom = opcyclesMap' e.hom h₁ h₂

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso'_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (opcyclesMapIso' e h₁ h₂).inv = opcyclesMap' e.inv h₂ h₁

instance CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [IsIso φ] (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : IsIso (opcyclesMap' φ h₁ h₂)

noncomputable def CategoryTheory.ShortComplex.rightHomologyMapIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : S₁.rightHomology ≅ S₂.rightHomology

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

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : (rightHomologyMapIso e).hom = rightHomologyMap e.hom

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : (rightHomologyMapIso e).inv = rightHomologyMap e.inv

instance CategoryTheory.ShortComplex.isIso_rightHomologyMap_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasRightHomology] [S₂.HasRightHomology] : IsIso (rightHomologyMap φ)

noncomputable def CategoryTheory.ShortComplex.opcyclesMapIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : S₁.opcycles ≅ S₂.opcycles

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

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : (opcyclesMapIso e).inv = opcyclesMap e.inv

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : (opcyclesMapIso e).hom = opcyclesMap e.hom

instance CategoryTheory.ShortComplex.isIso_opcyclesMap_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasRightHomology] [S₂.HasRightHomology] : IsIso (opcyclesMap φ)

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] : S.rightHomology ≅ h.H

The isomorphism S.rightHomology ≅ h.H induced by a right homology data h for a short complex S.

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] : S.opcycles ≅ h.Q

The isomorphism S.opcycles ≅ h.Q induced by a right homology data h for a short complex S.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] : CategoryStruct.comp h.p h.opcyclesIso.inv = S.pOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] {Z : C} (h✝ : S.opcycles ⟶ Z) : CategoryStruct.comp h.p (CategoryStruct.comp h.opcyclesIso.inv h✝) = CategoryStruct.comp S.pOpcycles h✝

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] : CategoryStruct.comp S.pOpcycles h.opcyclesIso.hom = h.p

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] {Z : C} (h✝ : h.Q ⟶ Z) : CategoryStruct.comp S.pOpcycles (CategoryStruct.comp h.opcyclesIso.hom h✝) = CategoryStruct.comp h.p h✝

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] : CategoryStruct.comp h.rightHomologyIso.inv S.rightHomologyι = CategoryStruct.comp h.ι h.opcyclesIso.inv

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] {Z : C} (h✝ : S.opcycles ⟶ Z) : CategoryStruct.comp h.rightHomologyIso.inv (CategoryStruct.comp S.rightHomologyι h✝) = CategoryStruct.comp h.ι (CategoryStruct.comp h.opcyclesIso.inv h✝)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] : CategoryStruct.comp h.rightHomologyIso.hom h.ι = CategoryStruct.comp S.rightHomologyι h.opcyclesIso.hom

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_ι_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] {Z : C} (h✝ : h.Q ⟶ Z) : CategoryStruct.comp h.rightHomologyIso.hom (CategoryStruct.comp h.ι h✝) = CategoryStruct.comp S.rightHomologyι (CategoryStruct.comp h.opcyclesIso.hom h✝)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_eq {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : rightHomologyMap φ = CategoryStruct.comp h₁.rightHomologyIso.hom (CategoryStruct.comp γ.φH h₂.rightHomologyIso.inv)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_eq {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : opcyclesMap φ = CategoryStruct.comp h₁.opcyclesIso.hom (CategoryStruct.comp γ.φQ h₂.opcyclesIso.inv)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_comm {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : CategoryStruct.comp (rightHomologyMap φ) h₂.rightHomologyIso.hom = CategoryStruct.comp h₁.rightHomologyIso.hom γ.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_comm {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : CategoryStruct.comp (opcyclesMap φ) h₂.opcyclesIso.hom = CategoryStruct.comp h₁.opcyclesIso.hom γ.φQ

noncomputable def CategoryTheory.ShortComplex.rightHomologyFunctor (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : Functor (ShortComplex C) C

The right homology functor ShortComplex C ⥤ C, where the right homology of a short complex S is understood as a kernel of the obvious map S.fromOpcycles : S.opcycles ⟶ S.X₃ where S.opcycles is a cokernel of S.f : S.X₁ ⟶ S.X₂.

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyFunctor_obj (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (S : ShortComplex C) : (rightHomologyFunctor C).obj S = S.rightHomology

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyFunctor_map (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X✝ Y✝ : ShortComplex C} (φ : X✝ ⟶ Y✝) : (rightHomologyFunctor C).map φ = rightHomologyMap φ

noncomputable def CategoryTheory.ShortComplex.opcyclesFunctor (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : Functor (ShortComplex C) C

The opcycles functor ShortComplex C ⥤ C which sends a short complex S to S.opcycles which is a cokernel of S.f : S.X₁ ⟶ S.X₂.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesFunctor_obj (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (S : ShortComplex C) : (opcyclesFunctor C).obj S = S.opcycles

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesFunctor_map (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X✝ Y✝ : ShortComplex C} (φ : X✝ ⟶ Y✝) : (opcyclesFunctor C).map φ = opcyclesMap φ

noncomputable def CategoryTheory.ShortComplex.rightHomologyιNatTrans (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : rightHomologyFunctor C ⟶ opcyclesFunctor C

The natural transformation S.rightHomology ⟶ S.opcycles for all short complexes S.

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyιNatTrans_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (S : ShortComplex C) : (rightHomologyιNatTrans C).app S = S.rightHomologyι

noncomputable def CategoryTheory.ShortComplex.pOpcyclesNatTrans (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : π₂ ⟶ opcyclesFunctor C

The natural transformation S.X₂ ⟶ S.opcycles for all short complexes S.

@[simp]

theorem CategoryTheory.ShortComplex.pOpcyclesNatTrans_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (S : ShortComplex C) : (pOpcyclesNatTrans C).app S = S.pOpcycles

noncomputable def CategoryTheory.ShortComplex.fromOpcyclesNatTrans (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : opcyclesFunctor C ⟶ π₃

The natural transformation S.opcycles ⟶ S.X₃ for all short complexes S.

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcyclesNatTrans_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (S : ShortComplex C) : (fromOpcyclesNatTrans C).app S = S.fromOpcycles

def CategoryTheory.ShortComplex.LeftHomologyMapData.op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) : RightHomologyMapData (opMap φ) h₂.op h₁.op

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) : ψ.op.φQ = ψ.φK.op

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.op_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) : ψ.op.φH = ψ.φH.op

def CategoryTheory.ShortComplex.LeftHomologyMapData.unop {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) : RightHomologyMapData (unopMap φ) h₂.unop h₁.unop

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) : ψ.unop.φQ = ψ.φK.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) : ψ.unop.φH = ψ.φH.unop

def CategoryTheory.ShortComplex.RightHomologyMapData.op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) : LeftHomologyMapData (opMap φ) h₂.op h₁.op

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.op_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) : ψ.op.φH = ψ.φH.op

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.op_φK {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) : ψ.op.φK = ψ.φQ.op

def CategoryTheory.ShortComplex.RightHomologyMapData.unop {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) : LeftHomologyMapData (unopMap φ) h₂.unop h₁.unop

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.unop_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) : ψ.unop.φH = ψ.φH.unop

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.unop_φK {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) : ψ.unop.φK = ψ.φQ.unop

noncomputable def CategoryTheory.ShortComplex.rightHomologyOpIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasLeftHomology] : S.op.rightHomology ≅ Opposite.op S.leftHomology

The right homology in the opposite category of the opposite of a short complex identifies to the left homology of this short complex.

noncomputable def CategoryTheory.ShortComplex.leftHomologyOpIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.op.leftHomology ≅ Opposite.op S.rightHomology

The left homology in the opposite category of the opposite of a short complex identifies to the right homology of this short complex.

noncomputable def CategoryTheory.ShortComplex.opcyclesOpIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasLeftHomology] : S.op.opcycles ≅ Opposite.op S.cycles

The opcycles in the opposite category of the opposite of a short complex identifies to the cycles of this short complex.

noncomputable def CategoryTheory.ShortComplex.cyclesOpIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : S.op.cycles ≅ Opposite.op S.opcycles

The cycles in the opposite category of the opposite of a short complex identifies to the opcycles of this short complex.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasLeftHomology] : CategoryStruct.comp S.opcyclesOpIso.hom S.toCycles.op = S.op.fromOpcycles

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasLeftHomology] {Z : Cᵒᵖ} (h : Opposite.op S.X₁ ⟶ Z) : CategoryStruct.comp S.opcyclesOpIso.hom (CategoryStruct.comp S.toCycles.op h) = CategoryStruct.comp S.op.fromOpcycles h

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : CategoryStruct.comp S.fromOpcycles.op S.cyclesOpIso.inv = S.op.toCycles

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {Z : Cᵒᵖ} (h : S.op.cycles ⟶ Z) : CategoryStruct.comp S.fromOpcycles.op (CategoryStruct.comp S.cyclesOpIso.inv h) = CategoryStruct.comp S.op.toCycles h

@[simp]

theorem CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasLeftHomology] : CategoryStruct.comp S.op.pOpcycles S.opcyclesOpIso.hom = S.iCycles.op

@[simp]

theorem CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasLeftHomology] {Z : Cᵒᵖ} (h : Opposite.op S.cycles ⟶ Z) : CategoryStruct.comp S.op.pOpcycles (CategoryStruct.comp S.opcyclesOpIso.hom h) = CategoryStruct.comp S.iCycles.op h

@[simp]

theorem CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : CategoryStruct.comp S.cyclesOpIso.inv S.op.iCycles = S.pOpcycles.op

@[simp]

theorem CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {Z : Cᵒᵖ} (h : S.op.X₂ ⟶ Z) : CategoryStruct.comp S.cyclesOpIso.inv (CategoryStruct.comp S.op.iCycles h) = CategoryStruct.comp S.pOpcycles.op h

theorem CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] : CategoryStruct.comp (opcyclesMap (opMap φ)) S₁.opcyclesOpIso.hom = CategoryStruct.comp S₂.opcyclesOpIso.hom (cyclesMap φ).op

theorem CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] {Z : Cᵒᵖ} (h : Opposite.op S₁.cycles ⟶ Z) : CategoryStruct.comp (opcyclesMap (opMap φ)) (CategoryStruct.comp S₁.opcyclesOpIso.hom h) = CategoryStruct.comp S₂.opcyclesOpIso.hom (CategoryStruct.comp (cyclesMap φ).op h)

theorem CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] : CategoryStruct.comp (cyclesMap φ).op S₁.opcyclesOpIso.inv = CategoryStruct.comp S₂.opcyclesOpIso.inv (opcyclesMap (opMap φ))

theorem CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] {Z : Cᵒᵖ} (h : S₁.op.opcycles ⟶ Z) : CategoryStruct.comp (cyclesMap φ).op (CategoryStruct.comp S₁.opcyclesOpIso.inv h) = CategoryStruct.comp S₂.opcyclesOpIso.inv (CategoryStruct.comp (opcyclesMap (opMap φ)) h)

theorem CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : CategoryStruct.comp (opcyclesMap φ).op S₁.cyclesOpIso.inv = CategoryStruct.comp S₂.cyclesOpIso.inv (cyclesMap (opMap φ))

theorem CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] {Z : Cᵒᵖ} (h : S₁.op.cycles ⟶ Z) : CategoryStruct.comp (opcyclesMap φ).op (CategoryStruct.comp S₁.cyclesOpIso.inv h) = CategoryStruct.comp S₂.cyclesOpIso.inv (CategoryStruct.comp (cyclesMap (opMap φ)) h)

theorem CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : CategoryStruct.comp (cyclesMap (opMap φ)) S₁.cyclesOpIso.hom = CategoryStruct.comp S₂.cyclesOpIso.hom (opcyclesMap φ).op

theorem CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] {Z : Cᵒᵖ} (h : Opposite.op S₁.opcycles ⟶ Z) : CategoryStruct.comp (cyclesMap (opMap φ)) (CategoryStruct.comp S₁.cyclesOpIso.hom h) = CategoryStruct.comp S₂.cyclesOpIso.hom (CategoryStruct.comp (opcyclesMap φ).op h)

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) : (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

theorem CategoryTheory.ShortComplex.leftHomologyMap_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] : (leftHomologyMap φ).op = CategoryStruct.comp S₂.rightHomologyOpIso.inv (CategoryStruct.comp (rightHomologyMap (opMap φ)) S₁.rightHomologyOpIso.hom)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

theorem CategoryTheory.ShortComplex.rightHomologyMap_op {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : (rightHomologyMap φ).op = CategoryStruct.comp S₂.leftHomologyOpIso.inv (CategoryStruct.comp (leftHomologyMap (opMap φ)) S₁.leftHomologyOpIso.hom)

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

If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a right homology data for S₁ induces a right homology data for S₂ with the same Q and H fields. This is obtained by dualising LeftHomologyData.ofEpiOfIsIsoOfMono'. The inverse construction is ofEpiOfIsIsoOfMono'.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).Q = h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).H = h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).p = CategoryStruct.comp (inv φ.τ₂) h.p

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).ι = h.ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_g' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).g' = CategoryStruct.comp h.g' φ.τ₃

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

If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a right homology data for S₂ induces a right homology data for S₁ with the same Q and H fields. This is obtained by dualising LeftHomologyData.ofEpiOfIsIsoOfMono. The inverse construction is ofEpiOfIsIsoOfMono.

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_Q {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).Q = h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_H {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).H = h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_p {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).p = CategoryStruct.comp φ.τ₂ h.p

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_ι {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).ι = h.ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_g'_τ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : CategoryStruct.comp (ofEpiOfIsIsoOfMono' φ h).g' φ.τ₃ = h.g'

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

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

theorem CategoryTheory.ShortComplex.hasRightHomology_of_epi_of_isIso_of_mono {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : S₂.HasRightHomology

theorem CategoryTheory.ShortComplex.hasRightHomology_of_epi_of_isIso_of_mono' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₂.HasRightHomology] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : S₁.HasRightHomology

theorem CategoryTheory.ShortComplex.hasRightHomology_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology] : S₂.HasRightHomology

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).φH = CategoryStruct.id h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono φ h).φQ = CategoryStruct.id h.Q

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).φQ = CategoryStruct.id (RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).φH = CategoryStruct.id (RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H

instance CategoryTheory.ShortComplex.instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : IsIso (rightHomologyMap' φ h₁ h₂)

instance CategoryTheory.ShortComplex.instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : IsIso (rightHomologyMap φ)

If a morphism of short complexes φ : S₁ ⟶ S₂ is such that φ.τ₁ is epi, φ.τ₂ is an iso, and φ.τ₃ is mono, then the induced morphism on right homology is an isomorphism.

noncomputable def CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels Cᵒᵖ] [Limits.HasCokernels Cᵒᵖ] : (rightHomologyFunctor C).op ≅ (opFunctor C).comp (leftHomologyFunctor Cᵒᵖ)

The opposite of the right homology functor is the left homology functor.

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_hom_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels Cᵒᵖ] [Limits.HasCokernels Cᵒᵖ] (X : (ShortComplex C)ᵒᵖ) : (rightHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).leftHomologyOpIso.inv

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_inv_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels Cᵒᵖ] [Limits.HasCokernels Cᵒᵖ] (X : (ShortComplex C)ᵒᵖ) : (rightHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).leftHomologyOpIso.hom

noncomputable def CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels Cᵒᵖ] [Limits.HasCokernels Cᵒᵖ] : (leftHomologyFunctor C).op ≅ (opFunctor C).comp (rightHomologyFunctor Cᵒᵖ)

The opposite of the left homology functor is the right homology functor.

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_hom_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels Cᵒᵖ] [Limits.HasCokernels Cᵒᵖ] (X : (ShortComplex C)ᵒᵖ) : (leftHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).rightHomologyOpIso.inv

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_inv_app (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasKernels Cᵒᵖ] [Limits.HasCokernels Cᵒᵖ] (X : (ShortComplex C)ᵒᵖ) : (leftHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).rightHomologyOpIso.hom

noncomputable def CategoryTheory.ShortComplex.descOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] : S.opcycles ⟶ A

A morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism S.opcycles ⟶ A.

@[simp]

theorem CategoryTheory.ShortComplex.p_descOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] : CategoryStruct.comp S.pOpcycles (S.descOpcycles k hk) = k

@[simp]

theorem CategoryTheory.ShortComplex.p_descOpcycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp S.pOpcycles (CategoryStruct.comp (S.descOpcycles k hk) h) = CategoryStruct.comp k h

theorem CategoryTheory.ShortComplex.descOpcycles_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] {A' : C} (α : A ⟶ A') : CategoryStruct.comp (S.descOpcycles k hk) α = S.descOpcycles (CategoryStruct.comp k α) ⋯

theorem CategoryTheory.ShortComplex.descOpcycles_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] {A' : C} (α : A ⟶ A') {Z : C} (h : A' ⟶ Z) : CategoryStruct.comp (S.descOpcycles k hk) (CategoryStruct.comp α h) = CategoryStruct.comp (S.descOpcycles (CategoryStruct.comp k α) ⋯) h

noncomputable def CategoryTheory.ShortComplex.opcyclesIsCokernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : Limits.IsColimit (Limits.CokernelCofork.ofπ S.pOpcycles ⋯)

Via S.pOpcycles : S.X₂ ⟶ S.opcycles, the object S.opcycles identifies to the cokernel of S.f : S.X₁ ⟶ S.X₂.

noncomputable def CategoryTheory.ShortComplex.opcyclesIsoCokernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] [Limits.HasCokernel S.f] : S.opcycles ≅ Limits.cokernel S.f

The canonical isomorphism S.opcycles ≅ cokernel S.f.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoCokernel_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] [Limits.HasCokernel S.f] : S.opcyclesIsoCokernel.hom = S.descOpcycles (Limits.cokernel.π S.f) ⋯

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoCokernel_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] [Limits.HasCokernel S.f] : S.opcyclesIsoCokernel.inv = Limits.cokernel.desc S.f S.pOpcycles ⋯

noncomputable def CategoryTheory.ShortComplex.descRightHomology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] : S.rightHomology ⟶ A

The morphism S.rightHomology ⟶ A obtained from a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0.

theorem CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) [S.HasRightHomology] (x : S.X₃ ⟶ A) (hx : k = CategoryStruct.comp S.g x) : CategoryStruct.comp S.rightHomologyι (S.descOpcycles k ⋯) = 0

theorem CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : S.X₂ ⟶ A) [S.HasRightHomology] (x : S.X₃ ⟶ A) (hx : k = CategoryStruct.comp S.g x) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp S.rightHomologyι (CategoryStruct.comp (S.descOpcycles k ⋯) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : CategoryStruct.comp S.rightHomologyι S.fromOpcycles = 0

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] {Z : C} (h : S.X₃ ⟶ Z) : CategoryStruct.comp S.rightHomologyι (CategoryStruct.comp S.fromOpcycles h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.ShortComplex.rightHomologyIsKernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : Limits.IsLimit (Limits.KernelFork.ofι S.rightHomologyι ⋯)

Via S.rightHomologyι : S.rightHomology ⟶ S.opcycles, the object S.rightHomology identifies to the kernel of S.fromOpcycles : S.opcycles ⟶ S.X₃.

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_comp_descOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S S₁ : ShortComplex C} {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] (φ : S₁ ⟶ S) [S₁.HasRightHomology] : CategoryStruct.comp (opcyclesMap φ) (S.descOpcycles k hk) = S₁.descOpcycles (CategoryStruct.comp φ.τ₂ k) ⋯

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_comp_descOpcycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S S₁ : ShortComplex C} {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] (φ : S₁ ⟶ S) [S₁.HasRightHomology] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (opcyclesMap φ) (CategoryStruct.comp (S.descOpcycles k hk) h) = CategoryStruct.comp (S₁.descOpcycles (CategoryStruct.comp φ.τ₂ k) ⋯) h

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_inv_comp_descOpcycles {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] : CategoryStruct.comp h.opcyclesIso.inv (S.descOpcycles k hk) = h.descQ k hk

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_inv_comp_descOpcycles_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] {Z : C} (h✝ : A ⟶ Z) : CategoryStruct.comp h.opcyclesIso.inv (CategoryStruct.comp (S.descOpcycles k hk) h✝) = CategoryStruct.comp (h.descQ k hk) h✝

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_hom_comp_descQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [S.HasRightHomology] : CategoryStruct.comp h.opcyclesIso.hom (h.descQ k hk) = S.descOpcycles k hk

theorem CategoryTheory.ShortComplex.HasRightHomology.hasCokernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] : Limits.HasCokernel S.f

theorem CategoryTheory.ShortComplex.HasRightHomology.hasKernel {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] [Limits.HasCokernel S.f] : Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)

noncomputable def CategoryTheory.ShortComplex.rightHomologyIsoKernelDesc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasRightHomology] [Limits.HasCokernel S.f] [Limits.HasKernel (Limits.cokernel.desc S.f S.g ⋯)] : S.rightHomology ≅ Limits.kernel (Limits.cokernel.desc S.f S.g ⋯)

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

The following lemmas and instance gives a sufficient condition for a morphism of short complexes to induce an isomorphism on opcycles.

theorem CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₁ : Epi φ.τ₁) (h₁✝ : S₁.RightHomologyData) (h₂✝ : S₂.RightHomologyData) : IsIso (opcyclesMap' φ h₁✝ h₂✝)

theorem CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₁ : Epi φ.τ₁) [S₁.HasRightHomology] [S₂.HasRightHomology] : IsIso (opcyclesMap φ)

instance CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [IsIso φ.τ₂] [Epi φ.τ₁] [S₁.HasRightHomology] [S₂.HasRightHomology] : IsIso (opcyclesMap φ)