Degree-at-least stupid truncations and retained components

Mathlib's degree-at-least stupid truncation has a canonical inclusion into its source cochain complex. Nested truncations have compatible inclusion maps in any category with zero morphisms and a zero object.

Main definitions

• HomologicalComplex.stupidTruncGEι includes a tail in its source complex.
• HomologicalComplex.stupidTruncGEMap includes a deeper tail in a shallower one.
• HomologicalComplex.stupidTruncGETower and HomologicalComplex.stupidTruncGETowerCocone collect the nested tails.
• HomologicalComplex.stupidTruncGEXIso chooses one component isomorphism at every retained integer degree, with a bicomplex specialization at HomologicalComplex₂.stupidTruncGEXIso.

Main results

• HomologicalComplex.stupidTruncGEMap_self and HomologicalComplex.stupidTruncGEMap_comp give the nested-tail laws.
• HomologicalComplex.isColimitStupidTruncGETowerCocone proves that the tower recovers the original complex as a colimit.
• HomologicalComplex.stupidTrunc_d_eq describes the retained differential.
• HomologicalComplex.stupidTruncMap_comp_stupidTruncGEι proves naturality of the tail inclusion, and HomologicalComplex.stupidTruncGEι_isIso_of_isZero detects an isomorphism when the discarded components vanish.
• HomologicalComplex.stupidTruncGEMap_naturality commutes tail inclusion with a cochain map.

Implementation notes

On retained degrees, the maps use Mathlib's canonical truncation isomorphism; outside the tail they use zero morphisms. The inclusion into the source is monic, so it characterizes the nested maps and proves their laws. At each fixed degree, the lower-tail tower eventually becomes constant; Mathlib's degreewise colimit criterion assembles these into a complex colimit.

References

This extends Mathlib's HomologicalComplex.stupidTrunc and HomologicalComplex.stupidTruncXIso in Algebra/Homology/Embedding/StupidTrunc.lean.

noncomputable def HomologicalComplex.stupidTruncGEXIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p i : ℤ) (hi : p ≤ i) : (K.stupidTrunc (ComplexShape.embeddingUpIntGE p)).X i ≅ K.X i

The component of a degree-at-least stupid truncation at a retained integer degree. This chooses the normalized index (i - p).toNat for Mathlib's HomologicalComplex.stupidTruncXIso; HomologicalComplex.stupidTruncXIso_eq_stupidTruncGEXIso identifies every retained-index presentation with this one.

Equations

• K.stupidTruncGEXIso p i hi = K.stupidTruncXIso (ComplexShape.embeddingUpIntGE p) ⋯

theorem HomologicalComplex.stupidTruncXIso_eq_stupidTruncGEXIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p i : ℤ) (k : ℕ) (h : (ComplexShape.embeddingUpIntGE p).f k = i) : K.stupidTruncXIso (ComplexShape.embeddingUpIntGE p) h = K.stupidTruncGEXIso p i ⋯

The embedding equation forces k = (i - p).toNat. Substituting that unique index identifies Mathlib's component isomorphism with the normalized one, independent of the caller's witness.

theorem HomologicalComplex.stupidTrunc_d_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p : ℤ) {i j : ℤ} (hi : p ≤ i) (hj : p ≤ j) : (K.stupidTrunc (ComplexShape.embeddingUpIntGE p)).d i j = CategoryTheory.CategoryStruct.comp (K.stupidTruncXIso (ComplexShape.embeddingUpIntGE p) ⋯).hom (CategoryTheory.CategoryStruct.comp (K.d i j) (K.stupidTruncXIso (ComplexShape.embeddingUpIntGE p) ⋯).inv)

noncomputable def HomologicalComplex.stupidTruncGEι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p : ℤ) : K.stupidTrunc (ComplexShape.embeddingUpIntGE p) ⟶ K

On retained degrees this uses HomologicalComplex.stupidTruncXIso; below p its source component is zero. The resulting map is monic without an abelian-category assumption.

Equations

