Distinguished mapping-cone triangles of curved duplexes

The concrete mapping cone realizes the triangulation of the homotopy category of curved duplexes obtained from the componentwise split Frobenius structure. For every closed even map f : X ⟶ Y, the triangle X ⟶ Y ⟶ cone(f) ⟶ X⟦1⟧ is distinguished. Conversely, every distinguished triangle is isomorphic to such a cone triangle.

The last map is minus the canonical projection to the parity shift, followed by its identification with the shift by 1. This is the same sign as Mathlib's CochainComplex.mappingCone.triangle: the cone differential has lower-left block f.

Main results

• HomotopyCategory.coneTriangle_distinguished: concrete cone triangles are distinguished.
• HomotopyCategory.mem_distTriang_iff_nonempty_iso_coneTriangle: cone triangles, up to isomorphism, exhaust the distinguished triangles.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), 1479–1503, Sections 2–3.

@[implicit_reducible]

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C w)

The mapping-cone triangle of a closed even morphism, with last map minus the projection to the parity shift, identified with the shift by 1 in the homotopy category.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (coneTriangle f).obj₁ = (nullHomotopic C w).quotientFunctor.obj X

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (coneTriangle f).obj₂ = (nullHomotopic C w).quotientFunctor.obj Y

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (coneTriangle f).obj₃ = (nullHomotopic C w).quotientFunctor.obj (cone f)

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (coneTriangle f).mor₁ = (nullHomotopic C w).quotientFunctor.map f

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (coneTriangle f).mor₂ = (nullHomotopic C w).quotientFunctor.map (coneInclusion f)

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (coneTriangle f).mor₃ = -CategoryTheory.CategoryStruct.comp ((nullHomotopic C w).quotientFunctor.map (coneProjection f)) ((parityShiftCompQuotientFunctorIso C w).hom.app X)

theorem TauCeti.CurvedDuplex.HomotopyCategory.coneTriangle_distinguished {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X Y : CurvedDuplex C w} [CategoryTheory.Limits.HasZeroObject C] (f : X ⟶ Y) : coneTriangle f ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

The concrete mapping-cone triangle is distinguished for Happel's triangulation of the homotopy category of curved duplexes. No zero-curvature hypothesis is required.

theorem TauCeti.CurvedDuplex.HomotopyCategory.mem_distTriang_iff_nonempty_iso_coneTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} [CategoryTheory.Limits.HasZeroObject C] (T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C w)) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ (X : CurvedDuplex C w) (Y : CurvedDuplex C w) (f : X ⟶ Y), Nonempty (T ≅ coneTriangle f)

Distinguished triangles are precisely those isomorphic to concrete mapping-cone triangles of closed even maps of curved duplexes.