Left Homology of short complexes

Given a short complex S : ShortComplex C, which consists of two composable maps f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0, we shall define here the "left homology" S.leftHomology of S. For this, we introduce the notion of "left homology data". Such an h : S.LeftHomologyData consists of the data of morphisms i : K ⟶ X₂ and π : K ⟶ H such that i identifies K with the kernel of g : X₂ ⟶ X₃, and that π identifies H with the cokernel of the induced map f' : X₁ ⟶ K.

When such a S.LeftHomologyData exists, we shall say that [S.HasLeftHomology] and we define S.leftHomology to be the H field of a chosen left homology data. Similarly, we define S.cycles to be the K field.

The dual notion is defined in RightHomologyData.lean. 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.LeftHomologyData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : Type (max u_1 u_2)

• K : C

  a choice of kernel of S.g : S.X₂ ⟶ S.X₃

• H : C

  a choice of cokernel of the induced morphism S.f' : S.X₁ ⟶ K

• i : s.K ⟶ S.X₂

  the inclusion of cycles in S.X₂

• π : s.K ⟶ s.H

  the projection from cycles to the (left) homology

• wi : CategoryTheory.CategoryStruct.comp s.i S.g = 0

  the kernel condition for i

• hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι s.i (_ : CategoryTheory.CategoryStruct.comp s.i S.g = 0))

  i : K ⟶ S.X₂ is a kernel of g : S.X₂ ⟶ S.X₃

• wπ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.lift s.hi (CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) s.π = 0

  the cokernel condition for π

• hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ s.π (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.lift s.hi (CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) s.π = 0))

  π : K ⟶ H is a cokernel of the induced morphism S.f' : S.X₁ ⟶ K

A left homology data for a short complex S consists of morphisms i : K ⟶ S.X₂ and π : K ⟶ H such that i identifies K to the kernel of g : S.X₂ ⟶ S.X₃, and that π identifies H to the cokernel of the induced map f' : S.X₁ ⟶ K

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_K {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).K = CategoryTheory.Limits.kernel S.g

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_H {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).H = CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_π {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).π = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).i = CategoryTheory.Limits.kernel.ι S.g

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : CategoryTheory.ShortComplex.LeftHomologyData S

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : CategoryTheory.ShortComplex.LeftHomologyData S) {Z : C} (h : self.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.lift self.hi (CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) (CategoryTheory.CategoryStruct.comp self.π h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.wi_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : CategoryTheory.ShortComplex.LeftHomologyData S) {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp S.g h) = CategoryTheory.CategoryStruct.comp 0 h

instance CategoryTheory.ShortComplex.LeftHomologyData.instMonoKX₂I {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) : CategoryTheory.Mono h.i

instance CategoryTheory.ShortComplex.LeftHomologyData.instEpiKHπ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) : CategoryTheory.Epi h.π

def CategoryTheory.ShortComplex.LeftHomologyData.liftK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) : A ⟶ h.K

Any morphism k : A ⟶ S.X₂ that is a cycle (i.e. k ≫ S.g = 0) lifts to a morphism A ⟶ K

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.liftK_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k hk) (CategoryTheory.CategoryStruct.comp h.i h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.liftK_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k hk) h.i = k

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

The (left) homology class A ⟶ H attached to a cycle k : A ⟶ S.X₂

def CategoryTheory.ShortComplex.LeftHomologyData.f' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) : S.X₁ ⟶ h.K

