Rotate #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file adds the ability to rotate triangles and triangle morphisms. It also shows that rotation gives an equivalence on the category of triangles.
@[simp]
theorem
category_theory.pretriangulated.triangle.rotate_mor₂
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.triangle.rotate_obj₂
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
def
category_theory.pretriangulated.triangle.rotate
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.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⟧
Equations
@[simp]
theorem
category_theory.pretriangulated.triangle.rotate_obj₃
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.triangle.rotate_mor₃
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.triangle.rotate_obj₁
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.triangle.rotate_mor₁
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.triangle.inv_rotate_obj₃
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
T.inv_rotate.obj₃ = T.obj₂
@[simp]
theorem
category_theory.pretriangulated.triangle.inv_rotate_obj₁
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
T.inv_rotate.obj₁ = (category_theory.shift_functor C (-1)).obj T.obj₃
noncomputable
def
category_theory.pretriangulated.triangle.inv_rotate
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.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.pretriangulated.triangle.mk (-(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)
@[simp]
theorem
category_theory.pretriangulated.triangle.inv_rotate_mor₃
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
T.inv_rotate.mor₃ = T.mor₂ ≫ (category_theory.shift_functor_comp_iso_id C (-1) 1 _).inv.app T.obj₃
@[simp]
theorem
category_theory.pretriangulated.triangle.inv_rotate_mor₁
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
T.inv_rotate.mor₁ = -(category_theory.shift_functor C (-1)).map T.mor₃ ≫ (category_theory.shift_functor_comp_iso_id C 1 (-1) _).hom.app T.obj₁
@[simp]
theorem
category_theory.pretriangulated.triangle.inv_rotate_mor₂
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
T.inv_rotate.mor₂ = T.mor₁
@[simp]
theorem
category_theory.pretriangulated.triangle.inv_rotate_obj₂
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
T.inv_rotate.obj₂ = T.obj₁
@[simp]
theorem
category_theory.pretriangulated.rotate_map_hom₂
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T₁ T₂ : category_theory.pretriangulated.triangle C)
(f : T₁ ⟶ T₂) :
((category_theory.pretriangulated.rotate C).map f).hom₂ = f.hom₃
@[simp]
theorem
category_theory.pretriangulated.rotate_map_hom₁
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T₁ T₂ : category_theory.pretriangulated.triangle C)
(f : T₁ ⟶ T₂) :
((category_theory.pretriangulated.rotate C).map f).hom₁ = f.hom₂
@[simp]
theorem
category_theory.pretriangulated.rotate_map_hom₃
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T₁ T₂ : category_theory.pretriangulated.triangle C)
(f : T₁ ⟶ T₂) :
((category_theory.pretriangulated.rotate C).map f).hom₃ = (category_theory.shift_functor C 1).map f.hom₁
@[simp]
theorem
category_theory.pretriangulated.rotate_obj
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
def
category_theory.pretriangulated.rotate
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ] :
Rotating triangles gives an endofunctor on the category of triangles in C.
Equations
- category_theory.pretriangulated.rotate C = {obj := category_theory.pretriangulated.triangle.rotate _inst_3, map := λ (T₁ T₂ : category_theory.pretriangulated.triangle C) (f : T₁ ⟶ T₂), {hom₁ := f.hom₂, hom₂ := f.hom₃, hom₃ := (category_theory.shift_functor C 1).map f.hom₁, comm₁' := _, comm₂' := _, comm₃' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.pretriangulated.rotate
@[simp]
theorem
category_theory.pretriangulated.inv_rotate_map_hom₁
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T₁ T₂ : category_theory.pretriangulated.triangle C)
(f : T₁ ⟶ T₂) :
((category_theory.pretriangulated.inv_rotate C).map f).hom₁ = (category_theory.shift_functor C (-1)).map f.hom₃
@[simp]
theorem
category_theory.pretriangulated.inv_rotate_map_hom₃
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T₁ T₂ : category_theory.pretriangulated.triangle C)
(f : T₁ ⟶ T₂) :
((category_theory.pretriangulated.inv_rotate C).map f).hom₃ = f.hom₂
@[simp]
theorem
category_theory.pretriangulated.inv_rotate_obj
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rotate_map_hom₂
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
(T₁ T₂ : category_theory.pretriangulated.triangle C)
(f : T₁ ⟶ T₂) :
((category_theory.pretriangulated.inv_rotate C).map f).hom₂ = f.hom₁
noncomputable
def
category_theory.pretriangulated.inv_rotate
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ] :
The inverse rotation of triangles gives an endofunctor on the category of triangles in C.
Equations
- category_theory.pretriangulated.inv_rotate C = {obj := category_theory.pretriangulated.triangle.inv_rotate _inst_3, map := λ (T₁ T₂ : category_theory.pretriangulated.triangle C) (f : T₁ ⟶ T₂), {hom₁ := (category_theory.shift_functor C (-1)).map f.hom₃, hom₂ := f.hom₁, hom₃ := f.hom₂, comm₁' := _, comm₂' := _, comm₃' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.pretriangulated.inv_rotate
@[simp]
theorem
category_theory.pretriangulated.rot_comp_inv_rot_hom_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.rot_comp_inv_rot_inv_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.rot_comp_inv_rot_hom_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.rot_comp_inv_rot_hom_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.rot_comp_inv_rot_inv_app_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]
(X : category_theory.pretriangulated.triangle C) :
noncomputable
def
category_theory.pretriangulated.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] :
The unit isomorphism of the auto-equivalence of categories triangle_rotation C of
triangle C given by the rotation of triangles.
Equations
- category_theory.pretriangulated.rot_comp_inv_rot = category_theory.nat_iso.of_components (λ (T : category_theory.pretriangulated.triangle C), ((𝟭 (category_theory.pretriangulated.triangle C)).obj T).iso_mk ((category_theory.pretriangulated.rotate C ⋙ category_theory.pretriangulated.inv_rotate C).obj T) ((category_theory.shift_equiv C 1).unit_iso.app T.obj₁) (category_theory.iso.refl ((𝟭 (category_theory.pretriangulated.triangle C)).obj T).obj₂) (category_theory.iso.refl ((𝟭 (category_theory.pretriangulated.triangle C)).obj T).obj₃) _ _ _) category_theory.pretriangulated.rot_comp_inv_rot._proof_4
@[simp]
theorem
category_theory.pretriangulated.rot_comp_inv_rot_inv_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rot_comp_rot_inv_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rot_comp_rot_hom_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rot_comp_rot_inv_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rot_comp_rot_inv_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rot_comp_rot_hom_app_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]
(X : category_theory.pretriangulated.triangle C) :
@[simp]
theorem
category_theory.pretriangulated.inv_rot_comp_rot_hom_app_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]
(X : category_theory.pretriangulated.triangle C) :
noncomputable
def
category_theory.pretriangulated.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] :
The counit isomorphism of the auto-equivalence of categories triangle_rotation C of
triangle C given by the rotation of triangles.
Equations
- category_theory.pretriangulated.inv_rot_comp_rot = category_theory.nat_iso.of_components (λ (T : category_theory.pretriangulated.triangle C), ((category_theory.pretriangulated.inv_rotate C ⋙ category_theory.pretriangulated.rotate C).obj T).iso_mk ((𝟭 (category_theory.pretriangulated.triangle C)).obj T) (category_theory.iso.refl ((category_theory.pretriangulated.inv_rotate C ⋙ category_theory.pretriangulated.rotate C).obj T).obj₁) (category_theory.iso.refl ((category_theory.pretriangulated.inv_rotate C ⋙ category_theory.pretriangulated.rotate C).obj T).obj₂) ((category_theory.shift_equiv C 1).counit_iso.app T.obj₃) _ _ _) category_theory.pretriangulated.inv_rot_comp_rot._proof_4
@[simp]
theorem
category_theory.pretriangulated.triangle_rotation_inverse
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :
@[simp]
theorem
category_theory.pretriangulated.triangle_rotation_unit_iso
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :
noncomputable
def
category_theory.pretriangulated.triangle_rotation
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :
Rotating triangles gives an auto-equivalence on the category of triangles in C.
Equations
- category_theory.pretriangulated.triangle_rotation C = {functor := category_theory.pretriangulated.rotate C _inst_3, inverse := category_theory.pretriangulated.inv_rotate C _inst_3, unit_iso := category_theory.pretriangulated.rot_comp_inv_rot _, counit_iso := category_theory.pretriangulated.inv_rot_comp_rot _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.pretriangulated.triangle_rotation_functor
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :
@[simp]
theorem
category_theory.pretriangulated.triangle_rotation_counit_iso
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :
@[protected, instance]
noncomputable
def
category_theory.pretriangulated.rotate.category_theory.is_equivalence
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :
@[protected, instance]
noncomputable
def
category_theory.pretriangulated.inv_rotate.category_theory.is_equivalence
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.has_shift C ℤ]
[∀ (n : ℤ), (category_theory.shift_functor C n).additive] :