Colimits and diagonal coordinates of direct-sum total complexes

Mathlib's direct-sum total functor preserves colimits of any diagram shape when the component category has those colimits and each total-degree fiber admits coproducts. For a particular cocone, colimits of its bidegree diagrams suffice. No exactness or homology argument is involved.

For integer-indexed totals, a projection to one summand exposes the horizontal and signed vertical parts of the incoming differential. Exactness in one column then clears one coordinate of a generalized cycle after an epi refinement. Finite iteration and a finite-support coproduct identity turn this into degree-local exactness and acyclicity when each total diagonal has finite nonzero support and the supported column entries are exact. The results assume the literal total already exists.

Main definitions

• HomologicalComplex₂.isColimitTotalFunctorMapCocone constructs the universal property for the literal mapped cocone.
• HomologicalComplex₂.totalProjection specializes the canonical coproduct projection to one total-degree summand.

Main results

• HomologicalComplex₂.totalFunctor_preservesColimitsOfShape exposes colimit preservation to typeclass search.
• HomologicalComplex₂.isZero_total_X_of_diagonal detects zero terms of a literal total from its bidegree summands. The three isStrictlyLE_total_* results specialize it to upper support bounds for cochain bicomplexes.
• HomologicalComplex₂.total_d_comp_totalProjection computes the incoming differential at one direct-sum coordinate.
• HomologicalComplex₂.exists_totalCycleRefinement_zero_le clears one coordinate of a generalized total cycle by an epi refinement.
• HomologicalComplex₂.exactAt_total_of_diagonal_bounds_of_column_exactAt proves exactness from finite support and exactness on one total-degree diagonal.
• HomologicalComplex₂.acyclic_total_of_diagonal_bounds_of_column_exactAt allows a separate finite support interval in every degree; HomologicalComplex₂.acyclic_total_of_upper_bounds_of_column_exactAt derives the uniform-rectangle case.
• HomologicalComplex₂.columnCone is the vertical pointwise cone of a bicomplex map; HomologicalComplex₂.hasTotal_columnCone constructs its literal total from source/target totals and the required biproducts.
• HomologicalComplex₂.totalColumnConeIso compares that literal total with the mapping cone of the literal total map, using a horizontal-degree sign on the source branch.
• HomologicalComplex₂.quasiIso_totalMap_of_four_diagonal_bounds_of_column_quasiIso upgrades a columnwise quasi-isomorphism to a quasi-isomorphism of literal totals when source and target each have lower and upper finite-support bounds in every total degree.

Implementation notes

Evaluate in each total degree, view its diagonal coproduct as a colimit over a discrete category, and commute the two colimits. Degreewise evaluation then reflects the resulting universal property.

For the integer-indexed coordinate result, compose each summand inclusion with the total differential and the canonical coproduct projection. The horizontal term reaches the next column, while the signed vertical term stays in the current column. Epi refinement supplies a preimage of the vertical cycle, and its boundary leaves all earlier columns zero. Finite iteration composes the epi refinements; the generic finite-support zero-map criterion CategoryTheory.Limits.Sigma.hom_eq_zero_of_finite_support makes the zero-coordinate residual a zero map.

References

The construction extends Mathlib's HomologicalComplex₂.totalFunctor and uses HomologicalComplex.isColimitOfEval and CategoryTheory.Limits.evaluationJointlyReflectsColimits. The coordinate results use CategoryTheory.Limits.Sigma.π and CategoryTheory.ShortComplex.Exact.exact_up_to_refinements.

Tags

bicomplex, total complex, coproduct, colimit, exactness, epi refinement