Given h : LeftHomologyData S, this is morphism S.X₁ ⟶ h.K induced by S.f : S.X₁ ⟶ S.X₂ and the fact that h.K is a kernel of S.g : S.X₂ ⟶ S.X₃.

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) (CategoryTheory.CategoryStruct.comp h.i h) = CategoryTheory.CategoryStruct.comp S.f h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) h.i = S.f

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_π_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {Z : C} (h : h.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) (CategoryTheory.CategoryStruct.comp h.π h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_π {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) h.π = 0

theorem CategoryTheory.ShortComplex.LeftHomologyData.liftK_π_eq_zero_of_boundary_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (x : A ⟶ S.X₁) (hx : k = CategoryTheory.CategoryStruct.comp x S.f) {Z : C} (h : h.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k (_ : CategoryTheory.CategoryStruct.comp k S.g = 0)) (CategoryTheory.CategoryStruct.comp h.π h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.LeftHomologyData.liftK_π_eq_zero_of_boundary {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (x : A ⟶ S.X₁) (hx : k = CategoryTheory.CategoryStruct.comp x S.f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k (_ : CategoryTheory.CategoryStruct.comp k S.g = 0)) h.π = 0

def CategoryTheory.ShortComplex.LeftHomologyData.hπ' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ h.π (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) h.π = 0))

For h : S.LeftHomologyData, this is a restatement of h.hπ, saying that π : h.K ⟶ h.H is a cokernel of h.f' : S.X₁ ⟶ h.K.

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

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.π_descH_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : h.K ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) k = 0) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.descH h k hk) h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.π_descH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : h.K ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h) k = 0) : CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.ShortComplex.LeftHomologyData.descH h k hk) = k

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

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).i = CategoryTheory.CategoryStruct.id S.X₂

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_K {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).K = S.X₂

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0) : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).i = CategoryTheory.CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_π {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0) : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).π = CategoryTheory.Limits.cokernel.π S.f

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_K {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0) : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).K = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_H {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0) : (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).H = CategoryTheory.Limits.cokernel S.f

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

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_π {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).π = CategoryTheory.CategoryStruct.id c.pt

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).i = CategoryTheory.Limits.Fork.ι c

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

A short complex S has left homology when there exists a S.LeftHomologyData

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

A chosen S.LeftHomologyData for a short complex S that has left homology

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

instance CategoryTheory.ShortComplex.HasLeftHomology.of_hasKernel_of_hasCokernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : CategoryTheory.ShortComplex.HasLeftHomology S

instance CategoryTheory.ShortComplex.HasLeftHomology.of_hasCokernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasCokernel f] : CategoryTheory.ShortComplex.HasLeftHomology (CategoryTheory.ShortComplex.mk f 0 (_ : CategoryTheory.CategoryStruct.comp f 0 = 0))

instance CategoryTheory.ShortComplex.HasLeftHomology.of_hasKernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {Y : C} {Z : C} (g : Y ⟶ Z) (X : C) [CategoryTheory.Limits.HasKernel g] : CategoryTheory.ShortComplex.HasLeftHomology (CategoryTheory.ShortComplex.mk 0 g (_ : CategoryTheory.CategoryStruct.comp 0 g = 0))

instance CategoryTheory.ShortComplex.HasLeftHomology.of_zeros {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) (Z : C) : CategoryTheory.ShortComplex.HasLeftHomology (CategoryTheory.ShortComplex.mk 0 0 (_ : CategoryTheory.CategoryStruct.comp 0 0 = 0))

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

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

  the induced map on cycles

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

  the induced map on left homology

• commi : CategoryTheory.CategoryStruct.comp s.φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂

  commutation with i

• commf' : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) s.φK = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.ShortComplex.LeftHomologyData.f' h₂)

  commutation with f'

• commπ : CategoryTheory.CategoryStruct.comp h₁.π s.φH = CategoryTheory.CategoryStruct.comp s.φK h₂.π

  commutation with π

Given left homology data h₁ and h₂ for two short complexes S₁ and S₂, a LeftHomologyMapData for a morphism φ : S₁ ⟶ S₂ consists of a description of the induced morphisms on the K (cycles) and H (left homology) fields of h₁ and h₂.

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.commf'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) (CategoryTheory.CategoryStruct.comp self.φK h) = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.commi_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) {Z : C} (h : S₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.φK (CategoryTheory.CategoryStruct.comp h₂.i h) = CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

