Opcycles and extension by zero #
The opcycles isomorphism of an extended complex is natural in chain maps and compatible with
HomologicalComplex.opcyclesToCycles. These identities require homology only in the degrees
involved, in a category with zero morphisms and a zero object.
Adapted from TauCetiProject/TauCeti#10141.
@[simp]
theorem
HomologicalComplex.extendOpcyclesIso_hom_naturality
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (opcyclesMap (extendMap φ e) j') (L.extendOpcyclesIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').hom (opcyclesMap φ j)
The identification of the opcycles of an extended complex is natural.
@[simp]
theorem
HomologicalComplex.extendOpcyclesIso_hom_naturality_assoc
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
{Z : C}
(h : L.opcycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (opcyclesMap (extendMap φ e) j')
(CategoryTheory.CategoryStruct.comp (L.extendOpcyclesIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').hom
(CategoryTheory.CategoryStruct.comp (opcyclesMap φ j) h)
The identification of the opcycles of an extended complex is natural.
theorem
HomologicalComplex.extend_opcyclesToCycles_comp_extendCyclesIso_hom
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j : ι}
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.CategoryStruct.comp ((K.extend e).opcyclesToCycles i' j') (K.extendCyclesIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hi').hom (K.opcyclesToCycles i j)
The identifications of the opcycles and cycles of an extended complex are compatible with the
maps opcyclesToCycles.
theorem
HomologicalComplex.extend_opcyclesToCycles_comp_extendCyclesIso_hom_assoc
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j : ι}
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
[K.HasHomology i]
[K.HasHomology j]
{Z : C}
(h : K.cycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.extend e).opcyclesToCycles i' j')
(CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hi').hom
(CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h)
The identifications of the opcycles and cycles of an extended complex are compatible with the
maps opcyclesToCycles.