Truncation functors commute with the shift

For a t-structure t on a pretriangulated category and a n : ℤ,

((t.truncLT (a + n)).obj X)⟦n⟧ ≅ (t.truncLT a).obj (X⟦n⟧)
((t.truncGE (a + n)).obj X)⟦n⟧ ≅ (t.truncGE a).obj (X⟦n⟧)

Why this is not in Mathlib

Mathlib's truncation API (TruncLTGE.lean, TruncLEGT.lean) has no shift lemmas at all, at either of the revisions this project pins — v4.29.0 (8a178386) and v4.32.1 (520045ab). The functors, their natural transformations, the truncation triangle and its uniqueness are all present; the interaction with shiftFunctor is simply absent. This file is Mathlib-shaped and is written to be upstreamed.

The proof, in one paragraph

Shifting the truncation triangle τ<ᵃ⁺ⁿX → X → τ≥ᵃ⁺ⁿX → [1] by n gives a distinguished triangle (Triangle.shift_distinguished) whose middle object is X⟦n⟧, whose first object is IsLE (a-1) and whose third is IsGE a (t.isLE_shift, t.isGE_shift). The truncation triangle of X⟦n⟧ at a has exactly the same three properties. Mathlib's t.triangle_iso_exists says a distinguished triangle with an IsLE (a-1) first object and an IsGE a third object is determined up to isomorphism by its middle object, so the two are isomorphic over 𝟙 (X⟦n⟧) — and both isomorphisms fall out of the single triangle isomorphism at once.

That uniqueness lemma is the whole content. Everything else is bookkeeping.

Downstream

This is what originalHeartCohFunctor t n ≅ shiftFunctor C n ⋙ originalHeartCohFunctor t 0 needs, and hence what upgrades heart cohomology from homological at n = 0 to homological in every degree. See issue #151.

noncomputable def CategoryTheory.Triangulated.TStructure.shiftedTriangleLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : Pretriangulated.Triangle C

The truncation triangle of X at a + n, shifted by n.

Its middle object is X⟦n⟧, so it is a candidate for the truncation triangle of X⟦n⟧ at a; the point of this file is that it is one.

Equations

• t.shiftedTriangleLTGE a n X = (CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n).obj ((t.triangleLTGE (a + n)).obj X)

theorem CategoryTheory.Triangulated.TStructure.shiftedTriangleLTGE_distinguished {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : t.shiftedTriangleLTGE a n X ∈ Pretriangulated.distinguishedTriangles

instance CategoryTheory.Triangulated.TStructure.isLE_shiftedTriangleLTGE_obj₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : t.IsLE (t.shiftedTriangleLTGE a n X).obj₁ (a - 1)

instance CategoryTheory.Triangulated.TStructure.isGE_shiftedTriangleLTGE_obj₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : t.IsGE (t.shiftedTriangleLTGE a n X).obj₃ a

theorem CategoryTheory.Triangulated.TStructure.exists_shiftedTriangleLTGE_iso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : ∃ (e : t.shiftedTriangleLTGE a n X ≅ (t.triangleLTGE a).obj ((shiftFunctor C n).obj X)), e.hom.hom₂ = CategoryStruct.id (t.shiftedTriangleLTGE a n X).obj₂

Uniqueness of the truncation decomposition, applied to the shifted truncation triangle: it is isomorphic to the truncation triangle of X⟦n⟧ at a, over the identity of X⟦n⟧.

noncomputable def CategoryTheory.Triangulated.TStructure.shiftedTriangleLTGEIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : t.shiftedTriangleLTGE a n X ≅ (t.triangleLTGE a).obj ((shiftFunctor C n).obj X)

The chosen triangle isomorphism. Both truncation-shift isomorphisms below are components of this one.

Equations

• t.shiftedTriangleLTGEIso a n X = ⋯.choose

theorem CategoryTheory.Triangulated.TStructure.shiftedTriangleLTGEIso_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : (t.shiftedTriangleLTGEIso a n X).hom.hom₂ = CategoryStruct.id ((shiftFunctor C n).obj X)

noncomputable def CategoryTheory.Triangulated.TStructure.truncLTShiftIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : (shiftFunctor C n).obj ((t.truncLT (a + n)).obj X) ≅ (t.truncLT a).obj ((shiftFunctor C n).obj X)

truncLT commutes with the shift.

Equations

• t.truncLTShiftIso a n X = CategoryTheory.Pretriangulated.Triangle.π₁.mapIso (t.shiftedTriangleLTGEIso a n X)

noncomputable def CategoryTheory.Triangulated.TStructure.truncGEShiftIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : (shiftFunctor C n).obj ((t.truncGE (a + n)).obj X) ≅ (t.truncGE a).obj ((shiftFunctor C n).obj X)

truncGE commutes with the shift.

Equations

• t.truncGEShiftIso a n X = CategoryTheory.Pretriangulated.Triangle.π₃.mapIso (t.shiftedTriangleLTGEIso a n X)

theorem CategoryTheory.Triangulated.TStructure.truncLTShiftIso_hom_comp_truncLTι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : CategoryStruct.comp (t.truncLTShiftIso a n X).hom ((t.truncLTι a).app ((shiftFunctor C n).obj X)) = n.negOnePow • (shiftFunctor C n).map ((t.truncLTι (a + n)).app X)

The truncLT isomorphism sits over X⟦n⟧, up to the sign (-1)ⁿ.

The sign is not an artefact of the proof: Triangle.shiftFunctor multiplies a triangle's maps by n.negOnePow, which is exactly why shiftFunctor C n is not a triangulated functor on the nose. Any downstream use of these isomorphisms inherits the sign, so it is stated rather than absorbed.

theorem CategoryTheory.Triangulated.TStructure.truncLTShiftIso_hom_comp_truncLTι_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) {Z : C} (h : (shiftFunctor C n).obj X ⟶ Z) : CategoryStruct.comp (t.truncLTShiftIso a n X).hom (CategoryStruct.comp ((t.truncLTι a).app ((shiftFunctor C n).obj X)) h) = CategoryStruct.comp (n.negOnePow • (shiftFunctor C n).map ((t.truncLTι (a + n)).app X)) h