The composition of left homology map data.

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

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

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : (CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φK = φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : (CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂

def CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : CategoryTheory.ShortComplex.LeftHomologyMapData φ (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S₁ hf₁ hg₁) (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S₂ hf₂ hg₂)

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

@[simp]

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

@[simp]

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

def CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : CategoryTheory.ShortComplex.LeftHomologyMapData φ (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (CategoryTheory.ShortComplex.LeftHomologyData.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 left 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.LeftHomologyMapData.ofIsLimitKernelFork_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g) (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g) (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)) : (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φK = f

@[simp]

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

def CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g) (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g) (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)) : CategoryTheory.ShortComplex.LeftHomologyMapData φ (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁) (CategoryTheory.ShortComplex.LeftHomologyData.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 left 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.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φK = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).K

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φK = CategoryTheory.Limits.Fork.ι c

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φH = CategoryTheory.Limits.Fork.ι c

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

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

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

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

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

The cycles of a short complex, given by the K field of a chosen left homology data.

noncomputable def CategoryTheory.ShortComplex.leftHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.ShortComplex.cycles S ⟶ CategoryTheory.ShortComplex.leftHomology S

The "homology class" map S.cycles ⟶ S.leftHomology.

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

The inclusion S.cycles ⟶ S.X₂.

noncomputable def CategoryTheory.ShortComplex.toCycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : S.X₁ ⟶ CategoryTheory.ShortComplex.cycles S

The "boundaries" map S.X₁ ⟶ S.cycles. (Note that in this homology API, we make no use of the "image" of this morphism, which under some categorical assumptions would be a subobject of S.X₂ contained in S.cycles.)

@[simp]

theorem CategoryTheory.ShortComplex.iCycles_g_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.CategoryStruct.comp S.g h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.iCycles_g {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) S.g = 0

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) h) = CategoryTheory.CategoryStruct.comp S.f h

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.ShortComplex.iCycles S) = S.f

instance CategoryTheory.ShortComplex.instMonoCyclesX₂ICycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.Mono (CategoryTheory.ShortComplex.iCycles S)

instance CategoryTheory.ShortComplex.instEpiCyclesLeftHomologyLeftHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.Epi (CategoryTheory.ShortComplex.leftHomologyπ S)

theorem CategoryTheory.ShortComplex.leftHomology_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {A : C} (f₁ : CategoryTheory.ShortComplex.leftHomology S ⟶ A) (f₂ : CategoryTheory.ShortComplex.leftHomology S ⟶ A) : f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) f₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) f₂

theorem CategoryTheory.ShortComplex.leftHomology_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {A : C} (f₁ : CategoryTheory.ShortComplex.leftHomology S ⟶ A) (f₂ : CategoryTheory.ShortComplex.leftHomology S ⟶ A) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) f₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) f₂) : f₁ = f₂

theorem CategoryTheory.ShortComplex.cycles_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {A : C} (f₁ : A ⟶ CategoryTheory.ShortComplex.cycles S) (f₂ : A ⟶ CategoryTheory.ShortComplex.cycles S) : f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.ShortComplex.iCycles S) = CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.ShortComplex.iCycles S)

theorem CategoryTheory.ShortComplex.cycles_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {A : C} (f₁ : A ⟶ CategoryTheory.ShortComplex.cycles S) (f₂ : A ⟶ CategoryTheory.ShortComplex.cycles S) (h : CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.ShortComplex.iCycles S) = CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.ShortComplex.iCycles S)) : f₁ = f₂

theorem CategoryTheory.ShortComplex.isIso_iCycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.iCycles S)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoX₂_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) : (CategoryTheory.ShortComplex.cyclesIsoX₂ S hg).hom = CategoryTheory.ShortComplex.iCycles S

noncomputable def CategoryTheory.ShortComplex.cyclesIsoX₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) : CategoryTheory.ShortComplex.cycles S ≅ S.X₂

