The stable category of a Frobenius exact category is triangulated

Let E be a Frobenius exact structure. Its projective stable category is pretriangulated, with the triangles isomorphic to standard triangles X ⟶ Y ⟶ Z ⟶ X⟦1⟧ of conflations. This file proves the octahedral axiom, completing Happel's theorem that the stable category is triangulated.

The octahedron comes from Noether's isomorphism in the exact category. Given conflations X₁ ⟶ X₂ ⟶ Z₁₂ and X₂ ⟶ X₃ ⟶ Z₂₃, the composite X₁ ⟶ X₃ is the inflation of a conflation X₁ ⟶ X₃ ⟶ Z₁₃, and the induced maps form a conflation Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ (TauCeti.ExactStructure.exists_conflation_comp). The standard triangles of these four conflations form an octahedron: its commutativity conditions are the naturality of connecting morphisms along the three evident morphisms of conflations. Every composable pair of stable morphisms is isomorphic to the image of a composable pair of inflations, by replacing a morphism f : X ⟶ Y with the inflation X ⟶ I(X) ⊞ Y of its cone conflation; since the octahedral axiom is invariant under isomorphism of the diagram, this proves it in general.

As with the pretriangulated structure, the Frobenius hypothesis hE is a proposition, so the result is a theorem rather than an instance.

Main definitions

• TauCeti.ExactStructure.IsFrobenius.stableConflationOctahedron: the octahedron formed by the standard triangles of two composable conflations, their composite, and the Noether conflation.

Main results

• TauCeti.ExactStructure.IsFrobenius.mk_distinguished_of_conflation: the standard triangle of a conflation, written with its three arrows, is distinguished.
• TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated: Happel's theorem, the stable category of a Frobenius exact category is triangulated.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2, Theorem 2.6.
• Theo Bühler, Exact Categories, Expositiones Mathematicae 28 (2010), 1–69, Lemma 3.5.

theorem TauCeti.ExactStructure.IsFrobenius.mk_distinguished_of_conflation {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 Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {w : CategoryTheory.CategoryStruct.comp f g = 0} (hS : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := g, zero := w }) {u : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y} (hu : E.projectiveStableFunctor.map f = u) : CategoryTheory.Pretriangulated.Triangle.mk u (E.projectiveStableFunctor.map g) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hS)) (hE.stableSuspensionObjIsoShift X).hom) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

The standard triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ of a conflation X ⟶ Y ⟶ Z, written with its three arrows, is a distinguished stable triangle. The first arrow may be given by any expression equal to the image of the inflation.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConflationOctahedron {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₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {i : X₁ ⟶ X₂} {p : X₂ ⟶ Z₁₂} {hip : CategoryTheory.CategoryStruct.comp i p = 0} {j : X₂ ⟶ X₃} {v : X₃ ⟶ Z₂₃} {hjv : CategoryTheory.CategoryStruct.comp j v = 0} {c : X₃ ⟶ Z₁₃} {hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i j) c = 0} {α : Z₁₂ ⟶ Z₁₃} {β : Z₁₃ ⟶ Z₂₃} {hαβ : CategoryTheory.CategoryStruct.comp α β = 0} (h₁₂ : E.Conflation { X₁ := X₁, X₂ := X₂, X₃ := Z₁₂, f := i, g := p, zero := hip }) (h₂₃ : E.Conflation { X₁ := X₂, X₂ := X₃, X₃ := Z₂₃, f := j, g := v, zero := hjv }) (h₁₃ : E.Conflation { X₁ := X₁, X₂ := X₃, X₃ := Z₁₃, f := CategoryTheory.CategoryStruct.comp i j, g := c, zero := hc }) (hN : E.Conflation { X₁ := Z₁₂, X₂ := Z₁₃, X₃ := Z₂₃, f := α, g := β, zero := hαβ }) (hjc : CategoryTheory.CategoryStruct.comp j c = CategoryTheory.CategoryStruct.comp p α) (hcβ : CategoryTheory.CategoryStruct.comp c β = v) : CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯

