The homology sequence

If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is a short exact sequence in a category of complexes HomologicalComplex C c in an abelian category (i.e. S is a short complex in that category and satisfies hS : S.ShortExact), then whenever i and j are degrees such that hij : c.Rel i j, then there is a long exact sequence : ... ⟶ S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j ⟶ .... The connecting homomorphism S.X₃.homology i ⟶ S.X₁.homology j is hS.δ i j hij, and the exactness is asserted as lemmas hS.homology_exact₁, hS.homology_exact₂ and hS.homology_exact₃.

The proof is based on the snake lemma, similarly as it was originally done in the Liquid Tensor Experiment.

References

• https://stacks.math.columbia.edu/tag/0111

noncomputable def HomologicalComplex.opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : K.opcycles i ⟶ K.cycles j

The morphism K.opcycles i ⟶ K.cycles j that is induced by K.d i j.

Equations

• K.opcyclesToCycles i j = K.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯

@[simp]

theorem HomologicalComplex.opcyclesToCycles_iCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j) = K.fromOpcycles i j

@[simp]

theorem HomologicalComplex.opcyclesToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h

theorem HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j)) = K.d i j

theorem HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h)) = CategoryTheory.CategoryStruct.comp (K.d i j) h

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.opcyclesToCycles i j) = K.toCycles i j

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesToCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.cycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h) = CategoryTheory.CategoryStruct.comp (K.toCycles i j) h

@[simp]

theorem HomologicalComplex.homologyι_opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.opcyclesToCycles i j) = 0

@[simp]

theorem HomologicalComplex.homologyι_opcyclesToCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.cycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.opcyclesToCycles_homologyπ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.homologyπ j) = 0

@[simp]

theorem HomologicalComplex.opcyclesToCycles_homologyπ_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.homology j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.opcyclesToCycles_naturality {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i j : ι) [K.HasHomology i] [K.HasHomology j] [L.HasHomology i] [L.HasHomology j] : CategoryTheory.CategoryStruct.comp (opcyclesMap φ i) (L.opcyclesToCycles i j) = CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (cyclesMap φ j)

@[simp]

theorem HomologicalComplex.opcyclesToCycles_naturality_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i j : ι) [K.HasHomology i] [K.HasHomology j] [L.HasHomology i] [L.HasHomology j] {Z : C} (h : L.cycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (opcyclesMap φ i) (CategoryTheory.CategoryStruct.comp (L.opcyclesToCycles i j) h) = CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (cyclesMap φ j) h)

noncomputable def HomologicalComplex.natTransOpCyclesToCycles (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (i j : ι) [CategoryTheory.CategoryWithHomology C] : opcyclesFunctor C c i ⟶ cyclesFunctor C c j

The natural transformation K.opcyclesToCycles i j : K.opcycles i ⟶ K.cycles j for all K : HomologicalComplex C c.

Equations

• HomologicalComplex.natTransOpCyclesToCycles C c i j = { app := fun (K : HomologicalComplex C c) => K.opcyclesToCycles i j, naturality := ⋯ }

@[simp]

theorem HomologicalComplex.natTransOpCyclesToCycles_app (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (i j : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (natTransOpCyclesToCycles C c i j).app K = K.opcyclesToCycles i j

noncomputable def HomologicalComplex.HomologySequence.composableArrows₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.ComposableArrows C 3

The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.

Equations

• HomologicalComplex.HomologySequence.composableArrows₃ K i j = CategoryTheory.ComposableArrows.mk₃ (K.homologyι i) (K.opcyclesToCycles i j) (K.homologyπ j)

instance HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.Mono ((composableArrows₃ K i j).map' 0 1 ⋯ ⋯)

instance HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.Epi ((composableArrows₃ K i j).map' 2 3 ⋯ ⋯)

theorem HomologicalComplex.HomologySequence.composableArrows₃_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hij : c.Rel i j) [CategoryTheory.CategoryWithHomology C] : (composableArrows₃ K i j).Exact

The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j is exact when c.Rel i j.

noncomputable def HomologicalComplex.HomologySequence.composableArrows₃Functor (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i j : ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ComposableArrows C 3)

The functor HomologicalComplex C c ⥤ ComposableArrows C 3 that maps K to the diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.

Equations

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

@[simp]

theorem HomologicalComplex.HomologySequence.composableArrows₃Functor_obj (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i j : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (composableArrows₃Functor C i j).obj K = composableArrows₃ K i j

@[simp]

theorem HomologicalComplex.HomologySequence.composableArrows₃Functor_map (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i j : ι) [CategoryTheory.CategoryWithHomology C] {K L : HomologicalComplex C c} (φ : K ⟶ L) : (composableArrows₃Functor C i j).map φ = CategoryTheory.ComposableArrows.homMk₃ (homologyMap φ i) (opcyclesMap φ i) (cyclesMap φ j) (homologyMap φ j) ⋯ ⋯ ⋯

theorem HomologicalComplex.opcycles_right_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [CategoryTheory.Epi S.g] (i : ι) [S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] : (CategoryTheory.ShortComplex.mk (opcyclesMap S.f i) (opcyclesMap S.g i) ⋯).Exact

If X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is an exact sequence of homological complexes, then X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0 is exact. This lemma states the exactness at X₂.opcycles i, while the fact that X₂.opcycles i ⟶ X₃.opcycles i is an epi is an instance.

theorem HomologicalComplex.cycles_left_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [CategoryTheory.Mono S.f] (i : ι) [S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] : (CategoryTheory.ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).Exact

If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ is an exact sequence of homological complex, then 0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i is exact. This lemma states the exactness at X₂.cycles i, while the fact that X₁.cycles i ⟶ X₂.cycles i is a mono is an instance.

noncomputable def HomologicalComplex.HomologySequence.snakeInput {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : CategoryTheory.ShortComplex.SnakeInput C

Given a short exact short complex S : HomologicalComplex C c, and degrees i and j such that c.Rel i j, this is the snake diagram whose four lines are respectively obtained by applying the functors homologyFunctor C c i, opcyclesFunctor C c i, cyclesFunctor C c j, homologyFunctor C c j to S. Applying the snake lemma to this gives the homology sequence of S.

Equations

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

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_L₁ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).L₁ = (opcyclesFunctor C c i).mapShortComplex.obj S

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_v₁₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).v₁₂ = S.mapNatTrans (natTransOpCyclesToCycles C c i j)

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_L₀ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).L₀ = (homologyFunctor C c i).mapShortComplex.obj S

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_v₂₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).v₂₃ = S.mapNatTrans (natTransHomologyπ C c j)

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_L₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).L₃ = (homologyFunctor C c j).mapShortComplex.obj S

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_v₀₁ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).v₀₁ = S.mapNatTrans (natTransHomologyι C c i)

