Computations for additive total-complex shapes

The total-complex shape induced by tensor signs adds the two input indices. This characteristic equation is independent of the category or bifunctor used to form a total complex.

The instance HomologicalComplex₂.totalComplexShapeSymmetryDownNat identifies the total complexes of a first-quadrant bicomplex and of its flip by the Koszul sign (-1)^(p*q) in bidegree (p, q). It is the natural-number analogue of Mathlib's TotalComplexShapeSymmetry instance for cochain complexes indexed by ℤ, and adapts its sign calculation.

@[simp]

theorem ComplexShape.π_eq_add {I : Type u_1} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] (p q : I) : c.π c c (p, q) = p + q

The additive total-complex shape sends a pair of indices to their sum.

@[instance_reducible]

instance HomologicalComplex₂.totalComplexShapeSymmetryDownNat : TotalComplexShapeSymmetry (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)

The total complexes of a first-quadrant bicomplex and its flip are identified by the Koszul sign (-1)^(p*q) on the term in bidegree (p, q).