The homotopy category of curved duplexes is triangulated

Let C be an R-linear additive category and w : R. The componentwise split exact structure on curved duplexes of curvature w is Frobenius, and its stable category is identified with the homotopy category CurvedDuplex.HomotopyCategory C w by ExactStructure.curvedDuplexSplitStableToHomotopy, compatibly with the shifts by ℤ (stable suspension on one side, the parity shift on the other). This file transports Happel's triangulation of the stable category along this equivalence, which makes the homotopy category of curved duplexes a triangulated category whose shift by 1 is the parity shift.

The distinguished triangles are described concretely. Let X₁ ⟶ X₂ ⟶ X₃ be a short complex of curved duplexes which splits in both components. Since the disk sum diskSum X₁ is contractible, the inflation X₁ ⟶ diskSum X₁ extends along X₁ ⟶ X₂ to a map a : X₂ ⟶ diskSum X₁, which induces δ : X₃ ⟶ X₁[1] on cokernels. Then

X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁[1]

with third map the homotopy class of δ is distinguished, and every distinguished triangle is isomorphic to one of these.

Main definitions

• TauCeti.CurvedDuplex.HomotopyCategory.instPretriangulated: the pretriangulated structure on the homotopy category of curved duplexes.

Main results

• TauCeti.CurvedDuplex.HomotopyCategory.instIsTriangulated: the homotopy category of curved duplexes is triangulated.
• TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy_isTriangulated: the comparison from the componentwise split stable category is a triangle functor.
• TauCeti.CurvedDuplex.HomotopyCategory.mk_distinguished_of_conflation: componentwise split short complexes give distinguished triangles.
• TauCeti.CurvedDuplex.HomotopyCategory.mem_distTriang_iff: every distinguished triangle is isomorphic to the triangle of a componentwise split short complex.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2, Theorem 2.6: the stable category of a Frobenius category is triangulated.
• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1, for complexes with the componentwise split exact structure.
• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), 1479–1503, Sections 2–3, for curved duplexes and their triangulated homotopy category.

@[instance_reducible]

noncomputable instance TauCeti.CurvedDuplex.HomotopyCategory.instPretriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.Pretriangulated (HomotopyCategory C w)

The homotopy category of curved duplexes is pretriangulated: its distinguished triangles are the images of Happel's distinguished triangles under the equivalence with the componentwise split stable category.

Equations

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

theorem TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy_isTriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (curvedDuplexSplitStableToHomotopy C w).IsTriangulated

The comparison from the componentwise split stable category of curved duplexes to their homotopy category is a triangle functor.

instance TauCeti.CurvedDuplex.HomotopyCategory.instIsTriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.IsTriangulated (HomotopyCategory C w)

The homotopy category of curved duplexes is triangulated, with the shift by 1 given by the parity shift.

theorem TauCeti.CurvedDuplex.HomotopyCategory.mk_distinguished_of_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {S : CategoryTheory.ShortComplex (CurvedDuplex C w)} (hS : ((ExactStructure.split C).curvedDuplex w).Conflation S) (a : S.X₂ ⟶ S.X₁.diskSum) (δ : S.X₃ ⟶ (parityShift C w).obj S.X₁) (ha : CategoryTheory.CategoryStruct.comp S.f a = S.X₁.toDiskSum) (hδ : CategoryTheory.CategoryStruct.comp S.g δ = CategoryTheory.CategoryStruct.comp a S.X₁.diskSumToParityShift) : CategoryTheory.Pretriangulated.Triangle.mk ((nullHomotopic C w).quotientFunctor.map S.f) ((nullHomotopic C w).quotientFunctor.map S.g) (CategoryTheory.CategoryStruct.comp ((nullHomotopic C w).quotientFunctor.map δ) ((parityShiftCompQuotientFunctorIso C w).hom.app S.X₁)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Componentwise split conflations give distinguished triangles. Let X₁ ⟶ X₂ ⟶ X₃ be a short complex of curved duplexes which splits in both components, let a : X₂ ⟶ diskSum X₁ extend the inclusion of X₁ into its disk sum, and let δ : X₃ ⟶ X₁[1] be the map induced by a on cokernels. Then the triangle X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ of homotopy classes, with third map the class of δ, is distinguished.

theorem TauCeti.CurvedDuplex.HomotopyCategory.mem_distTriang_iff (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C w)) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ (S : CategoryTheory.ShortComplex (CurvedDuplex C w)) (_ : ((ExactStructure.split C).curvedDuplex w).Conflation S) (a : S.X₂ ⟶ S.X₁.diskSum) (δ : S.X₃ ⟶ (parityShift C w).obj S.X₁) (_ : CategoryTheory.CategoryStruct.comp S.f a = S.X₁.toDiskSum) (_ : CategoryTheory.CategoryStruct.comp S.g δ = CategoryTheory.CategoryStruct.comp a S.X₁.diskSumToParityShift), Nonempty (T ≅ CategoryTheory.Pretriangulated.Triangle.mk ((nullHomotopic C w).quotientFunctor.map S.f) ((nullHomotopic C w).quotientFunctor.map S.g) (CategoryTheory.CategoryStruct.comp ((nullHomotopic C w).quotientFunctor.map δ) ((parityShiftCompQuotientFunctorIso C w).hom.app S.X₁)))

The distinguished triangles of the homotopy category of curved duplexes are exactly the triangles isomorphic to the triangle of homotopy classes X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ of a componentwise split short complex, with third map induced by an extension X₂ ⟶ diskSum X₁ of the inclusion of X₁ into its disk sum.