When S.g = 0, this is the canonical isomorphism S.cycles ≅ S.X₂ induced by S.iCycles.

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoX₂_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) {Z : C} (h : CategoryTheory.ShortComplex.cycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesIsoX₂ S hg).inv h) = h

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoX₂_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) (CategoryTheory.ShortComplex.cyclesIsoX₂ S hg).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.cycles S)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoX₂_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesIsoX₂ S hg).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) h) = h

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoX₂_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hg : S.g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesIsoX₂ S hg).inv (CategoryTheory.ShortComplex.iCycles S) = CategoryTheory.CategoryStruct.id S.X₂

theorem CategoryTheory.ShortComplex.isIso_leftHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyπ S)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) : (CategoryTheory.ShortComplex.cyclesIsoLeftHomology S hf).hom = CategoryTheory.ShortComplex.leftHomologyπ S

noncomputable def CategoryTheory.ShortComplex.cyclesIsoLeftHomology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) : CategoryTheory.ShortComplex.cycles S ≅ CategoryTheory.ShortComplex.leftHomology S

When S.f = 0, this is the canonical isomorphism S.cycles ≅ S.leftHomology induced by S.leftHomologyπ.

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) {Z : C} (h : CategoryTheory.ShortComplex.cycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesIsoLeftHomology S hf).inv h) = h

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) (CategoryTheory.ShortComplex.cyclesIsoLeftHomology S hf).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.cycles S)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesIsoLeftHomology S hf).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) h) = h

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] (hf : S.f = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesIsoLeftHomology S hf).inv (CategoryTheory.ShortComplex.leftHomologyπ S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.leftHomology S)

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

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

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

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap'_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) {Z : C} (h : S₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) (CategoryTheory.CategoryStruct.comp h₂.i h) = CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap'_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.f'_cyclesMap'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) {Z : C} (h : h₂.K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h) = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.f'_cyclesMap' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.ShortComplex.LeftHomologyData.f' h₂)

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) {Z : C} (h : h₂.H ⟶ Z) : CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) (CategoryTheory.CategoryStruct.comp h₂.π h)

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyπ_naturality' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) : CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h₂.π

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

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : S₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S₁) (CategoryTheory.CategoryStruct.comp φ.τ₂ h)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.ShortComplex.iCycles S₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S₁) φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.cycles S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) h) = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S₁) (CategoryTheory.ShortComplex.cyclesMap φ) = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.ShortComplex.toCycles S₂)

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyπ_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyπ_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S₁) (CategoryTheory.ShortComplex.leftHomologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.ShortComplex.leftHomologyπ S₂)

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

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ = γ.φK

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.leftHomology S)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.cycles S)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem CategoryTheory.ShortComplex.leftHomologyMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.ShortComplex.HasLeftHomology S₃] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₂) h)

@[simp]

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

theorem CategoryTheory.ShortComplex.cyclesMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.ShortComplex.HasLeftHomology S₃] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) {Z : C} (h : CategoryTheory.ShortComplex.cycles S₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₂) h)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMapIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : (CategoryTheory.ShortComplex.leftHomologyMapIso e).hom = CategoryTheory.ShortComplex.leftHomologyMap e.hom

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMapIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : (CategoryTheory.ShortComplex.leftHomologyMapIso e).inv = CategoryTheory.ShortComplex.leftHomologyMap e.inv

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMapIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : (CategoryTheory.ShortComplex.cyclesMapIso e).inv = CategoryTheory.ShortComplex.cyclesMap e.inv

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMapIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : (CategoryTheory.ShortComplex.cyclesMapIso e).hom = CategoryTheory.ShortComplex.cyclesMap e.hom

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

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

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

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.ShortComplex.leftHomology S ≅ h.H

The isomorphism S.leftHomology ≅ h.H induced by a left homology data h for a short complex S.

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.ShortComplex.cycles S ≅ h.K

