The two-periodic complex of a square-zero duplex

The square-zero duplex has the same differential in both parities. Its associated two-periodic complex has zero homology in both parities whenever homology exists.

theorem TauCeti.CurvedDuplex.isZero_squareZero_periodicHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) (i : ZMod 2) [((toPeriodicComplex C R).obj (squareZero A)).HasHomology i] : CategoryTheory.Limits.IsZero (((toPeriodicComplex C R).obj (squareZero A)).homology i)

The two-periodic complex associated to the square-zero duplex has zero homology in each parity.