Happel's octahedron. For conflations X₁ ⟶ X₂ ⟶ Z₁₂, X₂ ⟶ X₃ ⟶ Z₂₃ and X₁ ⟶ X₃ ⟶ Z₁₃ on a composable pair of inflations and its composite, a conflation Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ compatible with the three deflations makes their standard triangles an octahedron, whose two new arrows are the images of the maps of the fourth conflation. Such a fourth conflation always exists, by TauCeti.ExactStructure.exists_conflation_comp.

Equations

• hE.stableConflationOctahedron h₁₂ h₂₃ h₁₃ hN hjc hcβ = { m₁ := E.projectiveStableFunctor.map α, m₃ := E.projectiveStableFunctor.map β, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯, comm₄ := ⋯, mem := ⋯ }

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationOctahedron_m₁ {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₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {i : X₁ ⟶ X₂} {p : X₂ ⟶ Z₁₂} {hip : CategoryTheory.CategoryStruct.comp i p = 0} {j : X₂ ⟶ X₃} {v : X₃ ⟶ Z₂₃} {hjv : CategoryTheory.CategoryStruct.comp j v = 0} {c : X₃ ⟶ Z₁₃} {hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i j) c = 0} {α : Z₁₂ ⟶ Z₁₃} {β : Z₁₃ ⟶ Z₂₃} {hαβ : CategoryTheory.CategoryStruct.comp α β = 0} (h₁₂ : E.Conflation { X₁ := X₁, X₂ := X₂, X₃ := Z₁₂, f := i, g := p, zero := hip }) (h₂₃ : E.Conflation { X₁ := X₂, X₂ := X₃, X₃ := Z₂₃, f := j, g := v, zero := hjv }) (h₁₃ : E.Conflation { X₁ := X₁, X₂ := X₃, X₃ := Z₁₃, f := CategoryTheory.CategoryStruct.comp i j, g := c, zero := hc }) (hN : E.Conflation { X₁ := Z₁₂, X₂ := Z₁₃, X₃ := Z₂₃, f := α, g := β, zero := hαβ }) (hjc : CategoryTheory.CategoryStruct.comp j c = CategoryTheory.CategoryStruct.comp p α) (hcβ : CategoryTheory.CategoryStruct.comp c β = v) : (hE.stableConflationOctahedron h₁₂ h₂₃ h₁₃ hN hjc hcβ).m₁ = E.projectiveStableFunctor.map α

The first new arrow Z₁₂ ⟶ Z₁₃ of the octahedron is the image of the first map of the Noether conflation.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationOctahedron_m₃ {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₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {i : X₁ ⟶ X₂} {p : X₂ ⟶ Z₁₂} {hip : CategoryTheory.CategoryStruct.comp i p = 0} {j : X₂ ⟶ X₃} {v : X₃ ⟶ Z₂₃} {hjv : CategoryTheory.CategoryStruct.comp j v = 0} {c : X₃ ⟶ Z₁₃} {hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i j) c = 0} {α : Z₁₂ ⟶ Z₁₃} {β : Z₁₃ ⟶ Z₂₃} {hαβ : CategoryTheory.CategoryStruct.comp α β = 0} (h₁₂ : E.Conflation { X₁ := X₁, X₂ := X₂, X₃ := Z₁₂, f := i, g := p, zero := hip }) (h₂₃ : E.Conflation { X₁ := X₂, X₂ := X₃, X₃ := Z₂₃, f := j, g := v, zero := hjv }) (h₁₃ : E.Conflation { X₁ := X₁, X₂ := X₃, X₃ := Z₁₃, f := CategoryTheory.CategoryStruct.comp i j, g := c, zero := hc }) (hN : E.Conflation { X₁ := Z₁₂, X₂ := Z₁₃, X₃ := Z₂₃, f := α, g := β, zero := hαβ }) (hjc : CategoryTheory.CategoryStruct.comp j c = CategoryTheory.CategoryStruct.comp p α) (hcβ : CategoryTheory.CategoryStruct.comp c β = v) : (hE.stableConflationOctahedron h₁₂ h₂₃ h₁₃ hN hjc hcβ).m₃ = E.projectiveStableFunctor.map β

The second new arrow Z₁₃ ⟶ Z₂₃ of the octahedron is the image of the second map of the Noether conflation.

theorem TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated {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.IsTriangulated E.ProjectiveStableCategory

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