Integral shifts as triangulated functors

The ordinary shift functor commutes with every shift, but for an odd shift the commutation isomorphism used by a triangulated functor must carry the Koszul sign. This file packages that sign-correct comparison and proves that every integral shift is triangulated with respect to it.

The structures are explicit definitions rather than global instances. This avoids an instance diamond with the unsigned comparison, which remains useful for even shifts and object-only arguments. For an additive shift-compatible functor, its selected comparison with [n] is itself compatible with these signed packages; that reusable theorem is what transported DG consumers use.

noncomputable def CategoryTheory.Pretriangulated.signedShiftFunctorCommIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (n a : ℤ) : (shiftFunctor C a).comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp (shiftFunctor C a)

The Koszul-signed comparison between shifting by a and then by n, and shifting by n and then by a.

Equations

• CategoryTheory.Pretriangulated.signedShiftFunctorCommIso C n a = (n * a).negOnePow • CategoryTheory.shiftFunctorComm C a n

@[implicit_reducible]

noncomputable def CategoryTheory.Pretriangulated.shiftFunctorUnsignedCommShift (C : Type u) [Category.{v, u} C] [HasShift C ℤ] (n : ℤ) : (shiftFunctor C n).CommShift ℤ

The unsigned CommShift structure on an integral shift functor.

For odd n this is not the structure that makes the shift functor triangulated. It is retained as explicit data for sign-free and object-only arguments.

Equations

• CategoryTheory.Pretriangulated.shiftFunctorUnsignedCommShift C n = { commShiftIso := fun (a : ℤ) => CategoryTheory.shiftFunctorComm C a n, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

@[implicit_reducible]

noncomputable def CategoryTheory.Pretriangulated.shiftFunctorCommShift (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (n : ℤ) : (shiftFunctor C n).CommShift ℤ

The sign-correct CommShift structure on an integral shift functor.

Equations

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

@[simp]

theorem CategoryTheory.Pretriangulated.shiftFunctorCommShift_commShiftIso_hom_app (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (n a : ℤ) (X : C) : (Functor.commShiftIso (shiftFunctor C n) a).hom.app X = (n * a).negOnePow • (shiftFunctorComm C a n).hom.app X

theorem CategoryTheory.Pretriangulated.commShiftIso_commShift (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] (F : Functor C D) [F.Additive] [F.CommShift ℤ] (n : ℤ) : NatTrans.CommShift (Functor.commShiftIso F n).hom ℤ

The selected comparison of an additive functor with the shift by n is itself compatible with all integral shifts when the two shift functors carry the sign-correct CommShift structures.

The additivity hypothesis is essential: moving the Koszul sign through F.map is part of the compatibility equation.

noncomputable def CategoryTheory.Pretriangulated.shiftSignIso (C : Type u) [Category.{v, u} C] [Preadditive C] (n : ℤ) (X : C) : X ≅ X

The parity-sign automorphism used at the middle vertex of a shifted triangle.

Equations

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

noncomputable def CategoryTheory.Pretriangulated.shiftFunctorMapTriangleIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (n : ℤ) : (shiftFunctor C n).mapTriangle ≅ Triangle.shiftFunctor C n

Mapping a triangle by [n] with the sign-correct CommShift agrees with the canonical shift of that triangle.

Equations

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

theorem CategoryTheory.Pretriangulated.shiftFunctorIsTriangulated (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Limits.HasZeroObject C] [Pretriangulated C] (n : ℤ) : (shiftFunctor C n).IsTriangulated

Every integral shift is triangulated when equipped with the sign-correct CommShift structure.

noncomputable def CategoryTheory.Pretriangulated.shiftFunctorUnsignedMapTriangleIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (n : ℤ) (hn : Even n) : (shiftFunctor C n).mapTriangle ≅ Triangle.shiftFunctor C n

For an even n, the unsigned comparison also identifies triangle mapping by [n] with the canonical triangle shift.

Equations

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

theorem CategoryTheory.Pretriangulated.shiftFunctorUnsignedIsTriangulated (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Limits.HasZeroObject C] [Pretriangulated C] (n : ℤ) (hn : Even n) : (shiftFunctor C n).IsTriangulated

An even integral shift is triangulated with the unsigned CommShift presentation. This is a compatibility interface; the signed presentation works uniformly for every integer.