Right Homology of short complexes

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

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

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

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

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

• Q : C

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

• H : C

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

• p : S.X₂ ⟶ self.Q

  the projection from S.X₂

• ι : self.H ⟶ self.Q

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

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

  the cokernel condition for p

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

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

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

  the kernel condition for ι

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_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] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)] : (CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).H = CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyData.descQ h k hk = h.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ k hk)

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyData.descH h k hk = CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.ShortComplex.RightHomologyData.descQ h k hk)

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyData.g' h = CategoryTheory.ShortComplex.RightHomologyData.descQ h S.g ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_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.RightHomologyData S) {A : C} (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp S.g x) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp h✝.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.descQ h✝ k ⋯) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_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.RightHomologyData S) {A : C} (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp S.g x) : CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.ShortComplex.RightHomologyData.descQ h k ⋯) = 0

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyData.hι' h = h.hι

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyData.liftH h k hk = h.hι.lift (CategoryTheory.Limits.KernelFork.ofι k hk)

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_Q {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.RightHomologyData.ofIsLimitKernelFork S hf c hc).Q = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofIsLimitKernelFork S hf c hc).ι = CategoryTheory.Limits.Fork.ι c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofIsLimitKernelFork S hf c hc).H = c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_p {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.RightHomologyData.ofIsLimitKernelFork S hf c hc).p = CategoryTheory.CategoryStruct.id S.X₂

def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_g' {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.RightHomologyData.g' (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc) = S.g

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_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] (hf : S.f = 0) : (CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).H = CategoryTheory.Limits.kernel S.g

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_p {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.RightHomologyData.ofHasKernel S hf).p = CategoryTheory.CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofHasKernel S hf).ι = CategoryTheory.Limits.kernel.ι S.g

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_Q {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.RightHomologyData.ofHasKernel S hf).Q = S.X₂

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q {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.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).Q = c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).H = c.pt

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_p {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.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).p = CategoryTheory.Limits.Cofork.π c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).ι = CategoryTheory.CategoryStruct.id c.pt

def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_g' {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.RightHomologyData.g' (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc) = 0

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S

When the second map S.g is zero, this is the right 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.RightHomologyData.ofZeros_Q {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.RightHomologyData.ofZeros S hf hg).Q = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofZeros S hf hg).ι = CategoryTheory.CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_p {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.RightHomologyData.ofZeros S hf hg).p = CategoryTheory.CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofZeros S hf hg).H = S.X₂

def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_g' {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.RightHomologyData.g' (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg) = 0

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

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

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

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

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

Equations

• CategoryTheory.ShortComplex.rightHomologyData S = Nonempty.some ⋯

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

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

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.HasRightHomology.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.HasRightHomology (CategoryTheory.ShortComplex.mk 0 g ⋯)

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.HasRightHomology.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.HasRightHomology (CategoryTheory.ShortComplex.mk f 0 ⋯)

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.HasRightHomology.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.HasRightHomology (CategoryTheory.ShortComplex.mk 0 0 ⋯)

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_ι {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.LeftHomologyData.op h).ι = h.π.op

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_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.LeftHomologyData.op h).H = Opposite.op h.H

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_Q {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.LeftHomologyData.op h).Q = Opposite.op h.K

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_p {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.LeftHomologyData.op h).p = h.i.op

