The homology sequence of an extended short exact sequence

Let e : c.Embedding c' be an embedding of complex shapes and S a short exact sequence of complexes of shape c in an abelian category. Extending S by zero along e gives a short exact sequence of complexes of shape c' (CategoryTheory.ShortComplex.ShortExact.extend), and Mathlib identifies the homology of an extended complex in degree e.f j with the homology of the original complex in degree j (HomologicalComplex.extendHomologyIso). This file shows that the connecting maps of the two homology sequences correspond under these identifications (CategoryTheory.ShortComplex.ShortExact.extend_δ_comp_extendHomologyIso_hom).

This is what allows a connecting map computed on a complex reindexed along an embedding, such as the Tate complex, whose negative part is the complex of inhomogeneous chains reindexed by n ↦ -(n + 1), to be compared with the connecting map of the original complex.

This file is adapted from TauCetiProject/TauCeti#10141.

theorem CategoryTheory.ShortComplex.ShortExact.extend {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [Category.{v_1, u_3} C] [Abelian C] {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (e : c.Embedding c') : (S.map (e.extendFunctor C)).ShortExact

Extending a short exact sequence of complexes by zero along an embedding of complex shapes gives a short exact sequence.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.extend_δ_comp_extendHomologyIso_hom {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [Category.{v_1, u_3} C] [Abelian C] {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (e : c.Embedding c') {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hij' : c'.Rel i' j') : CategoryStruct.comp (⋯.δ i' j' hij') (S.X₁.extendHomologyIso e hj').hom = CategoryStruct.comp (S.X₃.extendHomologyIso e hi').hom (hS.δ i j hij)

The connecting maps of an extended short exact sequence. Under the identifications HomologicalComplex.extendHomologyIso of the homology of the extended complexes with the homology of the original ones, the connecting map of the extension of S along e in degrees e.f i ⟶ e.f j is the connecting map of S in degrees i ⟶ j.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.extend_δ_comp_extendHomologyIso_hom_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [Category.{v_1, u_3} C] [Abelian C] {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (e : c.Embedding c') {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hij' : c'.Rel i' j') {Z : C} (h : S.X₁.homology j ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp (⋯.δ i' j' hij') (S.X₁.extendHomologyIso e hj').hom) h = CategoryStruct.comp (CategoryStruct.comp (S.X₃.extendHomologyIso e hi').hom (hS.δ i j hij)) h

The connecting maps of an extended short exact sequence. Under the identifications HomologicalComplex.extendHomologyIso of the homology of the extended complexes with the homology of the original ones, the connecting map of the extension of S along e in degrees e.f i ⟶ e.f j is the connecting map of S in degrees i ⟶ j.