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

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

• 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 : self.K ⟶ S.X₂

  the inclusion of cycles in S.X₂

• π : self.K ⟶ self.H

  the projection from cycles to the (left) homology

• wi : CategoryStruct.comp self.i S.g = 0

  the kernel condition for i

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

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

• wπ : CategoryStruct.comp (self.hi.lift (Limits.KernelFork.ofι S.f ⋯)) self.π = 0

  the cokernel condition for π

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def CategoryTheory.ShortComplex.LeftHomologyData.liftK {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂) (hk : 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

Equations

• h.liftK k hk = h.hi.lift (CategoryTheory.Limits.KernelFork.ofι k hk)

@[simp]

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

@[simp]

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

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

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

Equations

• h.liftH k hk = CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.π

def CategoryTheory.ShortComplex.LeftHomologyData.f' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : 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₃.

Equations

• h.f' = h.liftK S.f ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def CategoryTheory.ShortComplex.LeftHomologyData.hπ' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.LeftHomologyData) : Limits.IsColimit (Limits.CokernelCofork.ofπ h.π ⋯)

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.

Equations

• h.hπ' = h.hπ

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

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

Equations

• h.descH k hk = h.hπ.desc (CategoryTheory.Limits.CokernelCofork.ofπ k hk)

@[simp]

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

@[simp]

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

• condition : Nonempty S.LeftHomologyData

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

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

Equations

• S.leftHomologyData = ⋯.some

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

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

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

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

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

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

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

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

  the induced map on cycles

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

  the induced map on left homology

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

  commutation with i

• commf' : CategoryStruct.comp h₁.f' self.φK = CategoryStruct.comp φ.τ₁ h₂.f'

  commutation with f'

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

  commutation with π

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁ h₂ = { φK := 0, φH := 0, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

The composition of left homology map data.

Equations

• ψ.comp ψ' = { φK := CategoryTheory.CategoryStruct.comp ψ.φK ψ'.φK, φH := CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

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

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

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

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

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂ = { φK := φ.τ₂, φH := φ.τ₂, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm = { φK := φ.τ₂, φH := f, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm = { φK := f, φH := f, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• S.leftHomology = S.leftHomologyData.H

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

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

Equations

• S.cycles = S.leftHomologyData.K

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

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

Equations

• S.leftHomologyπ = S.leftHomologyData.π

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

The inclusion S.cycles ⟶ S.X₂.

Equations

• S.iCycles = S.leftHomologyData.i

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

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

Equations

• S.toCycles = S.leftHomologyData.f'

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

Equations

• S.cyclesIsoX₂ hg = CategoryTheory.asIso S.iCycles

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• S.cyclesIsoLeftHomology hf = CategoryTheory.asIso S.leftHomologyπ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.leftHomologyMapData φ h₁ h₂ = default

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

Equations

• CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ = (CategoryTheory.ShortComplex.leftHomologyMapData φ h₁ h₂).φH

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

Equations

• CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ = (CategoryTheory.ShortComplex.leftHomologyMapData φ h₁ h₂).φK

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.leftHomologyMap φ = CategoryTheory.ShortComplex.leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData

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

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

Equations

• CategoryTheory.ShortComplex.cyclesMap φ = CategoryTheory.ShortComplex.cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• CategoryTheory.ShortComplex.cyclesMapIso e = { hom := CategoryTheory.ShortComplex.cyclesMap e.hom, inv := CategoryTheory.ShortComplex.cyclesMap e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

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

Equations

• h.cyclesIso = CategoryTheory.ShortComplex.cyclesMapIso' (CategoryTheory.Iso.refl S) S.leftHomologyData h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

noncomputable def CategoryTheory.ShortComplex.leftHomologyFunctor (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : Functor (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₃.

Equations

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ShortComplex.cyclesFunctor (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : Functor (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₃.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.leftHomologyπNatTrans C = { app := fun (S : CategoryTheory.ShortComplex C) => S.leftHomologyπ, naturality := ⋯ }

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.iCyclesNatTrans C = { app := fun (S : CategoryTheory.ShortComplex C) => S.iCycles, naturality := ⋯ }

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.toCyclesNatTrans C = { app := fun (S : CategoryTheory.ShortComplex C) => S.toCycles, naturality := ⋯ }

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

Equations

• CategoryTheory.ShortComplex.LeftHomologyData.ofIso e h₁ = CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono e.hom h₁

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

instance CategoryTheory.ShortComplex.instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : IsIso (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} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryStruct.comp k S.g = 0) [S.HasLeftHomology] : A ⟶ S.cycles

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

Equations

• S.liftCycles k hk = S.leftHomologyData.liftK k hk

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• S.cyclesIsKernel = S.leftHomologyData.hi

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

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

Equations

• S.cyclesIsoKernel = { hom := CategoryTheory.Limits.kernel.lift S.g S.iCycles ⋯, inv := S.liftCycles (CategoryTheory.Limits.kernel.ι S.g) ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• S.liftLeftHomology k hk = CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) S.leftHomologyπ

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• S.leftHomologyIsCokernel = S.leftHomologyData.hπ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• CategoryTheory.ShortComplex.leftHomologyIsoCokernelLift = (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).leftHomologyIso

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} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₃ : Mono φ.τ₃) (h₁ : S₁.LeftHomologyData) (h₂✝ : S₂.LeftHomologyData) : IsIso (cyclesMap' φ h₁ h₂✝)

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

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