• K.stupidTruncGEι p = { f := fun (i : ℤ) => if hi : p ≤ i then (K.stupidTruncXIso (ComplexShape.embeddingUpIntGE p) ⋯).hom else 0, comm' := ⋯ }

theorem HomologicalComplex.stupidTruncMap_comp_stupidTruncGEι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C (ComplexShape.up ℤ)} (f : K ⟶ L) (p : ℤ) : CategoryTheory.CategoryStruct.comp (stupidTruncMap f (ComplexShape.embeddingUpIntGE p)) (L.stupidTruncGEι p) = CategoryTheory.CategoryStruct.comp (K.stupidTruncGEι p) f

On retained degrees, the naturality square commutes by Mathlib's canonical truncation isomorphisms; below the cutoff its source is zero.

theorem HomologicalComplex.stupidTruncMap_comp_stupidTruncGEι_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C (ComplexShape.up ℤ)} (f : K ⟶ L) (p : ℤ) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp (stupidTruncMap f (ComplexShape.embeddingUpIntGE p)) (CategoryTheory.CategoryStruct.comp (L.stupidTruncGEι p) h) = CategoryTheory.CategoryStruct.comp (K.stupidTruncGEι p) (CategoryTheory.CategoryStruct.comp f h)

On retained degrees, the naturality square commutes by Mathlib's canonical truncation isomorphisms; below the cutoff its source is zero.

theorem HomologicalComplex.stupidTruncGEι_isIso_of_isZero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p : ℤ) (hK : ∀ i < p, CategoryTheory.Limits.IsZero (K.X i)) : CategoryTheory.IsIso (K.stupidTruncGEι p)

The inclusion is the canonical component isomorphism above the cutoff and the unique map between zero objects below it.

instance HomologicalComplex.stupidTruncGEι_f_mono {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p i : ℤ) : CategoryTheory.Mono ((K.stupidTruncGEι p).f i)

instance HomologicalComplex.stupidTruncGEι_mono {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p : ℤ) : CategoryTheory.Mono (K.stupidTruncGEι p)

noncomputable def HomologicalComplex.stupidTruncGEMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p q : ℤ) (hpq : p ≤ q) : K.stupidTrunc (ComplexShape.embeddingUpIntGE q) ⟶ K.stupidTrunc (ComplexShape.embeddingUpIntGE p)

Compatibility with the monic HomologicalComplex.stupidTruncGEι maps characterizes this nested-tail inclusion; cancellation gives its identity and composition laws.

Equations

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

@[simp]

theorem HomologicalComplex.stupidTruncGEMap_comp_ι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p q : ℤ) (hpq : p ≤ q) : CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap p q hpq) (K.stupidTruncGEι p) = K.stupidTruncGEι q

@[simp]

theorem HomologicalComplex.stupidTruncGEMap_comp_ι_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p q : ℤ) (hpq : p ≤ q) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap p q hpq) (CategoryTheory.CategoryStruct.comp (K.stupidTruncGEι p) h) = CategoryTheory.CategoryStruct.comp (K.stupidTruncGEι q) h

@[simp]

theorem HomologicalComplex.stupidTruncGEMap_self {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p : ℤ) : K.stupidTruncGEMap p p ⋯ = CategoryTheory.CategoryStruct.id (K.stupidTrunc (ComplexShape.embeddingUpIntGE p))

@[simp]

theorem HomologicalComplex.stupidTruncGEMap_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p q r : ℤ) (hpq : p ≤ q) (hqr : q ≤ r) : CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap q r hqr) (K.stupidTruncGEMap p q hpq) = K.stupidTruncGEMap p r ⋯

@[simp]

theorem HomologicalComplex.stupidTruncGEMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C (ComplexShape.up ℤ)) (p q r : ℤ) (hpq : p ≤ q) (hqr : q ≤ r) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : K.stupidTrunc (ComplexShape.embeddingUpIntGE p) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap q r hqr) (CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap p q hpq) h) = CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap p r ⋯) h

theorem HomologicalComplex.stupidTruncGEMap_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C (ComplexShape.up ℤ)} (f : K ⟶ L) (p q : ℤ) (hpq : p ≤ q) : CategoryTheory.CategoryStruct.comp (stupidTruncMap f (ComplexShape.embeddingUpIntGE q)) (L.stupidTruncGEMap p q hpq) = CategoryTheory.CategoryStruct.comp (K.stupidTruncGEMap p q hpq) (stupidTruncMap f (ComplexShape.embeddingUpIntGE p))

