Total complex of a bicomplex supported in degree zero

Placing an integer-indexed cochain complex in horizontal degree zero gives a bicomplex whose total is naturally isomorphic to the original complex. Exchanging axes gives the corresponding vertical-degree-zero comparison. Under an ambient total-existence assumption, the signed flipped comparison is natural in the input integer-indexed cochain complex. For any source complex shape embedded into integer cochains with a chosen degree mapping to zero, the total of its extended single is naturally the input integer-indexed cochain complex.

Main definitions

• HomologicalComplex₂.singleZeroBicomplex places a complex in horizontal degree zero.

Main results

• HomologicalComplex₂.singleZeroHasTotal constructs its total without ambient coproducts.
• HomologicalComplex₂.singleZeroTotalIso and HomologicalComplex₂.singleZeroTotalIso_naturality identify that total naturally with the original complex.
• HomologicalComplex₂.singleZeroFlipTotalIso and HomologicalComplex₂.singleZeroFlipTotalIso_naturality give the corresponding comparison after exchanging axes.
• HomologicalComplex₂.singleZeroFlipTotalNatIso assembles the signed flipped degree-zero comparisons into a natural isomorphism.
• HomologicalComplex₂.singleExtendMapTotalIso compares the total of an extended single with the original complex when the selected degree maps to zero.

Implementation notes

The total-degree n diagonal has one surviving summand, at (0, n). Its cofan supplies the required total in any preadditive category with a zero object. The flipped comparison uses Mathlib's signed total symmetry, so its sign agrees with the existing totalization convention. The natural isomorphism uses these component isomorphisms and their proved naturality, rather than changing the sign convention. The extended-single comparison first normalizes the bicomplex, then applies that signed isomorphism.

References

The construction uses Mathlib's HomologicalComplex.single and HomologicalComplex₂.totalFlipIso and the repository's HomologicalComplex₂.singleExtendMapFlipIso. It introduces no geometric assumptions.

noncomputable def HomologicalComplex₂.singleZeroBicomplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : CochainComplex C ℤ) : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)

A bicomplex concentrated in horizontal degree zero.

Equations

• HomologicalComplex₂.singleZeroBicomplex A = (HomologicalComplex.single (CochainComplex C ℤ) (ComplexShape.up ℤ) 0).obj A

noncomputable def HomologicalComplex₂.singleZeroXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : CochainComplex C ℤ) (i : ℤ) (hi : i = 0) : (singleZeroBicomplex A).X i ≅ A

Accepts an explicit equality identifying the horizontal index with zero, so callers can evaluate at their existing index without first rewriting the whole bicomplex.

Equations

• HomologicalComplex₂.singleZeroXIso A i hi = ⋯ ▸ HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 A

noncomputable def HomologicalComplex₂.singleZeroBicomplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {A B : CochainComplex C ℤ} (f : A ⟶ B) : singleZeroBicomplex A ⟶ singleZeroBicomplex B

Apply a cochain map to the supported horizontal degree. This uses no additive structure beyond the zero morphisms needed to form the single complex.

Equations

• HomologicalComplex₂.singleZeroBicomplexMap f = (HomologicalComplex.single (CochainComplex C ℤ) (ComplexShape.up ℤ) 0).map f

instance HomologicalComplex₂.singleZeroHasTotal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : CochainComplex C ℤ) : (singleZeroBicomplex A).HasTotal (ComplexShape.up ℤ)

The unique supported summand gives the total cofan without a category-wide coproduct assumption.

noncomputable def HomologicalComplex₂.singleZeroTotalXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : CochainComplex C ℤ) (n : ℤ) : ((singleZeroBicomplex A).total (ComplexShape.up ℤ)).X n ≅ A.X n

Projects the total-degree diagonal onto its surviving (0,n) summand; the inverse is that summand's canonical inclusion. Every other summand is zero.

Equations

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

noncomputable def HomologicalComplex₂.singleZeroTotalIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : CochainComplex C ℤ) : (singleZeroBicomplex A).total (ComplexShape.up ℤ) ≅ A

The horizontal differential vanishes and the totalization sign on the surviving column is positive, so the component projections commute with the original differential.

Equations

