Two-periodic complexes #
A two-periodic complex is a homological complex for ComplexShape.up (ZMod 2). Its morphisms
are determined by their components in degrees 0 and 1.
theorem
TauCeti.HomologicalComplex.hom_ext_two
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K L : HomologicalComplex C (ComplexShape.up (ZMod 2))}
{f g : K ⟶ L}
(h₀ : f.f 0 = g.f 0)
(h₁ : f.f 1 = g.f 1)
:
Morphisms of two-periodic complexes are determined by their components in degrees 0
and 1.