category_theory.triangulated.rotate

@[simp]

theorem category_theory.triangulated.triangle.rotate_mor₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

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

source

def category_theory.triangulated.triangle.rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

category_theory.triangulated.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 = category_theory.triangulated.triangle.mk C T.mor₂ T.mor₃ (-(category_theory.shift_functor C 1).map T.mor₁)

source

@[simp]

theorem category_theory.triangulated.triangle.rotate_obj₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.rotate.obj₃ = (category_theory.shift_functor C 1).obj T.obj₁

source

@[simp]

theorem category_theory.triangulated.triangle.rotate_mor₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.rotate.mor₁ = T.mor₂

source

@[simp]

theorem category_theory.triangulated.triangle.rotate_mor₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.rotate.mor₂ = T.mor₃

source

@[simp]

theorem category_theory.triangulated.triangle.rotate_obj₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.rotate.obj₂ = T.obj₃

source

@[simp]

theorem category_theory.triangulated.triangle.rotate_obj₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.rotate.obj₁ = T.obj₂

source

@[simp]

theorem category_theory.triangulated.triangle.inv_rotate_mor₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.inv_rotate.mor₁ = -(category_theory.shift_functor C (-1)).map T.mor₃ ≫ (category_theory.shift_shift_neg T.obj₁ 1).hom

source

@[simp]

theorem category_theory.triangulated.triangle.inv_rotate_obj₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.inv_rotate.obj₂ = T.obj₁

source

@[simp]

theorem category_theory.triangulated.triangle.inv_rotate_mor₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.inv_rotate.mor₂ = T.mor₁

source

@[simp]

theorem category_theory.triangulated.triangle.inv_rotate_mor₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.inv_rotate.mor₃ = T.mor₂ ≫ (category_theory.shift_neg_shift T.obj₃ 1).inv

source

@[simp]

theorem category_theory.triangulated.triangle.inv_rotate_obj₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.inv_rotate.obj₃ = T.obj₂

source

@[simp]

theorem category_theory.triangulated.triangle.inv_rotate_obj₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

T.inv_rotate.obj₁ = (category_theory.shift_functor C (-1)).obj T.obj₃

source

noncomputable def category_theory.triangulated.triangle.inv_rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

category_theory.triangulated.triangle C

Given a triangle of the form:

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

applying inv_rotate 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 counit_iso of shift C)

Equations

T.inv_rotate = category_theory.triangulated.triangle.mk C (-(category_theory.shift_functor C (-1)).map T.mor₃ ≫ (category_theory.shift_shift_neg T.obj₁ 1).hom) T.mor₁ (T.mor₂ ≫ (category_theory.shift_neg_shift T.obj₃ 1).inv)

source

def category_theory.triangulated.triangle_morphism.rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

category_theory.triangulated.triangle_morphism T₁.rotate T₂.rotate

You can also rotate a triangle morphism to get a morphism between the two rotated triangles. Given a triangle morphism of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
  │       │       │        │
  │a      │b      │c       │a⟦1⟧
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'⟦1⟧
      f'      g'      h'

applying rotate gives a triangle morphism of the form:

      g        h       -f⟦1⟧
  Y  ───> Z  ───>  X⟦1⟧ ───> Y⟦1⟧
  │       │         │         │
  │b      │c        │a⟦1⟧     │b⟦1⟧'
  V       V         V         V
  Y' ───> Z' ───> X'⟦1⟧ ───> Y'⟦1⟧
      g'      h'       -f'⟦1⟧

Equations

f.rotate = {hom₁ := f.hom₂, hom₂ := f.hom₃, hom₃ := (category_theory.shift_functor C 1).map f.hom₁, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[simp]

theorem category_theory.triangulated.triangle_morphism.rotate_hom₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

f.rotate.hom₂ = f.hom₃

source

@[simp]

theorem category_theory.triangulated.triangle_morphism.rotate_hom₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

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

source

@[simp]

theorem category_theory.triangulated.triangle_morphism.rotate_hom₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

f.rotate.hom₁ = f.hom₂

source

@[simp]

theorem category_theory.triangulated.triangle_morphism.inv_rotate_hom₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

f.inv_rotate.hom₂ = f.hom₁

source

@[simp]

theorem category_theory.triangulated.triangle_morphism.inv_rotate_hom₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

f.inv_rotate.hom₁ = (category_theory.shift_functor C (-1)).map f.hom₃

source

@[simp]

theorem category_theory.triangulated.triangle_morphism.inv_rotate_hom₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

f.inv_rotate.hom₃ = f.hom₂

source

def category_theory.triangulated.triangle_morphism.inv_rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.triangulated.triangle C} (f : category_theory.triangulated.triangle_morphism T₁ T₂) :

