Rotation of triangles in a Frobenius stable category

The cone sequence of a morphism f : X ⟶ Y is the conflation

Y ⟶ cone(f) ⟶ ΣX.

Its connecting morphism is the negative of the suspension of f. Consequently the rotation of the stable cone triangle of f is isomorphic to the stable conflation triangle of this cone sequence. Since every distinguished stable triangle is isomorphic to a conflation triangle and every such triangle is isomorphic to a cone triangle, distinguished stable triangles are closed under forward rotation.

Conversely, a triangle whose rotation is distinguished is itself distinguished. For a conflation X ⟶ Y ⟶ Z, pull the chosen loop conflation ΩZ ⟶ P(Z) ⟶ Z back along Y ⟶ Z. This gives a conflation ΩZ ⟶ W ⟶ Y whose middle term W is stably isomorphic to X, because P(Z) is projective. The rotation of its standard triangle is isomorphic to the standard triangle of X ⟶ Y ⟶ Z, through the stable isomorphism Z ≅ ΣΩZ given by the connecting map of the loop conflation. Since rotation is an autoequivalence of the category of triangles, the backward direction follows.

This is the rotation construction in Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_coneSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) {X Y : C} (f : X ⟶ Y) : E.projectiveStableFunctor.map (hE.connectingMap ⋯) = -E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)

The connecting morphism of the cone sequence is the negative of the map induced by f on the chosen suspension objects, after passing to the stable category.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConeTriangleRotateIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).rotate ≅ hE.stableConflationTriangle (hE.coneSequence f) ⋯

Rotating a stable cone triangle gives the stable conflation triangle of its cone sequence.

Equations

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

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_rotate_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).rotate ∈ hE.stableDistinguishedTriangles

The rotation of a stable cone triangle is distinguished.

theorem TauCeti.ExactStructure.IsFrobenius.rotate_stable_distinguished_triangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (T : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory) (hT : T ∈ hE.stableDistinguishedTriangles) : T.rotate ∈ hE.stableDistinguishedTriangles

Distinguished stable triangles are closed under forward rotation.

Every standard triangle is a rotation

theorem TauCeti.ExactStructure.IsFrobenius.mem_stableDistinguishedTriangles_of_rotate_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (T : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory) (hT : T.rotate ∈ hE.stableDistinguishedTriangles) : T ∈ hE.stableDistinguishedTriangles

A triangle whose rotation is a distinguished stable triangle is itself distinguished.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.rotate_mem_stableDistinguishedTriangles_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (T : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory) : T.rotate ∈ hE.stableDistinguishedTriangles ↔ T ∈ hE.stableDistinguishedTriangles

A triangle is a distinguished stable triangle exactly when its rotation is.