@[simp]

theorem HomologicalComplex.HomologySequence.snakeInput_L₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (snakeInput hS i j hij).L₂ = (cyclesFunctor C c j).mapShortComplex.obj S

noncomputable def CategoryTheory.ShortComplex.ShortExact.δ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : S.X₃.homology i ⟶ S.X₁.homology j

The connecting homoomorphism S.X₃.homology i ⟶ S.X₁.homology j for a short exact short complex S.

Equations

• hS.δ i j hij = (HomologicalComplex.HomologySequence.snakeInput hS i j hij).δ

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.δ_comp {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : CategoryStruct.comp (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) = 0

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) {Z : C} (h : S.X₂.homology j ⟶ Z) : CategoryStruct.comp (hS.δ i j hij) (CategoryStruct.comp (HomologicalComplex.homologyMap S.f j) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.comp_δ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) = 0

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) {Z : C} (h : S.X₁.homology j ⟶ Z) : CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (CategoryStruct.comp (hS.δ i j hij) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (ShortComplex.mk (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) ⋯).Exact

Exactness of S.X₃.homology i ⟶ S.X₁.homology j ⟶ S.X₂.homology j.

theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₂ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) : (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Exactness of S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i.

theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (ShortComplex.mk (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) ⋯).Exact

Exactness of S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j.

theorem CategoryTheory.ShortComplex.ShortExact.δ_eq' {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) {A : C} (x₃ : A ⟶ S.X₃.homology i) (x₂ : A ⟶ S.X₂.opcycles i) (x₁ : A ⟶ S.X₁.cycles j) (h₂ : CategoryStruct.comp x₂ (HomologicalComplex.opcyclesMap S.g i) = CategoryStruct.comp x₃ (S.X₃.homologyι i)) (h₁ : CategoryStruct.comp x₁ (HomologicalComplex.cyclesMap S.f j) = CategoryStruct.comp x₂ (S.X₂.opcyclesToCycles i j)) : CategoryStruct.comp x₃ (hS.δ i j hij) = CategoryStruct.comp x₁ (S.X₁.homologyπ j)

theorem CategoryTheory.ShortComplex.ShortExact.δ_eq {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Abelian C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) {A : C} (x₃ : A ⟶ S.X₃.X i) (hx₃ : CategoryStruct.comp x₃ (S.X₃.d i j) = 0) (x₂ : A ⟶ S.X₂.X i) (hx₂ : CategoryStruct.comp x₂ (S.g.f i) = x₃) (x₁ : A ⟶ S.X₁.X j) (hx₁ : CategoryStruct.comp x₁ (S.f.f j) = CategoryStruct.comp x₂ (S.X₂.d i j)) (k : ι) (hk : c.next j = k) : CategoryStruct.comp (S.X₃.liftCycles x₃ j ⋯ hx₃) (CategoryStruct.comp (S.X₃.homologyπ i) (hS.δ i j hij)) = CategoryStruct.comp (S.X₁.liftCycles x₁ k hk ⋯) (S.X₁.homologyπ j)