The truncLT isomorphism sits over X⟦n⟧, up to the sign (-1)ⁿ.

The sign is not an artefact of the proof: Triangle.shiftFunctor multiplies a triangle's maps by n.negOnePow, which is exactly why shiftFunctor C n is not a triangulated functor on the nose. Any downstream use of these isomorphisms inherits the sign, so it is stated rather than absorbed.

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEShiftIso_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : CategoryStruct.comp (n.negOnePow • (shiftFunctor C n).map ((t.truncGEπ (a + n)).app X)) (t.truncGEShiftIso a n X).hom = (t.truncGEπ a).app ((shiftFunctor C n).obj X)

The truncGE isomorphism sits under X⟦n⟧, up to the sign (-1)ⁿ; see the note on truncLTShiftIso_hom_comp_truncLTι.

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEShiftIso_hom_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) {Z : C} (h : (t.truncGE a).obj ((shiftFunctor C n).obj X) ⟶ Z) : CategoryStruct.comp (n.negOnePow • (shiftFunctor C n).map ((t.truncGEπ (a + n)).app X)) (CategoryStruct.comp (t.truncGEShiftIso a n X).hom h) = CategoryStruct.comp ((t.truncGEπ a).app ((shiftFunctor C n).obj X)) h

The truncGE isomorphism sits under X⟦n⟧, up to the sign (-1)ⁿ; see the note on truncLTShiftIso_hom_comp_truncLTι.

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEShiftIso_inv {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) : CategoryStruct.comp ((t.truncGEπ a).app ((shiftFunctor C n).obj X)) (t.truncGEShiftIso a n X).inv = n.negOnePow • (shiftFunctor C n).map ((t.truncGEπ (a + n)).app X)

Inverse form of truncGEπ_comp_truncGEShiftIso_hom, used to prove naturality of the comparison.

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEShiftIso_inv_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n : ℤ) (X : C) {Z : C} (h : (shiftFunctor C n).obj ((t.truncGE (a + n)).obj X) ⟶ Z) : CategoryStruct.comp ((t.truncGEπ a).app ((shiftFunctor C n).obj X)) (CategoryStruct.comp (t.truncGEShiftIso a n X).inv h) = CategoryStruct.comp (n.negOnePow • (shiftFunctor C n).map ((t.truncGEπ (a + n)).app X)) h

Inverse form of truncGEπ_comp_truncGEShiftIso_hom, used to prove naturality of the comparison.