The shift on the category of triangles

In this file, it is shown that if C is a preadditive category with a shift by ℤ, then the category of triangles Triangle C is also endowed with a shift. We also show that rotating triangles three times identifies with the shift by 1.

The shift on the category of triangles was also obtained by Adam Topaz, Johan Commelin and Andrew Yang during the Liquid Tensor Experiment.

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

The shift functor Triangle C ⥤ Triangle C by n : ℤ sends a triangle to the triangle obtained by shifting the objects by n in C and by multiplying the three morphisms by (-1)^n.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (n : ℤ) (T : Triangle C) : (shiftFunctor C n).obj T = mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₁) (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₂) (n.negOnePow • CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map T.mor₃) ((shiftFunctorComm C 1 n).hom.app T.obj₁))

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (n : ℤ) {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) : ((shiftFunctor C n).map f).hom₃ = (CategoryTheory.shiftFunctor C n).map f.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (n : ℤ) {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) : ((shiftFunctor C n).map f).hom₁ = (CategoryTheory.shiftFunctor C n).map f.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (n : ℤ) {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) : ((shiftFunctor C n).map f).hom₂ = (CategoryTheory.shiftFunctor C n).map f.hom₂

noncomputable def CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] : shiftFunctor C 0 ≅ Functor.id (Triangle C)

The canonical isomorphism Triangle.shiftFunctor C 0 ≅ 𝟭 (Triangle C).

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (X : Triangle C) : ((shiftFunctorZero C).hom.app X).hom₁ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (X : Triangle C) : ((shiftFunctorZero C).inv.app X).hom₃ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (X : Triangle C) : ((shiftFunctorZero C).hom.app X).hom₃ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (X : Triangle C) : ((shiftFunctorZero C).inv.app X).hom₁ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (X : Triangle C) : ((shiftFunctorZero C).hom.app X).hom₂ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (X : Triangle C) : ((shiftFunctorZero C).inv.app X).hom₂ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₂

noncomputable def CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) : shiftFunctor C n ≅ (shiftFunctor C a).comp (shiftFunctor C b)

The canonical isomorphism Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b when a + b = n.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) (X : Triangle C) : ((shiftFunctorAdd' C a b n h).hom.app X).hom₂ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) (X : Triangle C) : ((shiftFunctorAdd' C a b n h).inv.app X).hom₁ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) (X : Triangle C) : ((shiftFunctorAdd' C a b n h).hom.app X).hom₁ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) (X : Triangle C) : ((shiftFunctorAdd' C a b n h).inv.app X).hom₃ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) (X : Triangle C) : ((shiftFunctorAdd' C a b n h).inv.app X).hom₂ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ) (h : a + b = n) (X : Triangle C) : ((shiftFunctorAdd' C a b n h).hom.app X).hom₃ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₃

noncomputable def CategoryTheory.Pretriangulated.rotateRotateRotateIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] : (rotate C).comp ((rotate C).comp (rotate C)) ≅ Triangle.shiftFunctor C 1

Rotating triangles three times identifies with the shift by 1.

noncomputable def CategoryTheory.Pretriangulated.invRotateInvRotateInvRotateIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] : (invRotate C).comp ((invRotate C).comp (invRotate C)) ≅ Triangle.shiftFunctor C (-1)

Rotating triangles three times backwards identifies with the shift by -1.

noncomputable def CategoryTheory.Pretriangulated.invRotateIsoRotateRotateShiftFunctorNegOne (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] : invRotate C ≅ (rotate C).comp ((rotate C).comp (Triangle.shiftFunctor C (-1)))

The inverse of the rotation of triangles can be expressed using a double rotation and the shift by -1.

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

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_eq (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (n : ℤ) : CategoryTheory.shiftFunctor (Triangle C) n = shiftFunctor C n

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_eq (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : CategoryTheory.shiftFunctorZero (Triangle C) ℤ = shiftFunctorZero C

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd_eq (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b : ℤ) : shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_eq (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b c : ℤ) (h : a + b = c) : CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h = shiftFunctorAdd' C a b c h