Finite horizontal-strip comparison for total complexes

A columnwise quasi-isomorphism of bicomplexes supported on a finite horizontal interval induces a quasi-isomorphism of their actual signed total complexes. Total objects are constructed from finite diagonal support; no infinite coproduct assumption is needed.

Main result

HomologicalComplex₂.totalMap_quasiIso_of_finiteStrip identifies the actual total map as a quasi-isomorphism from quasi-isomorphisms on the finitely many supported columns. The vertical direction may be unbounded, and the horizontal interval may be empty.

Implementation notes

The adjacent-tail induction applies derived-category triangles of short exact sequences to literal total maps. The single-column quotient is the shifted original column; the outer tails vanish by the support conditions.

References

The adjacent-column short exact sequence is in FilteredTotalComplexAdjacentCore.

theorem HomologicalComplex₂.totalMap_quasiIso_of_finiteStrip {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (a b : ℤ) (hK : ∀ (p q : ℤ), p < a ∨ b < p → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hL : ∀ (p q : ℤ), p < a ∨ b < p → CategoryTheory.Limits.IsZero ((L.X p).X q)) (hcol : ∀ (p : ℤ), a ≤ p → p ≤ b → QuasiIso (f.f p)) : QuasiIso (total.map f (ComplexShape.up ℤ))

The literal total map of a finite horizontal-strip bicomplex morphism is a quasi-isomorphism when each retained vertical column map is one. The vertical columns may be unbounded, and the horizontal strip may be empty; finite diagonal support constructs the total complexes in an arbitrary abelian category.