Canonical good-truncation towers

Mathlib's good truncations assemble into a natural ℕ-indexed tower. Under local homology hypotheses, their inclusion cocone is colimiting.

Main definitions

CochainComplex.truncLEToTruncLE gives the transitions; CochainComplex.truncLETower and CochainComplex.truncLETowerCocone assemble the diagram and its inclusions; CochainComplex.truncLETowerMap acts on morphisms.

Main results

CochainComplex.isColimitTruncLETowerCocone proves the colimit property; CochainComplex.isColimitMapTruncLETowerCocone proves it after applying a zero-morphism-preserving functor degreewise.

Implementation notes

At degree p, the inclusion is an isomorphism when the cutoff is strictly greater than p; at the cutoff the truncation contains cycles. Evaluation is eventually constant, and degreewise colimits assemble into a colimit of complexes.

References

This extends Mathlib's CochainComplex.truncLE, CochainComplex.ιTruncLE, and CochainComplex.truncLEMap.

Tags

good truncation, cochain complexes, colimits

noncomputable def CochainComplex.truncLEToTruncLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] {n m : ℤ} (h : n ≤ m) : K.truncLE n ⟶ K.truncLE m

The transition is characterized by its composite with the monic inclusion into K: that composite is the inclusion at the earlier cutoff.

Equations

• K.truncLEToTruncLE h = CategoryTheory.CategoryStruct.comp (CategoryTheory.asIso ((K.truncLE n).ιTruncLE m)).inv (CochainComplex.truncLEMap (K.ιTruncLE n) m)

theorem CochainComplex.truncLEToTruncLE_comp_ιTruncLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] {n m : ℤ} (h : n ≤ m) : CategoryTheory.CategoryStruct.comp (K.truncLEToTruncLE h) (K.ιTruncLE m) = K.ιTruncLE n

Monicity of the later inclusion makes this equation the uniqueness principle used to prove the tower's functor laws.

theorem CochainComplex.truncLEToTruncLE_comp_ιTruncLE_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] {n m : ℤ} (h : n ≤ m) {Z : CochainComplex C ℤ} (h✝ : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.truncLEToTruncLE h) (CategoryTheory.CategoryStruct.comp (K.ιTruncLE m) h✝) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) h✝

Monicity of the later inclusion makes this equation the uniqueness principle used to prove the tower's functor laws.

noncomputable def CochainComplex.truncLETower {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] : CategoryTheory.Functor ℕ (CochainComplex C ℤ)

Natural-number cutoffs are cofinal among integer cutoffs; at each fixed degree, components stabilize once the cutoff is strictly above that degree.

Equations

• K.truncLETower = { obj := fun (n : ℕ) => K.truncLE ↑n, map := fun {n m : ℕ} (f : n ⟶ m) => K.truncLEToTruncLE ⋯, map_id := ⋯, map_comp := ⋯ }

noncomputable def CochainComplex.truncLETowerCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.Cocone K.truncLETower

The transition equation makes Mathlib's inclusions a cocone. Its point is definitionally K, allowing the degreewise colimit criterion to apply directly.

Equations

• K.truncLETowerCocone = { pt := K, ι := { app := fun (n : ℕ) => K.ιTruncLE ↑n, naturality := ⋯ } }

noncomputable def CochainComplex.isColimitTruncLETowerCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsColimit K.truncLETowerCocone

The colimit exists without ambient colimit assumptions: each evaluated cocone stabilizes beyond its degree, and the degreewise colimit criterion assembles them. Local homology assumptions are needed to form Mathlib's good truncations.

Equations

• K.isColimitTruncLETowerCocone = HomologicalComplex.isColimitOfEval K.truncLETower K.truncLETowerCocone (CochainComplex.towerEvalIsColimit✝ K)

noncomputable def CochainComplex.isColimitMapTruncLETowerCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsColimit ((F.mapHomologicalComplex (ComplexShape.up ℤ)).mapCocone K.truncLETowerCocone)

A functor preserving zero morphisms sends this particular good-truncation inclusion cocone to a colimit cocone of complexes. At every fixed degree its legs eventually become isomorphisms, and the functor preserves those isomorphisms. No ambient colimit-preservation hypothesis is needed.

Equations

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

theorem CochainComplex.truncLEToTruncLE_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : CochainComplex C ℤ} [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (f : K ⟶ L) {n m : ℤ} (h : n ≤ m) : CategoryTheory.CategoryStruct.comp (truncLEMap f n) (L.truncLEToTruncLE h) = CategoryTheory.CategoryStruct.comp (K.truncLEToTruncLE h) (truncLEMap f m)

Composing both sides with the monic later inclusion reduces this compatibility to naturality of Mathlib's truncation inclusions.

noncomputable def CochainComplex.truncLETowerMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : CochainComplex C ℤ} [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (f : K ⟶ L) : K.truncLETower ⟶ L.truncLETower

Mathlib's fixed-cutoff CochainComplex.truncLEMap gives the components; transition naturality assembles them into a map of towers.

Equations

• CochainComplex.truncLETowerMap f = { app := fun (n : ℕ) => CochainComplex.truncLEMap f ↑n, naturality := ⋯ }

theorem CochainComplex.truncLETowerMap_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : CochainComplex C ℤ} [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (f : K ⟶ L) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((truncLETowerMap f).app n) (L.truncLETowerCocone.ι.app n) = CategoryTheory.CategoryStruct.comp (K.truncLETowerCocone.ι.app n) f

Together with the colimit theorem, this identifies the map induced on colimit points by CochainComplex.truncLETowerMap with the original morphism f.

theorem CochainComplex.truncLETowerMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] : truncLETowerMap (CategoryTheory.CategoryStruct.id K) = CategoryTheory.CategoryStruct.id K.truncLETower

The identity law follows stagewise from Mathlib's fixed-cutoff truncation map law.

theorem CochainComplex.truncLETowerMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L M : CochainComplex C ℤ} [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] [∀ (i : ℤ), HomologicalComplex.HasHomology M i] (f : K ⟶ L) (g : L ⟶ M) : truncLETowerMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (truncLETowerMap f) (truncLETowerMap g)

The composition law follows stagewise from Mathlib's fixed-cutoff truncation map law.