The isomorphism S.cycles ≅ h.K induced by a left homology data h for a short complex S.

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom (CategoryTheory.CategoryStruct.comp h.i h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom h.i = CategoryTheory.ShortComplex.iCycles S

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) h) = CategoryTheory.CategoryStruct.comp h.i h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv (CategoryTheory.ShortComplex.iCycles S) = h.i

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : h.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom (CategoryTheory.CategoryStruct.comp h.π h)

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom h.π

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.π_comp_leftHomologyIso_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) h)

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.π_comp_leftHomologyIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv (CategoryTheory.ShortComplex.leftHomologyπ S)

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : CategoryTheory.ShortComplex.leftHomologyMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h₁).hom (CategoryTheory.CategoryStruct.comp γ.φH (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h₂).inv)

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : CategoryTheory.ShortComplex.cyclesMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h₁).hom (CategoryTheory.CategoryStruct.comp γ.φK (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h₂).inv)

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso h₁).hom γ.φH

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h₁).hom γ.φK

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : ∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.leftHomologyFunctor C).map φ = CategoryTheory.ShortComplex.leftHomologyMap φ

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

The left homology functor ShortComplex C ⥤ C, where the left homology of a short complex S is understood as a cokernel of the obvious map S.toCycles : S.X₁ ⟶ S.cycles where S.cycles is a kernel of S.g : S.X₂ ⟶ S.X₃.

@[simp]

theorem CategoryTheory.ShortComplex.cyclesFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : ∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.cyclesFunctor C).map φ = CategoryTheory.ShortComplex.cyclesMap φ

@[simp]

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

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

The cycles functor ShortComplex C ⥤ C which sends a short complex S to S.cycles which is a kernel of S.g : S.X₂ ⟶ S.X₃.

@[simp]

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

noncomputable def CategoryTheory.ShortComplex.leftHomologyπNatTrans (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.cyclesFunctor C ⟶ CategoryTheory.ShortComplex.leftHomologyFunctor C

The natural transformation S.cycles ⟶ S.leftHomology for all short complexes S.

@[simp]

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

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

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

@[simp]

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

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

The natural transformation S.X₁ ⟶ S.cycles for all short complexes S.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

instance CategoryTheory.ShortComplex.instIsIsoHLeftHomologyMap' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂)

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

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

noncomputable def CategoryTheory.ShortComplex.liftCycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] : A ⟶ CategoryTheory.ShortComplex.cycles S

A morphism k : A ⟶ S.X₂ such that k ≫ S.g = 0 lifts to a morphism A ⟶ S.cycles.

@[simp]

theorem CategoryTheory.ShortComplex.liftCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.ShortComplex.liftCycles_i {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) (CategoryTheory.ShortComplex.iCycles S) = k

theorem CategoryTheory.ShortComplex.comp_liftCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] {A' : C} (α : A' ⟶ A) {Z : C} (h : CategoryTheory.ShortComplex.cycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S (CategoryTheory.CategoryStruct.comp α k) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α k) S.g = 0)) h

theorem CategoryTheory.ShortComplex.comp_liftCycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] {A' : C} (α : A' ⟶ A) : CategoryTheory.CategoryStruct.comp α (CategoryTheory.ShortComplex.liftCycles S k hk) = CategoryTheory.ShortComplex.liftCycles S (CategoryTheory.CategoryStruct.comp α k) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α k) S.g = 0)

noncomputable def CategoryTheory.ShortComplex.cyclesIsKernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.ShortComplex.iCycles S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) S.g = 0))

Via S.iCycles : S.cycles ⟶ S.X₂, the object S.cycles identifies to the kernel of S.g : S.X₂ ⟶ S.X₃.

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoKernel_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Limits.HasKernel S.g] : (CategoryTheory.ShortComplex.cyclesIsoKernel S).inv = CategoryTheory.ShortComplex.liftCycles S (CategoryTheory.Limits.kernel.ι S.g) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) S.g = 0)

@[simp]