def CategoryTheory.ShortComplex.LeftHomologyData.op {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.RightHomologyData (CategoryTheory.ShortComplex.op S)

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.op_g' {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.RightHomologyData.g' (CategoryTheory.ShortComplex.LeftHomologyData.op h) = (CategoryTheory.ShortComplex.LeftHomologyData.f' h).op

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_p {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.LeftHomologyData.unop h).p = h.i.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_ι {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.LeftHomologyData.unop h).ι = h.π.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_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.LeftHomologyData.unop h).H = h.H.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_Q {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.LeftHomologyData.unop h).Q = h.K.unop

def CategoryTheory.ShortComplex.LeftHomologyData.unop {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.RightHomologyData (CategoryTheory.ShortComplex.unop S)

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_g' {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.RightHomologyData.g' (CategoryTheory.ShortComplex.LeftHomologyData.unop h) = (CategoryTheory.ShortComplex.LeftHomologyData.f' h).unop

instance CategoryTheory.ShortComplex.instHasRightHomologyOppositeOppositeHasZeroMorphismsOppositeOp {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.HasRightHomology (CategoryTheory.ShortComplex.op S)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.ShortComplex.hasLeftHomology_iff_op {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.HasRightHomology (CategoryTheory.ShortComplex.op S)

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

theorem CategoryTheory.ShortComplex.hasLeftHomology_iff_unop {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.HasRightHomology (CategoryTheory.ShortComplex.unop S)

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

structure CategoryTheory.ShortComplex.RightHomologyMapData {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : Type u_2

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

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

  the induced map on opcycles

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

  the induced map on right homology

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

  commutation with p

• commg' : CategoryTheory.CategoryStruct.comp self.φQ (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₁) φ.τ₃

  commutation with g'

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

  commutation with ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp self.φH (CategoryTheory.CategoryStruct.comp h₂.ι h) = CategoryTheory.CategoryStruct.comp h₁.ι (CategoryTheory.CategoryStruct.comp self.φQ h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.commp_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp h₁.p (CategoryTheory.CategoryStruct.comp self.φQ h) = CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp h₂.p h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.commg'_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.φQ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₁) (CategoryTheory.CategoryStruct.comp φ.τ₃ h)

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.zero_φQ {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂).φQ = 0

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂).φH = 0

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.ShortComplex.RightHomologyMapData 0 h₁ h₂

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂ = { φQ := 0, φH := 0, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.id h = { φQ := CategoryTheory.CategoryStruct.id h.Q, φH := CategoryTheory.CategoryStruct.id h.H, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} {h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃) : (CategoryTheory.ShortComplex.RightHomologyMapData.comp ψ ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ {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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} {h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃) : (CategoryTheory.ShortComplex.RightHomologyMapData.comp ψ ψ').φQ = CategoryTheory.CategoryStruct.comp ψ.φQ ψ'.φQ

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} {h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃) : CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.CategoryStruct.comp φ φ') h₁ h₃

The composition of right homology map data.

Equations

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

instance CategoryTheory.ShortComplex.RightHomologyMapData.instSubsingletonRightHomologyMapData {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : Subsingleton (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.RightHomologyMapData.instInhabitedRightHomologyMapData {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : Inhabited (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)

Equations

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

instance CategoryTheory.ShortComplex.RightHomologyMapData.instUniqueRightHomologyMapData {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : Unique (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.instUniqueRightHomologyMapData φ h₁ h₂ = Unique.mk' (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} {γ₁ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂} {γ₂ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φH = γ₂.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ {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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} {γ₁ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂} {γ₂ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φQ = γ₂.φQ

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φQ {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.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φQ = φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData φ (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S₁ hf₁ hg₁) (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S₂ hf₂ hg₂)

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂ = { φQ := φ.τ₂, φH := φ.τ₂, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φQ {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.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φQ = φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φH = f

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData φ (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁) (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm = { φQ := φ.τ₂, φH := f, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φQ {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.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φQ = f

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData φ (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm = { φQ := f, φH := f, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φH = CategoryTheory.Limits.Fork.ι c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φQ {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.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φQ = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).Q

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc) (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg)

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ {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.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φQ = CategoryTheory.Limits.Cofork.π c

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH = CategoryTheory.Limits.Cofork.π c

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg) (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc)

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

Equations

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

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

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

Equations

• CategoryTheory.ShortComplex.rightHomology S = (CategoryTheory.ShortComplex.rightHomologyData S).H

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

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

Equations

• CategoryTheory.ShortComplex.opcycles S = (CategoryTheory.ShortComplex.rightHomologyData S).Q

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

The canonical map S.rightHomology ⟶ S.opcycles.

Equations

• CategoryTheory.ShortComplex.rightHomologyι S = (CategoryTheory.ShortComplex.rightHomologyData S).ι

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

The projection S.X₂ ⟶ S.opcycles.

Equations

• CategoryTheory.ShortComplex.pOpcycles S = (CategoryTheory.ShortComplex.rightHomologyData S).p

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

The canonical map S.opcycles ⟶ X₃.

Equations

• CategoryTheory.ShortComplex.fromOpcycles S = CategoryTheory.ShortComplex.RightHomologyData.g' (CategoryTheory.ShortComplex.rightHomologyData S)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.opcyclesIsoX₂ S hf = let_fun this := ⋯; (CategoryTheory.asIso (CategoryTheory.ShortComplex.pOpcycles S)).symm

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_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.HasRightHomology S] (hf : S.f = 0) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesIsoX₂ S hf).hom h) = h

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_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.HasRightHomology S] (hf : S.f = 0) {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesIsoX₂ S hf).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S) h) = h

@[simp]

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

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.opcyclesIsoRightHomology S hg = let_fun this := ⋯; (CategoryTheory.asIso (CategoryTheory.ShortComplex.rightHomologyι S)).symm

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_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.HasRightHomology S] (hg : S.g = 0) {Z : C} (h : CategoryTheory.ShortComplex.rightHomology S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesIsoRightHomology S hg).hom h) = h

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_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.HasRightHomology S] (hg : S.g = 0) {Z : C} (h : CategoryTheory.ShortComplex.opcycles S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesIsoRightHomology S hg).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) h) = h

@[simp]

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

def CategoryTheory.ShortComplex.rightHomologyMapData {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂

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

Equations

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

def CategoryTheory.ShortComplex.rightHomologyMap' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : h₁.H ⟶ h₂.H

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

Equations

• CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ = (CategoryTheory.ShortComplex.rightHomologyMapData φ h₁ h₂).φH

def CategoryTheory.ShortComplex.opcyclesMap' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : h₁.Q ⟶ h₂.Q

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

Equations

• CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ = (CategoryTheory.ShortComplex.rightHomologyMapData φ h₁ h₂).φQ

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp h₁.p (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) h) = CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp h₂.p h)

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp h₁.p (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_g'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₁) (CategoryTheory.CategoryStruct.comp φ.τ₃ h)

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_g' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₁) φ.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) {Z : C} (h : h₂.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) (CategoryTheory.CategoryStruct.comp h₂.ι h) = CategoryTheory.CategoryStruct.comp h₁.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)

noncomputable def CategoryTheory.ShortComplex.rightHomologyMap {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.rightHomology S₁ ⟶ CategoryTheory.ShortComplex.rightHomology S₂

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

Equations

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

noncomputable def CategoryTheory.ShortComplex.opcyclesMap {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.opcycles S₁ ⟶ CategoryTheory.ShortComplex.opcycles S₂

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

Equations

• CategoryTheory.ShortComplex.opcyclesMap φ = CategoryTheory.ShortComplex.opcyclesMap' φ (CategoryTheory.ShortComplex.rightHomologyData S₁) (CategoryTheory.ShortComplex.rightHomologyData S₂)

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.opcycles S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h) = CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S₂) h)

@[simp]

theorem CategoryTheory.ShortComplex.p_opcyclesMap {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles S₁) (CategoryTheory.ShortComplex.opcyclesMap φ) = CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.ShortComplex.pOpcycles S₂)

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcycles_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.fromOpcycles S₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.fromOpcycles S₁) (CategoryTheory.CategoryStruct.comp φ.τ₃ h)

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcycles_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (CategoryTheory.ShortComplex.fromOpcycles S₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.fromOpcycles S₁) φ.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) {Z : C} (h : CategoryTheory.ShortComplex.opcycles S₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (φ : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) (CategoryTheory.ShortComplex.rightHomologyι S₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S₁) (CategoryTheory.ShortComplex.opcyclesMap φ)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ = γ.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ = γ.φQ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.ShortComplex.rightHomologyMap' 0 h₁ h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.ShortComplex.opcyclesMap' 0 h₁ h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.ShortComplex.rightHomologyMap 0 = 0

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.ShortComplex.opcyclesMap 0 = 0

theorem CategoryTheory.ShortComplex.rightHomologyMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃) {Z : C} (h : h₃.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₂ h₃) h)

theorem CategoryTheory.ShortComplex.rightHomologyMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃) : CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂) (CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₂ h₃)

theorem CategoryTheory.ShortComplex.opcyclesMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃) {Z : C} (h : h₃.Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₁ h₁ h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₂ h₂ h₃) h)

theorem CategoryTheory.ShortComplex.opcyclesMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (h₃ : CategoryTheory.ShortComplex.RightHomologyData S₃) : CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₁ h₁ h₂) (CategoryTheory.ShortComplex.opcyclesMap' φ₂ h₂ h₃)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.ShortComplex.HasRightHomology S₃] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) : CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ₁) (CategoryTheory.ShortComplex.rightHomologyMap φ₂)

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.ShortComplex.HasRightHomology S₃] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) : CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ₁) (CategoryTheory.ShortComplex.opcyclesMap φ₂)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.rightHomologyMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.rightHomologyMap' e.inv h₂ h₁

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.rightHomologyMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.rightHomologyMap' e.hom h₁ h₂

