Quasi-isomorphisms for mapping cones and first-quadrant totals

This file proves quasi-isomorphism criteria for mapping-cone maps and first-quadrant total complexes of abelian groups.

Main definitions

• HomologicalComplex₂.IsVerticallyConnective records vanishing in negative vertical degrees.
• HomologicalComplex₂.IsHorizontallyConnective records vanishing in negative horizontal degrees.

Main results

• CochainComplex.mappingCone.quasiIso_compMap deduces a quasi-isomorphism for the cone map of a composite from quasi-isomorphisms for the two constituent cone maps.
• CochainComplex.mappingCone.quasiIsoAt_inr_of_isZero_X gives a quasi-isomorphism at the cone inclusion in degree n when the source A of the arrow f : A ⟶ B vanishes in degrees n and n + 1.
• HomologicalComplex₂.totalMap_quasiIso turns a columnwise quasi-isomorphism of first-quadrant bicomplexes of abelian groups into a quasi-isomorphism of their totals.

Implementation notes

The composition result uses the octahedral mapping-cone triangle in the derived category. The total result compares finite-column cones through adjacent-column maps, then identifies the connective tail with the full total. The generic adjacent-column maps and their cone quasi-isomorphism are in FilteredTotalComplexAdjacentCore. The middle-term short-exact comparison lives at the separate generic homology-sequence owner. The downstream finite-strip comparison in FiniteStripTotal uses derived short-exact triangles directly.

References

These proofs use Mathlib's mapping-cone composition triangle, derived-category localization, and homological-complex totalization.

theorem CochainComplex.mappingCone.quasiIso_compMap {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CochainComplex AddCommGrpCat ℤ} {f : X₁ ⟶ X₂} {g : X₂ ⟶ X₃} {f' : Y₁ ⟶ Y₂} {g' : Y₂ ⟶ Y₃} (a : X₁ ⟶ Y₁) (b : X₂ ⟶ Y₂) (c : X₃ ⟶ Y₃) (hf : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') (hg : CategoryTheory.CategoryStruct.comp g c = CategoryTheory.CategoryStruct.comp b g') [QuasiIso (map f f' a b hf)] [QuasiIso (map g g' b c hg)] : QuasiIso (map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g') a c ⋯)

In a morphism between two composable pairs of cochain-complex maps, quasi-isomorphisms on the mapping cones of the two individual maps imply a quasi-isomorphism on the mapping cone of their composites. This is the octahedral analogue of the five lemma.

theorem CochainComplex.mappingCone.quasiIsoAt_inr_of_isZero_X {A B : CochainComplex AddCommGrpCat ℤ} (f : A ⟶ B) (n : ℤ) (hn : CategoryTheory.Limits.IsZero (A.X n)) (hn₁ : CategoryTheory.Limits.IsZero (A.X (n + 1))) : QuasiIsoAt (inr f) n

If the source complex vanishes in two adjacent degrees, the canonical inclusion into the mapping cone is a quasi-isomorphism in the lower degree.

def HomologicalComplex₂.IsVerticallyConnective (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) : Prop

A bicomplex is vertically connective when every term in negative vertical degree is zero.

Equations

• K.IsVerticallyConnective = ∀ (p q : ℤ), q < 0 → CategoryTheory.Limits.IsZero ((K.X p).X q)

def HomologicalComplex₂.IsHorizontallyConnective (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) : Prop

A bicomplex is horizontally connective when every term in negative horizontal degree is zero.

Equations

• K.IsHorizontallyConnective = ∀ (p q : ℤ), p < 0 → CategoryTheory.Limits.IsZero ((K.X p).X q)

theorem HomologicalComplex₂.totalMap_quasiIso {K L : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (hKv : K.IsVerticallyConnective) (hLv : L.IsVerticallyConnective) (hKh : K.IsHorizontallyConnective) (hLh : L.IsHorizontallyConnective) (hcol : ∀ (n : ℕ), QuasiIso (f.f ↑n)) : QuasiIso (total.map f (ComplexShape.up ℤ))

A columnwise quasi-isomorphism between first-quadrant bicomplexes of abelian groups induces a quasi-isomorphism on their total complexes.