theorem CategoryTheory.ShortComplex.cyclesIsoKernel_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Limits.HasKernel S.g] : (CategoryTheory.ShortComplex.cyclesIsoKernel S).hom = CategoryTheory.Limits.kernel.lift S.g (CategoryTheory.ShortComplex.iCycles S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) S.g = 0)

noncomputable def CategoryTheory.ShortComplex.cyclesIsoKernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Limits.HasKernel S.g] : CategoryTheory.ShortComplex.cycles S ≅ CategoryTheory.Limits.kernel S.g

The canonical isomorphism S.cycles ≅ kernel S.g.

noncomputable def CategoryTheory.ShortComplex.liftLeftHomology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] : A ⟶ CategoryTheory.ShortComplex.leftHomology S

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

theorem CategoryTheory.ShortComplex.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) [CategoryTheory.ShortComplex.HasLeftHomology S] (x : A ⟶ S.X₁) (hx : k = CategoryTheory.CategoryStruct.comp x S.f) {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k (_ : CategoryTheory.CategoryStruct.comp k S.g = 0)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.liftCycles_leftHomologyπ_eq_zero_of_boundary {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) [CategoryTheory.ShortComplex.HasLeftHomology S] (x : A ⟶ S.X₁) (hx : k = CategoryTheory.CategoryStruct.comp x S.f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k (_ : CategoryTheory.CategoryStruct.comp k S.g = 0)) (CategoryTheory.ShortComplex.leftHomologyπ S) = 0

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_comp_leftHomologyπ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : CategoryTheory.ShortComplex.leftHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyπ S) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_comp_leftHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.ShortComplex.leftHomologyπ S) = 0

noncomputable def CategoryTheory.ShortComplex.leftHomologyIsCokernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.ShortComplex.leftHomologyπ S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.ShortComplex.leftHomologyπ S) = 0))

Via S.leftHomologyπ : S.cycles ⟶ S.leftHomology, the object S.leftHomology identifies to the cokernel of S.toCycles : S.X₁ ⟶ S.cycles.

@[simp]

theorem CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {S₁ : CategoryTheory.ShortComplex C} {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] (φ : S ⟶ S₁) [CategoryTheory.ShortComplex.HasLeftHomology S₁] {Z : C} (h : CategoryTheory.ShortComplex.cycles S₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S₁ (CategoryTheory.CategoryStruct.comp k φ.τ₂) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k φ.τ₂) S₁.g = 0)) h

@[simp]

theorem CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {S₁ : CategoryTheory.ShortComplex C} {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] (φ : S ⟶ S₁) [CategoryTheory.ShortComplex.HasLeftHomology S₁] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) (CategoryTheory.ShortComplex.cyclesMap φ) = CategoryTheory.ShortComplex.liftCycles S₁ (CategoryTheory.CategoryStruct.comp k φ.τ₂) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k φ.τ₂) S₁.g = 0)

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : h.K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k hk) h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).hom = CategoryTheory.ShortComplex.LeftHomologyData.liftK h k hk

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.lift_K_comp_cyclesIso_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] {Z : C} (h : CategoryTheory.ShortComplex.cycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k hk) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.liftCycles S k hk) h

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.lift_K_comp_cyclesIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.liftK h k hk) (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso h).inv = CategoryTheory.ShortComplex.liftCycles S k hk

theorem CategoryTheory.ShortComplex.HasLeftHomology.hasKernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] : CategoryTheory.Limits.HasKernel S.g

theorem CategoryTheory.ShortComplex.HasLeftHomology.hasCokernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Limits.HasKernel S.g] : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

noncomputable def CategoryTheory.ShortComplex.leftHomologyIsoCokernelLift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Limits.HasKernel S.g] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))] : CategoryTheory.ShortComplex.leftHomology S ≅ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

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

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

theorem CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso_of_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₂ : CategoryTheory.IsIso φ.τ₂) (h₃ : CategoryTheory.Mono φ.τ₃) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂)

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

instance CategoryTheory.ShortComplex.isIso_cyclesMap_of_isIso_of_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)