Naturality of truncation--shift comparisons

The objectwise truncation--shift isomorphisms from TStructure.Shift assemble into natural isomorphisms. The signs in their compatibility with the truncation unit and counit cancel by centrality of scalar multiplication.

noncomputable def CategoryTheory.Triangulated.TStructure.truncLTShiftNatIso {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 : ℤ) : (t.truncLT (a + n)).comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp (t.truncLT a)

The truncLT shift comparison is natural in the object.

Equations

• t.truncLTShiftNatIso a n = CategoryTheory.NatIso.ofComponents (fun (X : C) => t.truncLTShiftIso a n X) ⋯

noncomputable def CategoryTheory.Triangulated.TStructure.truncGEShiftNatIso {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 : ℤ) : (t.truncGE (a + n)).comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp (t.truncGE a)

The truncGE shift comparison is natural in the object.

Equations

• t.truncGEShiftNatIso a n = CategoryTheory.NatIso.ofComponents (fun (X : C) => t.truncGEShiftIso a n X) ⋯

noncomputable def CategoryTheory.Triangulated.TStructure.truncLEShiftNatIso {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 : ℤ) : (t.truncLE (a + n)).comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp (t.truncLE a)

The truncLE shift comparison, obtained from truncLTShiftNatIso by the canonical identification truncLE a ≅ truncLT (a + 1).

Equations

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

noncomputable def CategoryTheory.Triangulated.TStructure.truncGELEShiftNatIso {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 : ℤ) : (t.truncGELE (a + n) (a + n)).comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp (t.truncGELE a a)

Pure truncation commutes naturally with the shift.

Equations

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