category_theory.triangulated.triangle_morphism T₁.inv_rotate T₂.inv_rotate

Given a triangle morphism of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
  │       │       │        │
  │a      │b      │c       │a⟦1⟧
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'⟦1⟧
      f'      g'      h'

applying inv_rotate gives a triangle morphism that can be thought of as:

        -h⟦-1⟧      f         g
  Z⟦-1⟧  ───>  X   ───>  Y   ───>  Z
    │          │         │         │
    │c⟦-1⟧'    │a        │b        │c
    V          V         V         V
  Z'⟦-1⟧ ───>  X'  ───>  Y'  ───>  Z'
       -h'⟦-1⟧     f'        g'

(note that this diagram doesn't technically fit the definition of triangle morphism, as Z⟦-1⟧⟦1⟧ is not necessarily equal to Z, and Z'⟦-1⟧⟦1⟧ is not necessarily equal to Z', but they are isomorphic, by the counit_iso of shift C)

Equations

f.inv_rotate = {hom₁ := (category_theory.shift_functor C (-1)).map f.hom₃, hom₂ := f.hom₁, hom₃ := f.hom₂, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[simp]

theorem category_theory.triangulated.rotate_obj (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.rotate C).obj T = T.rotate

source

@[simp]

theorem category_theory.triangulated.rotate_map (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (_x _x_1 : category_theory.triangulated.triangle C) (f : _x ⟶ _x_1) :

(category_theory.triangulated.rotate C).map f = category_theory.triangulated.triangle_morphism.rotate f

source

def category_theory.triangulated.rotate (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] :

category_theory.triangulated.triangle C ⥤ category_theory.triangulated.triangle C

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

Equations

category_theory.triangulated.rotate C = {obj := category_theory.triangulated.triangle.rotate _inst_3, map := λ (_x _x_1 : category_theory.triangulated.triangle C) (f : _x ⟶ _x_1), category_theory.triangulated.triangle_morphism.rotate f, map_id' := _, map_comp' := _}

Instances for category_theory.triangulated.rotate

category_theory.triangulated.rotate.category_theory.is_equivalence

source

@[simp]

theorem category_theory.triangulated.inv_rotate_obj (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.inv_rotate C).obj T = T.inv_rotate

source

noncomputable def category_theory.triangulated.inv_rotate (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] :

category_theory.triangulated.triangle C ⥤ category_theory.triangulated.triangle C

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

Equations

category_theory.triangulated.inv_rotate C = {obj := category_theory.triangulated.triangle.inv_rotate _inst_3, map := λ (_x _x_1 : category_theory.triangulated.triangle C) (f : _x ⟶ _x_1), category_theory.triangulated.triangle_morphism.inv_rotate f, map_id' := _, map_comp' := _}

Instances for category_theory.triangulated.inv_rotate

category_theory.triangulated.inv_rotate.category_theory.is_equivalence

source

@[simp]

theorem category_theory.triangulated.inv_rotate_map (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] (_x _x_1 : category_theory.triangulated.triangle C) (f : _x ⟶ _x_1) :

(category_theory.triangulated.inv_rotate C).map f = category_theory.triangulated.triangle_morphism.inv_rotate f

source

noncomputable def category_theory.triangulated.to_inv_rotate_rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

T ⟶ (category_theory.triangulated.inv_rotate C).obj ((category_theory.triangulated.rotate C).obj T)

There is a natural map from a triangle to the inv_rotate of its rotate.

Equations

category_theory.triangulated.to_inv_rotate_rotate T = {hom₁ := (category_theory.shift_shift_neg T.obj₁ 1).inv, hom₂ := 𝟙 T.obj₂, hom₃ := 𝟙 T.obj₃, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[simp]

theorem category_theory.triangulated.to_inv_rotate_rotate_hom₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.to_inv_rotate_rotate T).hom₂ = 𝟙 T.obj₂

source

@[simp]

theorem category_theory.triangulated.to_inv_rotate_rotate_hom₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.to_inv_rotate_rotate T).hom₃ = 𝟙 T.obj₃

source

@[simp]

theorem category_theory.triangulated.to_inv_rotate_rotate_hom₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.to_inv_rotate_rotate T).hom₁ = (category_theory.shift_shift_neg T.obj₁ 1).inv

source

@[simp]

theorem category_theory.triangulated.rot_comp_inv_rot_hom_app {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

category_theory.triangulated.rot_comp_inv_rot_hom.app T = category_theory.triangulated.to_inv_rotate_rotate T

source

noncomputable def category_theory.triangulated.rot_comp_inv_rot_hom {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

𝟭 (category_theory.triangulated.triangle C) ⟶ category_theory.triangulated.rotate C ⋙ category_theory.triangulated.inv_rotate C

There is a natural transformation between the identity functor on triangles in C, and the composition of a rotation with an inverse rotation.

Equations

category_theory.triangulated.rot_comp_inv_rot_hom = {app := category_theory.triangulated.to_inv_rotate_rotate category_theory.triangulated.rot_comp_inv_rot_hom._proof_1, naturality' := _}

source

noncomputable def category_theory.triangulated.from_inv_rotate_rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.inv_rotate C).obj ((category_theory.triangulated.rotate C).obj T) ⟶ T

There is a natural map from the inv_rotate of the rotate of a triangle to itself.

Equations

category_theory.triangulated.from_inv_rotate_rotate T = {hom₁ := (category_theory.shift_equiv C 1).unit_inv.app T.obj₁, hom₂ := 𝟙 T.obj₂, hom₃ := 𝟙 T.obj₃, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[simp]

theorem category_theory.triangulated.from_inv_rotate_rotate_hom₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.from_inv_rotate_rotate T).hom₁ = (category_theory.shift_equiv C 1).unit_inv.app T.obj₁

source

@[simp]

theorem category_theory.triangulated.from_inv_rotate_rotate_hom₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.from_inv_rotate_rotate T).hom₂ = 𝟙 T.obj₂

source

@[simp]

theorem category_theory.triangulated.from_inv_rotate_rotate_hom₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.from_inv_rotate_rotate T).hom₃ = 𝟙 T.obj₃

source

@[simp]

theorem category_theory.triangulated.rot_comp_inv_rot_inv_app {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

category_theory.triangulated.rot_comp_inv_rot_inv.app T = category_theory.triangulated.from_inv_rotate_rotate T

source

noncomputable def category_theory.triangulated.rot_comp_inv_rot_inv {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

category_theory.triangulated.rotate C ⋙ category_theory.triangulated.inv_rotate C ⟶ 𝟭 (category_theory.triangulated.triangle C)

There is a natural transformation between the composition of a rotation with an inverse rotation on triangles in C, and the identity functor.

Equations

category_theory.triangulated.rot_comp_inv_rot_inv = {app := category_theory.triangulated.from_inv_rotate_rotate category_theory.triangulated.rot_comp_inv_rot_inv._proof_1, naturality' := _}

source

@[simp]

theorem category_theory.triangulated.rot_comp_inv_rot_hom_2 {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

category_theory.triangulated.rot_comp_inv_rot.hom = category_theory.triangulated.rot_comp_inv_rot_hom

source

@[simp]

theorem category_theory.triangulated.rot_comp_inv_rot_inv_2 {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

category_theory.triangulated.rot_comp_inv_rot.inv = category_theory.triangulated.rot_comp_inv_rot_inv

source

noncomputable def category_theory.triangulated.rot_comp_inv_rot {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

𝟭 (category_theory.triangulated.triangle C) ≅ category_theory.triangulated.rotate C ⋙ category_theory.triangulated.inv_rotate C

The natural transformations between the identity functor on triangles in C and the composition of a rotation with an inverse rotation are natural isomorphisms (they are isomorphisms in the category of functors).

Equations

category_theory.triangulated.rot_comp_inv_rot = {hom := category_theory.triangulated.rot_comp_inv_rot_hom category_theory.triangulated.rot_comp_inv_rot._proof_1, inv := category_theory.triangulated.rot_comp_inv_rot_inv category_theory.triangulated.rot_comp_inv_rot._proof_2, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.triangulated.from_rotate_inv_rotate_hom₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.from_rotate_inv_rotate T).hom₂ = 𝟙 T.obj₂

source

@[simp]

theorem category_theory.triangulated.from_rotate_inv_rotate_hom₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.from_rotate_inv_rotate T).hom₃ = (category_theory.shift_equiv C 1).counit.app T.obj₃

source

@[simp]

theorem category_theory.triangulated.from_rotate_inv_rotate_hom₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.from_rotate_inv_rotate T).hom₁ = 𝟙 T.obj₁

source

noncomputable def category_theory.triangulated.from_rotate_inv_rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.rotate C).obj ((category_theory.triangulated.inv_rotate C).obj T) ⟶ T

There is a natural map from the rotate of the inv_rotate of a triangle to itself.

Equations

category_theory.triangulated.from_rotate_inv_rotate T = {hom₁ := 𝟙 T.obj₁, hom₂ := 𝟙 T.obj₂, hom₃ := (category_theory.shift_equiv C 1).counit.app T.obj₃, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[simp]

theorem category_theory.triangulated.inv_rot_comp_rot_hom_app {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

category_theory.triangulated.inv_rot_comp_rot_hom.app T = category_theory.triangulated.from_rotate_inv_rotate T

source

noncomputable def category_theory.triangulated.inv_rot_comp_rot_hom {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

category_theory.triangulated.inv_rotate C ⋙ category_theory.triangulated.rotate C ⟶ 𝟭 (category_theory.triangulated.triangle C)

There is a natural transformation between the composition of an inverse rotation with a rotation on triangles in C, and the identity functor.

Equations

category_theory.triangulated.inv_rot_comp_rot_hom = {app := category_theory.triangulated.from_rotate_inv_rotate category_theory.triangulated.inv_rot_comp_rot_hom._proof_1, naturality' := _}

source

@[simp]

theorem category_theory.triangulated.to_rotate_inv_rotate_hom₃ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.to_rotate_inv_rotate T).hom₃ = (category_theory.shift_equiv C 1).counit_inv.app T.obj₃

source

@[simp]

theorem category_theory.triangulated.to_rotate_inv_rotate_hom₁ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.to_rotate_inv_rotate T).hom₁ = 𝟙 T.obj₁

source

@[simp]

theorem category_theory.triangulated.to_rotate_inv_rotate_hom₂ {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

(category_theory.triangulated.to_rotate_inv_rotate T).hom₂ = 𝟙 T.obj₂

source

noncomputable def category_theory.triangulated.to_rotate_inv_rotate {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

T ⟶ (category_theory.triangulated.rotate C).obj ((category_theory.triangulated.inv_rotate C).obj T)

There is a natural map from a triangle to the rotate of its inv_rotate.

Equations

category_theory.triangulated.to_rotate_inv_rotate T = {hom₁ := 𝟙 T.obj₁, hom₂ := 𝟙 T.obj₂, hom₃ := (category_theory.shift_equiv C 1).counit_inv.app T.obj₃, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[simp]

theorem category_theory.triangulated.inv_rot_comp_rot_inv_app {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (T : category_theory.triangulated.triangle C) :

category_theory.triangulated.inv_rot_comp_rot_inv.app T = category_theory.triangulated.to_rotate_inv_rotate T

source

noncomputable def category_theory.triangulated.inv_rot_comp_rot_inv {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

𝟭 (category_theory.triangulated.triangle C) ⟶ category_theory.triangulated.inv_rotate C ⋙ category_theory.triangulated.rotate C

There is a natural transformation between the identity functor on triangles in C, and the composition of an inverse rotation with a rotation.

Equations

category_theory.triangulated.inv_rot_comp_rot_inv = {app := category_theory.triangulated.to_rotate_inv_rotate category_theory.triangulated.inv_rot_comp_rot_inv._proof_1, naturality' := _}

source

noncomputable def category_theory.triangulated.inv_rot_comp_rot {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.has_shift C ℤ] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

category_theory.triangulated.inv_rotate C ⋙ category_theory.triangulated.rotate C ≅ 𝟭 (category_theory.triangulated.triangle C)

The natural transformations between the composition of a rotation with an inverse rotation on triangles in C, and the identity functor on triangles are natural isomorphisms (they are isomorphisms in the category of functors).

Equations