• HomologicalComplex₂.singleZeroTotalIso A = HomologicalComplex.Hom.isoOfComponents (HomologicalComplex₂.singleZeroTotalXIso A) ⋯

theorem HomologicalComplex₂.singleZeroTotalIso_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {A B : CochainComplex C ℤ} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (total.map (singleZeroBicomplexMap f) (ComplexShape.up ℤ)) (singleZeroTotalIso B).hom = CategoryTheory.CategoryStruct.comp (singleZeroTotalIso A).hom f

The total-complex identification for a bicomplex supported in horizontal degree zero is natural.

theorem HomologicalComplex₂.singleZeroTotalIso_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {A B : CochainComplex C ℤ} (f : A ⟶ B) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (total.map (singleZeroBicomplexMap f) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (singleZeroTotalIso B).hom h) = CategoryTheory.CategoryStruct.comp (singleZeroTotalIso A).hom (CategoryTheory.CategoryStruct.comp f h)

The total-complex identification for a bicomplex supported in horizontal degree zero is natural.

noncomputable def HomologicalComplex₂.singleZeroFlipTotalIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : CochainComplex C ℤ) : (singleZeroBicomplex A).flip.total (ComplexShape.up ℤ) ≅ A

Exchanges axes using Mathlib's signed total symmetry, then applies HomologicalComplex₂.singleZeroTotalIso, preserving the established totalization sign.

Equations

• HomologicalComplex₂.singleZeroFlipTotalIso A = (HomologicalComplex₂.singleZeroBicomplex A).totalFlipIso (ComplexShape.up ℤ) ≪≫ HomologicalComplex₂.singleZeroTotalIso A

theorem HomologicalComplex₂.singleZeroFlipTotalIso_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {A B : CochainComplex C ℤ} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (total.map (flipMap (singleZeroBicomplexMap f)) (ComplexShape.up ℤ)) (singleZeroFlipTotalIso B).hom = CategoryTheory.CategoryStruct.comp (singleZeroFlipTotalIso A).hom f

Composes naturality of the signed total symmetry with naturality of the first-axis comparison.

theorem HomologicalComplex₂.singleZeroFlipTotalIso_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {A B : CochainComplex C ℤ} (f : A ⟶ B) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (total.map (flipMap (singleZeroBicomplexMap f)) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (singleZeroFlipTotalIso B).hom h) = CategoryTheory.CategoryStruct.comp (singleZeroFlipTotalIso A).hom (CategoryTheory.CategoryStruct.comp f h)

Composes naturality of the signed total symmetry with naturality of the first-axis comparison.

noncomputable def HomologicalComplex₂.singleZeroFlipTotalNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)), K.HasTotal (ComplexShape.up ℤ)] : (HomologicalComplex.single (CochainComplex C ℤ) (ComplexShape.up ℤ) 0).comp ((flipFunctor C (ComplexShape.up ℤ) (ComplexShape.up ℤ)).comp (totalFunctor C (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ))) ≅ CategoryTheory.Functor.id (CochainComplex C ℤ)

Packages HomologicalComplex₂.singleZeroFlipTotalIso into a natural isomorphism. Mathlib's HomologicalComplex₂.totalFunctor requires totals for every bicomplex; the objectwise single-zero totals alone do not construct that functor. Flipping moves support from outer to inner degree zero.

Equations

• HomologicalComplex₂.singleZeroFlipTotalNatIso = CategoryTheory.NatIso.ofComponents (fun (K : CochainComplex C ℤ) => HomologicalComplex₂.singleZeroFlipTotalIso K) ⋯

noncomputable def HomologicalComplex₂.singleExtendMapTotalIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)), K.HasTotal (ComplexShape.up ℤ)] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (e : c.Embedding (ComplexShape.up ℤ)) (i : ι) (h : e.f i = 0) : (((HomologicalComplex.single C c i).comp (e.extendFunctor C)).mapHomologicalComplex (ComplexShape.up ℤ)).comp (totalFunctor C (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ)) ≅ CategoryTheory.Functor.id (CochainComplex C ℤ)

Extend a single along any complex-shape embedding whose chosen degree maps to integer degree zero. The pre-total bicomplex isomorphism identifies its target with the flipped single-zero bicomplex; the signed total natural isomorphism then recovers the input cochain complex.

Equations

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