The stable category of a Frobenius exact category is pretriangulated

Let E be a Frobenius exact structure. Its projective stable category carries the shift by ℤ generated by stable suspension and the class of distinguished triangles generated by the standard triangles X ⟶ Y ⟶ Z ⟶ X⟦1⟧ of conflations. This file checks the remaining axiom, that the contractible triangles X ⟶ X ⟶ 0 ⟶ X⟦1⟧ are distinguished, and assembles the axioms into Mathlib's CategoryTheory.Pretriangulated structure:

• distinguished triangles are closed under isomorphism by construction;
• the contractible triangle of X is the standard triangle of the split conflation X ⟶ X ⟶ 0;
• every morphism lies in a distinguished cone triangle;
• a triangle is distinguished exactly when its rotation is;
• commutative squares on the first arrows extend to morphisms of distinguished triangles.

As with the shift, the Frobenius hypothesis hE is a proposition, so the structure is a definition rather than an instance; statements install it with letI := hE.stablePretriangulated.

Main definitions

• TauCeti.ExactStructure.IsFrobenius.stablePretriangulated: the pretriangulated structure on the stable category of a Frobenius exact category.

Main results

• TauCeti.ExactStructure.IsFrobenius.contractibleTriangle_mem_stableDistinguishedTriangles: contractible triangles are distinguished.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2, Theorem 2.6.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.contractibleTriangle_mem_stableDistinguishedTriangles {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 : E.ProjectiveStableCategory) : CategoryTheory.Pretriangulated.contractibleTriangle X ∈ hE.stableDistinguishedTriangles

The contractible triangle X ⟶ X ⟶ 0 ⟶ X⟦1⟧ is a distinguished stable triangle: it is the standard triangle of the split conflation X ⟶ X ⟶ 0.

@[instance_reducible]

noncomputable def TauCeti.ExactStructure.IsFrobenius.stablePretriangulated {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) : CategoryTheory.Pretriangulated E.ProjectiveStableCategory

Happel's theorem, pretriangulated part. The stable category of a Frobenius exact category, with the shift generated by stable suspension and the triangles generated by conflations, is pretriangulated.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stablePretriangulated_distinguishedTriangles {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) : CategoryTheory.Pretriangulated.distinguishedTriangles = hE.stableDistinguishedTriangles

The distinguished triangles of stablePretriangulated are the triangles isomorphic to standard triangles of conflations.