Naturality of the extension homology isomorphism

Extending a complex along a ComplexShape.Embedding does not change its homology, and Mathlib records the isomorphism HomologicalComplex.extendHomologyIso together with its compatibility with homologyπ, homologyι, cycles, and opcycles — but not its naturality in the complex.

Naturality is what a comparison argument needs when the complex varies. Here the ℕ-indexed Čech complex is extended to ℤ, and the comparison has to commute with the map induced by a morphism of sheaves; that requires the extension isomorphism to commute with induced maps.

Both lemmas follow from the cycles-level identity by cancelling the epimorphism homologyπ.

theorem HomologicalComplex.extendCyclesIso_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} {ι' : Type u_3} {c : ComplexShape ι} {c' : ComplexShape ι'} {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') {j : ι} {j' : ι'} (hj' : e.f j = j') [K.HasHomology j] [L.HasHomology j] [(K.extend e).HasHomology j'] [(L.extend e).HasHomology j'] : CategoryTheory.CategoryStruct.comp (cyclesMap (extendMap φ e) j') (L.extendCyclesIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (cyclesMap φ j)

The cycles isomorphism for an extended complex commutes with induced maps.

The cycles of an extension are the cycles of the original in the corresponding degree, and both sides agree after cancelling the mono iCycles.

theorem HomologicalComplex.extendCyclesIso_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} {ι' : Type u_3} {c : ComplexShape ι} {c' : ComplexShape ι'} {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') {j : ι} {j' : ι'} (hj' : e.f j = j') [K.HasHomology j] [L.HasHomology j] [(K.extend e).HasHomology j'] [(L.extend e).HasHomology j'] {Z : C} (h : L.cycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap (extendMap φ e) j') (CategoryTheory.CategoryStruct.comp (L.extendCyclesIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (CategoryTheory.CategoryStruct.comp (cyclesMap φ j) h)

The cycles isomorphism for an extended complex commutes with induced maps.

The cycles of an extension are the cycles of the original in the corresponding degree, and both sides agree after cancelling the mono iCycles.

theorem HomologicalComplex.extendHomologyIso_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} {ι' : Type u_3} {c : ComplexShape ι} {c' : ComplexShape ι'} {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') {j : ι} {j' : ι'} (hj' : e.f j = j') [K.HasHomology j] [L.HasHomology j] [(K.extend e).HasHomology j'] [(L.extend e).HasHomology j'] : CategoryTheory.CategoryStruct.comp (homologyMap (extendMap φ e) j') (L.extendHomologyIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom (homologyMap φ j)

The homology isomorphism for an extended complex commutes with induced maps.

This is the statement the Čech comparison needs, since the Čech complex is ℕ-indexed and the comparison chain is ℤ-indexed. It follows from the cycles version by cancelling homologyπ.

theorem HomologicalComplex.extendHomologyIso_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} {ι' : Type u_3} {c : ComplexShape ι} {c' : ComplexShape ι'} {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') {j : ι} {j' : ι'} (hj' : e.f j = j') [K.HasHomology j] [L.HasHomology j] [(K.extend e).HasHomology j'] [(L.extend e).HasHomology j'] {Z : C} (h : L.homology j ⟶ Z) : CategoryTheory.CategoryStruct.comp (homologyMap (extendMap φ e) j') (CategoryTheory.CategoryStruct.comp (L.extendHomologyIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom (CategoryTheory.CategoryStruct.comp (homologyMap φ j) h)

The homology isomorphism for an extended complex commutes with induced maps.

This is the statement the Čech comparison needs, since the Čech complex is ℕ-indexed and the comparison chain is ℤ-indexed. It follows from the cycles version by cancelling homologyπ.