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

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

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⟧

Equations

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

Instances For

source

@[simp]

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

T.rotate.mor₁ = T.mor₂

source

@[simp]

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

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

source

@[simp]

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

T.rotate.obj₂ = T.obj₃

source

@[simp]

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

T.rotate.obj₁ = T.obj₂

source

@[simp]

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

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

source

@[simp]

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

T.rotate.mor₂ = T.mor₃

source

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

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)

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

T.invRotate.mor₃ = CategoryStruct.comp T.mor₂ ((shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3)

source

@[simp]

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

T.invRotate.obj₂ = T.obj₁

source

@[simp]

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

T.invRotate.obj₃ = T.obj₂

source

@[simp]

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

T.invRotate.mor₂ = T.mor₁

source

@[simp]

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

T.invRotate.mor₁ = -CategoryStruct.comp ((shiftFunctor C (-1)).map T.mor₃) ((shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁)

source

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

Functor (Triangle C) (Triangle C)

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

Equations

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

Instances For

source

@[simp]

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

(rotate C).obj T = T.rotate

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_map_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :

((rotate C).map f).hom₃ = (shiftFunctor C 1).map f.hom₁

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_map_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :

((rotate C).map f).hom₁ = f.hom₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.rotate_map_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :

((rotate C).map f).hom₂ = f.hom₃

source

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

Functor (Triangle C) (Triangle C)

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

Equations

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

Instances For

source

@[simp]

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

(invRotate C).obj T = T.invRotate

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_map_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :

((invRotate C).map f).hom₁ = (shiftFunctor C (-1)).map f.hom₃

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_map_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :

((invRotate C).map f).hom₃ = f.hom₂

source

@[simp]

theorem CategoryTheory.Pretriangulated.invRotate_map_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :

((invRotate C).map f).hom₂ = f.hom₁

source

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

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

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(rotCompInvRot.inv.app X).hom₁ = (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X.obj₁

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(rotCompInvRot.hom.app X).hom₁ = (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X.obj₁

source

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

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

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(invRotCompRot.hom.app X).hom₃ = (shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app X.obj₃

source

@[simp]

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

(invRotCompRot.inv.app X).hom₃ = (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app X.obj₃

source

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

Triangle C ≌ Triangle C

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

Equations

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

Instances For

source

@[simp]

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

(triangleRotation C).inverse = invRotate C

source

@[simp]

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

(triangleRotation C).functor = rotate C

source

@[simp]

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

(triangleRotation C).counitIso = invRotCompRot

source

@[simp]

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

(triangleRotation C).unitIso = rotCompInvRot

source

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

(rotate C).IsEquivalence

source

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

(invRotate C).IsEquivalence

Documentation

Mathlib.CategoryTheory.Triangulated.Rotate

Rotate #