def CategoryTheory.ShortComplex.rightHomologyMapIso' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : h₁.H ≅ h₂.H

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

Equations

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

instance CategoryTheory.ShortComplex.isIso_rightHomologyMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.opcyclesMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.opcyclesMap' e.hom h₁ h₂

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.opcyclesMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.opcyclesMap' e.inv h₂ h₁

def CategoryTheory.ShortComplex.opcyclesMapIso' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : h₁.Q ≅ h₂.Q

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

Equations

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

instance CategoryTheory.ShortComplex.isIso_opcyclesMap'_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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : (CategoryTheory.ShortComplex.rightHomologyMapIso e).inv = CategoryTheory.ShortComplex.rightHomologyMap e.inv

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMapIso_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : (CategoryTheory.ShortComplex.rightHomologyMapIso e).hom = CategoryTheory.ShortComplex.rightHomologyMap e.hom

noncomputable def CategoryTheory.ShortComplex.rightHomologyMapIso {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.ShortComplex.rightHomology S₁ ≅ CategoryTheory.ShortComplex.rightHomology S₂

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

Equations

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

instance CategoryTheory.ShortComplex.isIso_rightHomologyMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap φ)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : (CategoryTheory.ShortComplex.opcyclesMapIso e).inv = CategoryTheory.ShortComplex.opcyclesMap e.inv

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMapIso_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : (CategoryTheory.ShortComplex.opcyclesMapIso e).hom = CategoryTheory.ShortComplex.opcyclesMap e.hom