noncomputable def HomologicalComplex₂.isColimitTotalFunctorMapCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type w} [CategoryTheory.Category.{u_4, w} J] {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [∀ (n : I₁₂), CategoryTheory.Limits.HasCoproductsOfShape (↑(c₁.π c₂ c₁₂ ⁻¹' {n})) C] (F : CategoryTheory.Functor J (HomologicalComplex₂ C c₁ c₂)) [∀ (p : I₁) (q : I₂), CategoryTheory.Limits.HasColimit ((F.comp (HomologicalComplex.eval (HomologicalComplex C c₂) c₁ p)).comp (HomologicalComplex.eval C c₂ q))] (s : CategoryTheory.Limits.Cocone F) (h : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Limits.IsColimit ((totalFunctor C c₁ c₂ c₁₂).mapCocone s)

Evaluate the cocone in each bidegree, commute its diagram colimit with the coproduct over each total-degree fiber, and reflect colimits through degreewise evaluation. Only the bidegree diagrams occurring in F need colimits; ambient colimits of shape J are unnecessary.

Equations

• One or more equations did not get rendered due to their size.

instance HomologicalComplex₂.totalFunctor_preservesColimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type w} [CategoryTheory.Category.{u_4, w} J] {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [∀ (n : I₁₂), CategoryTheory.Limits.HasCoproductsOfShape (↑(c₁.π c₂ c₁₂ ⁻¹' {n})) C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.PreservesColimitsOfShape J (totalFunctor C c₁ c₂ c₁₂)

Register HomologicalComplex₂.isColimitTotalFunctorMapCocone for typeclass search, so downstream consumers can transport their cocones with CategoryTheory.Limits.isColimitOfPreserves.

theorem HomologicalComplex₂.isZero_total_X_of_diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (n : I₁₂) (h : ∀ (p : I₁) (q : I₂), c₁.π c₂ c₁₂ (p, q) = n → CategoryTheory.Limits.IsZero ((K.X p).X q)) : CategoryTheory.Limits.IsZero ((K.total c₁₂).X n)

A term of a literal total is zero when every bidegree summand on its diagonal is zero. No exactness or boundedness is required.

theorem HomologicalComplex₂.isStrictlyLE_total_of_diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (c : ℤ) (h : ∀ (p q : ℤ), c < p + q → CategoryTheory.Limits.IsZero ((K.X p).X q)) : CochainComplex.IsStrictlyLE (K.total (ComplexShape.up ℤ)) c

This diagonal criterion permits support regions without separate bounds on the two coordinates: only their sum controls the total.

theorem HomologicalComplex₂.isStrictlyLE_total_of_upper_bounds {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (a b : ℤ) (hOuter : ∀ (p q : ℤ), a < p → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hInner : ∀ (p q : ℤ), b < q → CategoryTheory.Limits.IsZero ((K.X p).X q)) : CochainComplex.IsStrictlyLE (K.total (ComplexShape.up ℤ)) (a + b)

Above the sum of the coordinate bounds, every summand lies beyond at least one bound, so the diagonal vanishing criterion applies.

theorem HomologicalComplex₂.isStrictlyLE_total_of_nonpositive_rows {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (c : ℤ) (hOuter : ∀ (p : ℤ), c < p → CategoryTheory.Limits.IsZero (K.X p)) (hInner : ∀ (p q : ℤ), 0 < q → CategoryTheory.Limits.IsZero ((K.X p).X q)) : CochainComplex.IsStrictlyLE (K.total (ComplexShape.up ℤ)) c

This form accepts zero outer rows directly: evaluation converts row vanishing to term vanishing, so nonpositive resolution rows retain the input's upper bound.

@[reducible, inline]

noncomputable abbrev HomologicalComplex₂.totalProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (p q n : ℤ) (h : p + q = n) : (K.total (ComplexShape.up ℤ)).X n ⟶ (K.X p).X q

The canonical projection from the literal direct-sum total complex to its (p,q) summand in total degree n.

Equations

• K.totalProjection p q n h = CategoryTheory.Limits.Sigma.π (K.toGradedObject.mapObjFun ((ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ)) n) ⟨(p, q), h⟩

theorem HomologicalComplex₂.total_d_comp_totalProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (p q n : ℤ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp ((K.total (ComplexShape.up ℤ)).d n (n + 1)) (K.totalProjection p (q + 1) (n + 1) ⋯) = CategoryTheory.CategoryStruct.comp (K.totalProjection (p - 1) (q + 1) n ⋯) ((K.d (p - 1) p).f (q + 1)) + (ComplexShape.up ℤ).ε p • CategoryTheory.CategoryStruct.comp (K.totalProjection p q n h) ((K.X p).d q (q + 1))

Compute an incoming coordinate by checking each coproduct inclusion against Mathlib's outgoing differential formulas. This uses the coproduct universal property and requires no finite diagonal support.

theorem HomologicalComplex₂.comp_totalProjection_comp_d_eq_zero_of_total_component_eq_zero_of_horizontal_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (p q n : ℤ) (h : p + q = n) {A : C} (x : A ⟶ (K.total (ComplexShape.up ℤ)).X n) (hx : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x ((K.total (ComplexShape.up ℤ)).d n (n + 1))) (K.totalProjection p (q + 1) (n + 1) ⋯) = 0) (hl : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x (K.totalProjection (p - 1) (q + 1) n ⋯)) ((K.d (p - 1) p).f (q + 1)) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x (K.totalProjection p q n h)) ((K.X p).d q (q + 1)) = 0

The incoming-coordinate formula isolates the vertical differential after the horizontal contribution vanishes; applying its sign again removes the sign. Only the selected total-differential coordinate must vanish, so callers need not supply a full total cycle.

theorem HomologicalComplex₂.exists_totalCycleRefinement_zero_le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (p q n : ℤ) (h : p + q = n) (hE : { X₁ := (K.X p).X (q - 1), X₂ := (K.X p).X q, X₃ := (K.X p).X (q + 1), f := (K.X p).d (q - 1) q, g := (K.X p).d q (q + 1), zero := ⋯ }.Exact) {A : C} (x : A ⟶ (K.total (ComplexShape.up ℤ)).X n) (hx : CategoryTheory.CategoryStruct.comp x ((K.total (ComplexShape.up ℤ)).d n (n + 1)) = 0) (hlow : ∀ (r s : ℤ) (hr : r + s = n), r < p → CategoryTheory.CategoryStruct.comp x (K.totalProjection r s n hr) = 0) : ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (y : A' ⟶ (K.X p).X (q - 1)), have z := CategoryTheory.CategoryStruct.comp ((ComplexShape.up ℤ).ε p • y) (K.ιTotal (ComplexShape.up ℤ) p (q - 1) (n - 1) ⋯); CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp π x - CategoryTheory.CategoryStruct.comp z ((K.total (ComplexShape.up ℤ)).d (n - 1) n)) ((K.total (ComplexShape.up ℤ)).d n (n + 1)) = 0 ∧ ∀ (r s : ℤ) (hr : r + s = n), r ≤ p → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp π x - CategoryTheory.CategoryStruct.comp z ((K.total (ComplexShape.up ℤ)).d (n - 1) n)) (K.totalProjection r s n hr) = 0

Apply exactness up to epi refinement to the selected vertical cycle, then subtract the boundary of its signed preimage. That boundary reaches only columns p and p + 1, preserving the cleared lower coordinates. Refinement avoids assuming that the generalized cycle lifts on its original source.

theorem HomologicalComplex₂.exactAt_total_of_diagonal_bounds_of_column_exactAt {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Abelian C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (n a b : ℤ) (hLower : ∀ (p q : ℤ), p + q = n → p < a → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hUpper : ∀ (p q : ℤ), p + q = n → b < p → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hExact : ∀ (p : ℤ), a ≤ p → p ≤ b → (K.X p).ExactAt (n - p)) : (K.total (ComplexShape.up ℤ)).ExactAt n

Refine a total cycle through the finitely supported diagonal, then use the finite projection identity to make its residual zero. The abelian exactness criterion then makes the literal total exact at n.

theorem HomologicalComplex₂.acyclic_total_of_diagonal_bounds_of_column_exactAt {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Abelian C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (hData : ∀ (n : ℤ), ∃ (a : ℤ) (b : ℤ), (∀ (p q : ℤ), p + q = n → p < a → CategoryTheory.Limits.IsZero ((K.X p).X q)) ∧ (∀ (p q : ℤ), p + q = n → b < p → CategoryTheory.Limits.IsZero ((K.X p).X q)) ∧ ∀ (p : ℤ), a ≤ p → p ≤ b → (K.X p).ExactAt (n - p)) : (K.total (ComplexShape.up ℤ)).Acyclic

Apply degree-local exactness to each diagonal, allowing the support interval and required column exactness to vary with total degree.

theorem HomologicalComplex₂.acyclic_total_of_upper_bounds_of_column_exactAt {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Abelian C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] (b c : ℤ) (hp : ∀ (p q : ℤ), b < p → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hq : ∀ (p q : ℤ), c < q → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hExact : ∀ (p q : ℤ), p ≤ b → q ≤ c → (K.X p).ExactAt q) : (K.total (ComplexShape.up ℤ)).Acyclic

A uniform upper rectangle gives finite support on every diagonal. Only columns and degrees inside that rectangle need the exactness premise.

noncomputable def HomologicalComplex₂.columnCone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) [∀ (p q : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.X p).X (q + 1)) ((L.X p).X q)] : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)

Take the pointwise cone vertically, leaving the horizontal bicomplex direction in place.

Equations

• HomologicalComplex₂.columnCone f = HomologicalComplex₂.flip (CochainComplex.mappingCone ((HomologicalComplex₂.flipFunctor C (ComplexShape.up ℤ) (ComplexShape.up ℤ)).map f))

theorem HomologicalComplex₂.hasTotal_columnCone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) [∀ (p q : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.X p).X (q + 1)) ((L.X p).X q)] [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] [∀ (n : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.total (ComplexShape.up ℤ)).X (n + 1)) ((L.total (ComplexShape.up ℤ)).X n)] : (columnCone f).HasTotal (ComplexShape.up ℤ)

Construct a literal total of the vertical column cone from the two given totals. Only the pointwise and total-degree biproducts are needed.

noncomputable def HomologicalComplex₂.totalColumnConeIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) [∀ (p q : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.X p).X (q + 1)) ((L.X p).X q)] [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] [∀ (n : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.total (ComplexShape.up ℤ)).X (n + 1)) ((L.total (ComplexShape.up ℤ)).X n)] : (columnCone f).total (ComplexShape.up ℤ) ≅ CochainComplex.mappingCone (total.map f (ComplexShape.up ℤ))

The literal total of the vertical column cone is the mapping cone of the literal total map. The source branch at horizontal degree p acquires the sign (-1)^p; the target branch is unchanged.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex₂.ι_totalColumnConeIso_hom_source {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) [∀ (p q : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.X p).X (q + 1)) ((L.X p).X q)] [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] [∀ (n : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.total (ComplexShape.up ℤ)).X (n + 1)) ((L.total (ComplexShape.up ℤ)).X n)] (p q n : ℤ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (((CochainComplex.mappingCone.inl ((flipFunctor C (ComplexShape.up ℤ) (ComplexShape.up ℤ)).map f)).v (q + 1) q ⋯).f p) (CategoryTheory.CategoryStruct.comp ((columnCone f).ιTotal (ComplexShape.up ℤ) p q n ⋯) ((totalColumnConeIso f).hom.f n)) = CategoryTheory.CategoryStruct.comp (p.negOnePow • K.ιTotal (ComplexShape.up ℤ) p (q + 1) (n + 1) ⋯) ((CochainComplex.mappingCone.inl (total.map f (ComplexShape.up ℤ))).v (n + 1) n ⋯)

This source-branch rewrite rule exposes the sign needed to reconcile totalization with the negated differential on the shifted cone source.

theorem HomologicalComplex₂.ι_totalColumnConeIso_hom_target {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) [∀ (p q : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.X p).X (q + 1)) ((L.X p).X q)] [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] [∀ (n : ℤ), CategoryTheory.Limits.HasBinaryBiproduct ((K.total (ComplexShape.up ℤ)).X (n + 1)) ((L.total (ComplexShape.up ℤ)).X n)] (p q n : ℤ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (((CochainComplex.mappingCone.inr ((flipFunctor C (ComplexShape.up ℤ) (ComplexShape.up ℤ)).map f)).f q).f p) (CategoryTheory.CategoryStruct.comp ((columnCone f).ιTotal (ComplexShape.up ℤ) p q n ⋯) ((totalColumnConeIso f).hom.f n)) = CategoryTheory.CategoryStruct.comp (L.ιTotal (ComplexShape.up ℤ) p q n ⋯) ((CochainComplex.mappingCone.inr (total.map f (ComplexShape.up ℤ))).f n)

Use this rule to transport the target-cone inclusion through the comparison without unfolding the coproduct descent maps.

theorem HomologicalComplex₂.quasiIso_totalMap_of_four_diagonal_bounds_of_column_quasiIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] (aK bK aL bL : ℤ → ℤ) (hKLower : ∀ (n p q : ℤ), p + q = n → p < aK n → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hKUpper : ∀ (n p q : ℤ), p + q = n → bK n < p → CategoryTheory.Limits.IsZero ((K.X p).X q)) (hLLower : ∀ (n p q : ℤ), p + q = n → p < aL n → CategoryTheory.Limits.IsZero ((L.X p).X q)) (hLUpper : ∀ (n p q : ℤ), p + q = n → bL n < p → CategoryTheory.Limits.IsZero ((L.X p).X q)) (hcol : ∀ (p : ℤ), QuasiIso (f.f p)) : QuasiIso (total.map f (ComplexShape.up ℤ))

A columnwise quasi-isomorphism induces a quasi-isomorphism of literal totals under finite diagonal support. The proof applies total acyclicity to the column cone: its degree n support combines source bounds at n + 1 with target bounds at n, then uses HomologicalComplex₂.totalColumnConeIso. These are bounds on the terms themselves; bounds on cohomology alone do not provide this support.