Documentation

Mathlib.CategoryTheory.Triangulated.TriangleShift

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.

source
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) (T : CategoryTheory.Pretriangulated.Triangle C) :
(CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).toPrefunctor.obj T = CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).toPrefunctor.map T.mor₁) (n.negOnePow • (CategoryTheory.shiftFunctor C n).toPrefunctor.map T.mor₂) (n.negOnePow • CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).toPrefunctor.map T.mor₃) ((CategoryTheory.shiftFunctorComm C 1 n).hom.app T.obj₁))
source
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) :
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).toPrefunctor.map f).hom₂ = (CategoryTheory.shiftFunctor C n).toPrefunctor.map f.hom₂
source
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) :
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).toPrefunctor.map f).hom₁ = (CategoryTheory.shiftFunctor C n).toPrefunctor.map f.hom₁
source
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) :
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).toPrefunctor.map f).hom₃ = (CategoryTheory.shiftFunctor C n).toPrefunctor.map f.hom₃
source
noncomputable def CategoryTheory.Pretriangulated.Triangle.shiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) :
CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₂ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₂
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₃ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₃
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₁ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₁
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₁ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₁
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₃ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₃
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₂ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₂
    source
    noncomputable def CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :
    CategoryTheory.Pretriangulated.Triangle.shiftFunctor C 0 ≅ CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₂ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₂
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₃ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₃
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₂ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₂
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₁ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₁
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₁ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₁
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₃ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₃
      source
      noncomputable def CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (n : ℤ) (h : a + b = n) :
      CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n ≅ CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C a) (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C b)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def CategoryTheory.Pretriangulated.rotateRotateRotateIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :
        CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.rotate C) (CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.rotate C) (CategoryTheory.Pretriangulated.rotate C)) ≅ CategoryTheory.Pretriangulated.Triangle.shiftFunctor C 1

        Rotating triangles three times identifies with the shift by 1.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def CategoryTheory.Pretriangulated.invRotateInvRotateInvRotateIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :
          CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.invRotate C) (CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.invRotate C) (CategoryTheory.Pretriangulated.invRotate C)) ≅ CategoryTheory.Pretriangulated.Triangle.shiftFunctor C (-1)

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def CategoryTheory.Pretriangulated.invRotateIsoRotateRotateShiftFunctorNegOne (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] :
            CategoryTheory.Pretriangulated.invRotate C ≅ CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.rotate C) (CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.rotate C) (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C (-1)))

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable instance CategoryTheory.Pretriangulated.Triangle.instHasShiftTriangleIntTriangleCategoryInstAddMonoidInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] :
              CategoryTheory.HasShift (CategoryTheory.Pretriangulated.Triangle C) ℤ
              Equations
              • One or more equations did not get rendered due to their size.
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctor_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (n : ℤ) :
              CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n = CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] :
              CategoryTheory.shiftFunctorZero (CategoryTheory.Pretriangulated.Triangle C) ℤ = CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) :
              CategoryTheory.shiftFunctorAdd (CategoryTheory.Pretriangulated.Triangle C) a b = CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b (a + b) (_ : a + b = a + b)
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] (a : ℤ) (b : ℤ) (c : ℤ) (h : a + b = c) :
              CategoryTheory.shiftFunctorAdd' (CategoryTheory.Pretriangulated.Triangle C) a b c h = CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b c h