noncomputable def CategoryTheory.ShortComplex.opcyclesMapIso {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.ShortComplex.opcycles S₁ ≅ CategoryTheory.ShortComplex.opcycles S₂

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

Equations

• CategoryTheory.ShortComplex.opcyclesMapIso e = { hom := CategoryTheory.ShortComplex.opcyclesMap e.hom, inv := CategoryTheory.ShortComplex.opcyclesMap e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

instance CategoryTheory.ShortComplex.isIso_opcyclesMap_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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)

Equations

• ⋯ = ⋯

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

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

Equations

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

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

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

Equations

• CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h = CategoryTheory.ShortComplex.opcyclesMapIso' (CategoryTheory.Iso.refl S) (CategoryTheory.ShortComplex.rightHomologyData S) h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.ShortComplex.rightHomologyMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h₁).hom (CategoryTheory.CategoryStruct.comp γ.φH (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h₂).inv)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.ShortComplex.opcyclesMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h₁).hom (CategoryTheory.CategoryStruct.comp γ.φQ (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h₂).inv)

theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso h₁).hom γ.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso h₁).hom γ.φQ

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyFunctor_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.rightHomologyFunctor C).map φ = CategoryTheory.ShortComplex.rightHomologyMap φ

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyFunctor_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.rightHomologyFunctor C).obj S = CategoryTheory.ShortComplex.rightHomology S

noncomputable def CategoryTheory.ShortComplex.rightHomologyFunctor (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 right homology functor ShortComplex C ⥤ C, where the right homology of a short complex S is understood as a kernel of the obvious map S.fromOpcycles : S.opcycles ⟶ S.X₃ where S.opcycles is a cokernel of S.f : S.X₁ ⟶ S.X₂.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesFunctor_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.opcyclesFunctor C).map φ = CategoryTheory.ShortComplex.opcyclesMap φ

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesFunctor_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.opcyclesFunctor C).obj S = CategoryTheory.ShortComplex.opcycles S

noncomputable def CategoryTheory.ShortComplex.opcyclesFunctor (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 opcycles functor ShortComplex C ⥤ C which sends a short complex S to S.opcycles which is a cokernel of S.f : S.X₁ ⟶ S.X₂.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyι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.rightHomologyιNatTrans C).app S = CategoryTheory.ShortComplex.rightHomologyι S