A cochain map commutes with nested-tail inclusion. On retained degrees, both composites reduce to the same map after transporting through the stupid-truncation degreewise isomorphisms; elsewhere the source is zero.

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

Stage n has lower cutoff c - n. If the components of K vanish above some degree, each stage has finite degree support. The colimit construction needs no such bound.

Equations

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

noncomputable def HomologicalComplex.stupidTruncGETowerCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (c : ℤ) : CategoryTheory.Limits.Cocone (stupidTruncGETower K c)

The stage inclusions commute with the transition maps, and the vertex is definitionally K; this lets the degreewise colimit criterion apply directly.

Equations

• HomologicalComplex.stupidTruncGETowerCocone K c = { pt := K, ι := { app := fun (n : ℕ) => HomologicalComplex.stupidTruncGEι K (c - ↑n), naturality := ⋯ } }

noncomputable def HomologicalComplex.isColimitStupidTruncGETowerCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (c : ℤ) : CategoryTheory.Limits.IsColimit (stupidTruncGETowerCocone K c)

The lower stupid truncations recover every complex: at each fixed degree, the inclusions are eventually isomorphisms. No upper bound or ambient colimits are required.

Equations

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

noncomputable def HomologicalComplex₂.stupidTruncGEXIso {C : Type w} [CategoryTheory.Category.{v_1, w} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p i : ℤ) (hi : p ≤ i) : (HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntGE p)).X i ≅ K.X i

The bicomplex specialization of the normalized retained component HomologicalComplex.stupidTruncGEXIso. It is definitionally the same iso as Mathlib's HomologicalComplex.stupidTruncXIso at index (i - p).toNat.

Equations

• K.stupidTruncGEXIso p i hi = HomologicalComplex.stupidTruncGEXIso K p i hi

@[simp]

theorem HomologicalComplex₂.stupidTruncXIso_eq_stupidTruncGEXIso {C : Type w} [CategoryTheory.Category.{v_1, w} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p i : ℤ) (k : ℕ) (h : (ComplexShape.embeddingUpIntGE p).f k = i) : HomologicalComplex.stupidTruncXIso K (ComplexShape.embeddingUpIntGE p) h = K.stupidTruncGEXIso p i ⋯

@[simp]

theorem HomologicalComplex₂.stupidTruncGEXIso_inv_hom_f {C : Type w} [CategoryTheory.Category.{v_1, w} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p i j : ℤ) (hi hi' : p ≤ i) : CategoryTheory.CategoryStruct.comp ((K.stupidTruncGEXIso p i hi).inv.f j) ((K.stupidTruncGEXIso p i hi').hom.f j) = CategoryTheory.CategoryStruct.id ((K.X i).X j)

@[simp]

theorem HomologicalComplex₂.stupidTruncGEXIso_inv_hom_f_assoc {C : Type w} [CategoryTheory.Category.{v_1, w} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p i j : ℤ) (hi hi' : p ≤ i) {Z : C} (h : (K.X i).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.stupidTruncGEXIso p i hi).inv.f j) (CategoryTheory.CategoryStruct.comp ((K.stupidTruncGEXIso p i hi').hom.f j) h) = h

@[simp]

theorem HomologicalComplex₂.stupidTruncGEXIso_hom_inv_f {C : Type w} [CategoryTheory.Category.{v_1, w} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p i j : ℤ) (hi hi' : p ≤ i) : CategoryTheory.CategoryStruct.comp ((K.stupidTruncGEXIso p i hi).hom.f j) ((K.stupidTruncGEXIso p i hi').inv.f j) = CategoryTheory.CategoryStruct.id (((HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntGE p)).X i).X j)

@[simp]

theorem HomologicalComplex₂.stupidTruncGEXIso_hom_inv_f_assoc {C : Type w} [CategoryTheory.Category.{v_1, w} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p i j : ℤ) (hi hi' : p ≤ i) {Z : C} (h : ((HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntGE p)).X i).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.stupidTruncGEXIso p i hi).hom.f j) (CategoryTheory.CategoryStruct.comp ((K.stupidTruncGEXIso p i hi').inv.f j) h) = h