Vanishing outside the bounds of a bounded cochain complex

Mathlib records the boundedness of a cochain complex indexed by ℤ in the classes CochainComplex.IsStrictlyGE and CochainComplex.IsStrictlyLE, and converts them into vanishing statements one strict inequality at a time. An argument that runs over the degrees of a bounded complex instead wants the two bounds packaged as a single finite interval Finset.Icc a b, so that membership in the summation range is the only case distinction left.

This file records the resulting two statements: outside Finset.Icc a b, the terms of a strictly bounded complex vanish, while its cohomology vanishes under the corresponding cohomological bounds. They are the finiteness input to alternating-sum (Euler characteristic) computations over a bounded complex.

Main results

• HomologicalComplex.isZero_X_of_notMem_Icc: the terms vanish outside the bounding interval.
• HomologicalComplex.isZero_homology_of_notMem_Icc: the cohomology vanishes outside the bounding interval.

theorem HomologicalComplex.isZero_X_of_notMem_Icc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasZeroMorphisms A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {n : ℤ} (hn : n ∉ Finset.Icc a b) : CategoryTheory.Limits.IsZero (K.X n)

A strictly bounded cochain complex is zero outside any interval supplied by its bounds.

theorem HomologicalComplex.isZero_homology_of_notMem_Icc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasZeroMorphisms A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE b] {n : ℤ} [HasHomology K n] (hn : n ∉ Finset.Icc a b) : CategoryTheory.Limits.IsZero (homology K n)

The homology of a cochain complex is zero outside any interval supplied by its cohomological bounds.