noncomputable def CategoryTheory.ShortComplex.rightHomologyι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.rightHomologyFunctor C ⟶ CategoryTheory.ShortComplex.opcyclesFunctor C

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.pOpcyclesNatTrans_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.pOpcyclesNatTrans C).app S = CategoryTheory.ShortComplex.pOpcycles S

noncomputable def CategoryTheory.ShortComplex.pOpcyclesNatTrans (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.opcyclesFunctor C

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.fromOpcyclesNatTrans_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.fromOpcyclesNatTrans C).app S = CategoryTheory.ShortComplex.fromOpcycles S

noncomputable def CategoryTheory.ShortComplex.fromOpcyclesNatTrans (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.opcyclesFunctor C ⟶ CategoryTheory.ShortComplex.π₃

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.op_φ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.op ψ).φH = ψ.φH.op

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ {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.op ψ).φQ = ψ.φK.op

def CategoryTheory.ShortComplex.LeftHomologyMapData.op {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.RightHomologyMapData (CategoryTheory.ShortComplex.opMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.op h₂) (CategoryTheory.ShortComplex.LeftHomologyData.op h₁)

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

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.op ψ = { φQ := ψ.φK.op, φH := ψ.φH.op, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ {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.unop ψ).φQ = ψ.φK.unop

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φ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.unop ψ).φH = ψ.φH.unop

def CategoryTheory.ShortComplex.LeftHomologyMapData.unop {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.RightHomologyMapData (CategoryTheory.ShortComplex.unopMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.unop h₂) (CategoryTheory.ShortComplex.LeftHomologyData.unop h₁)

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

Equations

• CategoryTheory.ShortComplex.LeftHomologyMapData.unop ψ = { φQ := ψ.φK.unop, φH := ψ.φH.unop, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.op_φ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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.RightHomologyMapData.op ψ).φK = ψ.φQ.op

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.op_φ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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.RightHomologyMapData.op ψ).φH = ψ.φH.op

def CategoryTheory.ShortComplex.RightHomologyMapData.op {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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.ShortComplex.opMap φ) (CategoryTheory.ShortComplex.RightHomologyData.op h₂) (CategoryTheory.ShortComplex.RightHomologyData.op h₁)

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.op ψ = { φK := ψ.φQ.op, φH := ψ.φH.op, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.unop_φ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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.RightHomologyMapData.unop ψ).φK = ψ.φQ.unop

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.unop_φ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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : (CategoryTheory.ShortComplex.RightHomologyMapData.unop ψ).φH = ψ.φH.unop

def CategoryTheory.ShortComplex.RightHomologyMapData.unop {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.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) : CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.ShortComplex.unopMap φ) (CategoryTheory.ShortComplex.RightHomologyData.unop h₂) (CategoryTheory.ShortComplex.RightHomologyData.unop h₁)

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

Equations

• CategoryTheory.ShortComplex.RightHomologyMapData.unop ψ = { φK := ψ.φQ.unop, φH := ψ.φH.unop, commi := ⋯, commf' := ⋯, commπ := ⋯ }

noncomputable def CategoryTheory.ShortComplex.rightHomologyOpIso {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.rightHomology (CategoryTheory.ShortComplex.op S) ≅ Opposite.op (CategoryTheory.ShortComplex.leftHomology S)

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

Equations

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

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

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

Equations

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

noncomputable def CategoryTheory.ShortComplex.opcyclesOpIso {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.opcycles (CategoryTheory.ShortComplex.op S) ≅ Opposite.op (CategoryTheory.ShortComplex.cycles S)

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

Equations

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_op {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.leftHomologyMap' φ h₁ h₂).op = CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.ShortComplex.opMap φ) (CategoryTheory.ShortComplex.LeftHomologyData.op h₂) (CategoryTheory.ShortComplex.LeftHomologyData.op h₁)

theorem CategoryTheory.ShortComplex.leftHomologyMap_op {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.ShortComplex.leftHomologyMap φ).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyOpIso S₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.ShortComplex.opMap φ)) (CategoryTheory.ShortComplex.rightHomologyOpIso S₁).hom)

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_op {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂).op = CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.ShortComplex.opMap φ) (CategoryTheory.ShortComplex.RightHomologyData.op h₂) (CategoryTheory.ShortComplex.RightHomologyData.op h₁)

