Euler characteristics of shifted cochain complexes

The term of the shifted cochain complex K⟦a⟧ in degree i is the term of K in degree i + a, so shifting by a moves every term across a degrees and multiplies the Euler characteristic of the terms by (-1) ^ a. This is the bookkeeping needed when a complex is built in one grading and normalized by a shift, as for the normalized Khovanov complex.

The identity holds for Mathlib's finsum-based definition without any finiteness hypothesis: reindexing preserves the support of the summand, and multiplication by the unit (-1) ^ a of ℤ does not change it either.

Main results

• CochainComplex.eulerChar_shift: χ(K⟦a⟧) = (-1) ^ a χ(K).

@[simp]

theorem CochainComplex.eulerChar_shift {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℤ) (a : ℤ) : HomologicalComplex.eulerChar (K⟦a⟧) = ↑a.negOnePow * HomologicalComplex.eulerChar K

Shifting a cochain complex of modules by a multiplies the Euler characteristic of its terms by (-1) ^ a.