Rotate #

This file adds the ability to rotate triangles and triangle morphisms. It also shows that rotation gives an equivalence on the category of triangles.

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.rotate_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.rotate T).mor₂ = T.mor₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.rotate_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.rotate T).mor₁ = T.mor₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.rotate_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.rotate T).obj₃ = (CategoryTheory.shiftFunctor C 1).obj T.obj₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.rotate_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.rotate T).obj₂ = T.obj₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.rotate_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.rotate T).mor₃ = -(CategoryTheory.shiftFunctor C 1).map T.mor₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.rotate_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.rotate T).obj₁ = T.obj₂

source

def CategoryTheory.Pretriangulated.Triangle.rotate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

CategoryTheory.Pretriangulated.Triangle C

If you rotate a triangle, you get another triangle. Given a triangle of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

applying rotate gives a triangle of the form:

      g       h        -f⟦1⟧'
  Y  ───> Z  ───>  X⟦1⟧ ───> Y⟦1⟧

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.invRotate_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.invRotate T).mor₃ = CategoryTheory.CategoryStruct.comp T.mor₂ ((CategoryTheory.shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv.app T.3)

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.invRotate_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.invRotate T).obj₂ = T.obj₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.invRotate_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.invRotate T).mor₁ = -CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (-1)).map T.mor₃) ((CategoryTheory.shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom.app T.obj₁)

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.invRotate_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.invRotate T).obj₃ = T.obj₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.invRotate_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.invRotate T).mor₂ = T.mor₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.invRotate_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.Triangle.invRotate T).obj₁ = (CategoryTheory.shiftFunctor C (-1)).obj T.obj₃

source

def CategoryTheory.Pretriangulated.Triangle.invRotate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

CategoryTheory.Pretriangulated.Triangle C

Given a triangle of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

applying invRotate gives a triangle that can be thought of as:

        -h⟦-1⟧'     f       g
  Z⟦-1⟧  ───>  X  ───> Y  ───> Z

(note that this diagram doesn't technically fit the definition of triangle, as Z⟦-1⟧⟦1⟧ is not necessarily equal to Z, but it is isomorphic, by the counitIso of shiftEquiv C 1)

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_map_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.rotate C).map f).hom₁ = f.hom₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotate C).obj T = CategoryTheory.Pretriangulated.Triangle.rotate T

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_map_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.rotate C).map f).hom₃ = (CategoryTheory.shiftFunctor C 1).map f.hom₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_map_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.rotate C).map f).hom₂ = f.hom₃

source

def CategoryTheory.Pretriangulated.rotate (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)

Rotating triangles gives an endofunctor on the category of triangles in C.

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_map_hom₃ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₃ = f.hom₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_map_hom₂ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₂ = f.hom₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotate C).obj T = CategoryTheory.Pretriangulated.Triangle.invRotate T

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_map_hom₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₁ = (CategoryTheory.shiftFunctor C (-1)).map f.hom₃

source

def CategoryTheory.Pretriangulated.invRotate (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] :

CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)

The inverse rotation of triangles gives an endofunctor on the category of triangles in C.

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotCompInvRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotCompInvRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotCompInvRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).inv.app X.obj₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotCompInvRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotCompInvRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotCompInvRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom.app X.obj₁

source

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

CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C) ≅ CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.rotate C) (CategoryTheory.Pretriangulated.invRotate C)

The unit isomorphism of the auto-equivalence of categories triangleRotation C of Triangle C given by the rotation of triangles.

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotCompRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotCompRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).hom.app X.obj₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotCompRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotCompRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotCompRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv.app X.obj₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotCompRot_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)] (X : CategoryTheory.Pretriangulated.Triangle C) :

(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂

source

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

CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.invRotate C) (CategoryTheory.Pretriangulated.rotate C) ≅ CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)

The counit isomorphism of the auto-equivalence of categories triangleRotation C of Triangle C given by the rotation of triangles.

Instances For

source

@[simp]

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

(CategoryTheory.Pretriangulated.triangleRotation C).unitIso = CategoryTheory.Pretriangulated.rotCompInvRot

source

@[simp]

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

(CategoryTheory.Pretriangulated.triangleRotation C).inverse = CategoryTheory.Pretriangulated.invRotate C

source

@[simp]

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

(CategoryTheory.Pretriangulated.triangleRotation C).counitIso = CategoryTheory.Pretriangulated.invRotCompRot

source

@[simp]

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

(CategoryTheory.Pretriangulated.triangleRotation C).functor = CategoryTheory.Pretriangulated.rotate C

source

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

CategoryTheory.Pretriangulated.Triangle C ≌ CategoryTheory.Pretriangulated.Triangle C

Rotating triangles gives an auto-equivalence on the category of triangles in C.

Instances For

source

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

CategoryTheory.IsEquivalence (CategoryTheory.Pretriangulated.rotate C)

source

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

CategoryTheory.IsEquivalence (CategoryTheory.Pretriangulated.invRotate C)