theorem CategoryTheory.ShortComplex.rightHomologyMap_op {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : (CategoryTheory.ShortComplex.rightHomologyMap φ).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyOpIso S₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.ShortComplex.opMap φ)) (CategoryTheory.ShortComplex.leftHomologyOpIso S₁).hom)

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.RightHomologyData S₂

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_Q {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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).Q = h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).H = h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_p {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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).p = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv φ.τ₂) h.p

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).ι = h.ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_g' {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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.RightHomologyData.g' (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h) φ.τ₃

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.RightHomologyData S₁

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_Q {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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q = h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H = h.H

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_p {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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).p = CategoryTheory.CategoryStruct.comp φ.τ₂ h.p

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).ι = h.ι

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_g'_τ₃ {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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h)) φ.τ₃ = CategoryTheory.ShortComplex.RightHomologyData.g' h

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData S₁) : CategoryTheory.ShortComplex.RightHomologyData S₂

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

Equations

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

theorem CategoryTheory.ShortComplex.hasRightHomology_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.HasRightHomology S₁] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HasRightHomology S₂

theorem CategoryTheory.ShortComplex.hasRightHomology_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.HasRightHomology S₂] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.HasRightHomology S₁

theorem CategoryTheory.ShortComplex.hasRightHomology_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.HasRightHomology S₁] : CategoryTheory.ShortComplex.HasRightHomology S₂

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φQ {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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono φ h).φQ = CategoryTheory.CategoryStruct.id h.Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono φ h).φH = CategoryTheory.CategoryStruct.id h.H

def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₁) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.RightHomologyMapData φ h (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h)

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φQ {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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φQ = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φH = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H

noncomputable def CategoryTheory.ShortComplex.RightHomologyMapData.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.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.ShortComplex.RightHomologyMapData φ (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h) h

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

Equations

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

instance CategoryTheory.ShortComplex.instIsIsoHRightHomologyMap' {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.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.instIsIsoRightHomologyRightHomologyMap {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.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap φ)

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

• CategoryTheory.ShortComplex.descOpcycles S k hk = CategoryTheory.ShortComplex.RightHomologyData.descQ (CategoryTheory.ShortComplex.rightHomologyData S) k hk

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• CategoryTheory.ShortComplex.opcyclesIsCokernel S = (CategoryTheory.ShortComplex.rightHomologyData S).hp

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

• CategoryTheory.ShortComplex.descRightHomology S k hk = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) (CategoryTheory.ShortComplex.descOpcycles S k hk)

theorem CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_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 : S.X₂ ⟶ A) [CategoryTheory.ShortComplex.HasRightHomology S] (x : S.X₃ ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp S.g x) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.descOpcycles S k ⋯) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_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 : S.X₂ ⟶ A) [CategoryTheory.ShortComplex.HasRightHomology S] (x : S.X₃ ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp S.g x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyι S) (CategoryTheory.ShortComplex.descOpcycles S k ⋯) = 0

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.rightHomologyIsKernel S = (CategoryTheory.ShortComplex.rightHomologyData S).hι

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_comp_descOpcycles_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 : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [CategoryTheory.ShortComplex.HasRightHomology S] (φ : S₁ ⟶ S) [CategoryTheory.ShortComplex.HasRightHomology S₁] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.descOpcycles S k hk) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.descOpcycles S₁ (CategoryTheory.CategoryStruct.comp φ.τ₂ k) ⋯) h

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_comp_descOpcycles {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 : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [CategoryTheory.ShortComplex.HasRightHomology S] (φ : S₁ ⟶ S) [CategoryTheory.ShortComplex.HasRightHomology S₁] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (CategoryTheory.ShortComplex.descOpcycles S k hk) = CategoryTheory.ShortComplex.descOpcycles S₁ (CategoryTheory.CategoryStruct.comp φ.τ₂ k) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

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

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

theorem CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi {C : Type u_1} [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.Epi φ.τ₁) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)

theorem CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi' {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.Epi φ.τ₁) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)

instance CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi {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.Epi φ.τ₁] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)

Equations

• ⋯ = ⋯