The shift on the homotopy category of curved duplexes

The parity shift, which swaps the two components of a curved duplex and negates both differentials, is a self-equivalence of the homotopy category CurvedDuplex.HomotopyCategory C w. This file equips the homotopy category with the shift by ℤ that it generates, so that the shift by 1 is the parity shift.

This is the shift of Happel's triangulation. The componentwise split exact structure on curved duplexes is Frobenius, and every curved duplex X has the relative injective presentation

X ⟶ diskSum X ⟶ X[1]

whose middle term is the contractible disk sum on the components of X and whose cokernel term is the parity shift X[1]. Since stable suspension may be computed from any relative injective presentation, stable suspension is the parity shift in the stable category. Consequently the equivalence ExactStructure.curvedDuplexSplitStableToHomotopy between the stable category and the homotopy category commutes coherently with the shifts by ℤ: the one generated by stable suspension and the one generated by the parity shift. This is the compatibility needed to transport Happel's triangulated structure from the stable category to the homotopy category.

Main definitions

• TauCeti.CurvedDuplex.HomotopyCategory.instHasShift: the shift by ℤ on the homotopy category of curved duplexes generated by the parity shift.
• TauCeti.CurvedDuplex.HomotopyCategory.parityShiftCompQuotientFunctorIso: the image of the parity shift of a curved duplex is the shift by 1 of its image.
• TauCeti.ExactStructure.curvedDuplexSplitSuspensionPresentation: the componentwise split injective presentation X ⟶ diskSum X ⟶ X[1].
• TauCeti.ExactStructure.curvedDuplexSplitStableSuspensionIsoParityShift: stable suspension of curved duplexes is the parity shift.
• TauCeti.ExactStructure.stableSuspensionCompCurvedDuplexSplitStableToHomotopyIso: the stable-to-homotopy comparison intertwines stable suspension with the parity shift.
• TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopyCommShift: the stable-to-homotopy comparison commutes with the shifts by ℤ.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2: suspension in the stable category of a Frobenius category.
• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1, for complexes with the componentwise split exact structure, whose stable category is their homotopy category.
• 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, their parity shift and their homotopy category.

@[instance_reducible]

noncomputable instance TauCeti.CurvedDuplex.HomotopyCategory.instHasShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.HasShift (HomotopyCategory C w) ℤ

The shift by ℤ on the homotopy category of curved duplexes generated by the parity shift.

Equations

• TauCeti.CurvedDuplex.HomotopyCategory.instHasShift C w = (TauCeti.CurvedDuplex.HomotopyCategory.parityShiftEquivalence C w).hasShift

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.shiftFunctorOneIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.shiftFunctor (HomotopyCategory C w) 1 ≅ (parityShiftEquivalence C w).functor

The shift by 1 on the homotopy category of curved duplexes is the parity shift.

Equations

• TauCeti.CurvedDuplex.HomotopyCategory.shiftFunctorOneIso C w = (TauCeti.CurvedDuplex.HomotopyCategory.parityShiftEquivalence C w).shiftFunctorOneIso

theorem TauCeti.CurvedDuplex.HomotopyCategory.shiftFunctorOneIso_def (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : shiftFunctorOneIso C w = (parityShiftEquivalence C w).shiftFunctorOneIso

The identification of the shift by 1 with the parity shift is the one carried by the shift generated by the parity-shift autoequivalence.

instance TauCeti.CurvedDuplex.HomotopyCategory.instAdditiveShiftFunctorInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (n : ℤ) : (CategoryTheory.shiftFunctor (HomotopyCategory C w) n).Additive

Every shift functor of the homotopy category of curved duplexes is additive.

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.parityShiftCompQuotientFunctorIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (parityShift C w).comp (nullHomotopic C w).quotientFunctor ≅ (nullHomotopic C w).quotientFunctor.comp (CategoryTheory.shiftFunctor (HomotopyCategory C w) 1)

The image in the homotopy category of the parity shift of a curved duplex is the shift by 1 of its image, naturally.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.parityShiftCompQuotientFunctorIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (X : CurvedDuplex C w) : (parityShiftCompQuotientFunctorIso C w).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((shiftFunctorOneIso C w).inv.app ((nullHomotopic C w).quotientFunctor.obj X))

The component of parityShiftCompQuotientFunctorIso at X identifies the image of the parity shift of X with the parity shift of its image, followed by shiftFunctorOneIso.

noncomputable def TauCeti.ExactStructure.curvedDuplexSplitSuspensionPresentation {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] (X : CurvedDuplex C w) : ((split C).curvedDuplex w).InjectivePresentation X

The componentwise split injective presentation X ⟶ diskSum X ⟶ X[1] of a curved duplex: its middle term is the contractible disk sum on the components of X, and its cokernel term is the parity shift of X.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitSuspensionPresentation_I {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] (X : CurvedDuplex C w) : (curvedDuplexSplitSuspensionPresentation X).I = X.diskSum

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitSuspensionPresentation_K {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] (X : CurvedDuplex C w) : (curvedDuplexSplitSuspensionPresentation X).K = (CurvedDuplex.parityShift C w).obj X

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitSuspensionPresentation_i {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] (X : CurvedDuplex C w) : (curvedDuplexSplitSuspensionPresentation X).i = X.toDiskSum

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitSuspensionPresentation_p {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] (X : CurvedDuplex C w) : (curvedDuplexSplitSuspensionPresentation X).p = X.diskSumToParityShift

theorem TauCeti.ExactStructure.projectiveStableFunctor_map_curvedDuplexSplitSuspensionPresentation_cokernelMap {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] {X Y : CurvedDuplex C w} (f : X ⟶ Y) : ((split C).curvedDuplex w).projectiveStableFunctor.map ((curvedDuplexSplitSuspensionPresentation X).cokernelMap (curvedDuplexSplitSuspensionPresentation Y) f) = ((split C).curvedDuplex w).projectiveStableFunctor.map ((CurvedDuplex.parityShift C w).map f)

In the stable category, the morphism induced by f on the cokernel terms of the disk-sum presentations is the parity shift of f.

noncomputable def TauCeti.ExactStructure.curvedDuplexSplitStableSuspensionIsoParityShift (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] : ((split C).curvedDuplex w).projectiveStableFunctor.comp ⋯.stableSuspension ≅ (CurvedDuplex.parityShift C w).comp ((split C).curvedDuplex w).projectiveStableFunctor

Stable suspension of curved duplexes is the parity shift. For the componentwise split exact structure, the stable suspension of (the image of) a curved duplex is (the image of) its parity shift, naturally.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitStableSuspensionIsoParityShift_hom_app (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] (X : CurvedDuplex C w) : (curvedDuplexSplitStableSuspensionIsoParityShift C w).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (((split C).curvedDuplex w).projectiveStableFunctor.map ((⋯.suspensionPresentation X).cokernelMap (curvedDuplexSplitSuspensionPresentation X) (CategoryTheory.CategoryStruct.id X)))

The component of curvedDuplexSplitStableSuspensionIsoParityShift at X is induced by the identity of X, from the chosen suspension presentation to the disk-sum presentation.

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitStableSuspensionIsoParityShift_inv_app (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] (X : CurvedDuplex C w) : (curvedDuplexSplitStableSuspensionIsoParityShift C w).inv.app X = CategoryTheory.CategoryStruct.comp (((split C).curvedDuplex w).projectiveStableFunctor.map ((curvedDuplexSplitSuspensionPresentation X).cokernelMap (⋯.suspensionPresentation X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯)

The inverse component of curvedDuplexSplitStableSuspensionIsoParityShift at X is induced by the identity of X, from the disk-sum presentation to the chosen suspension presentation.

noncomputable def TauCeti.ExactStructure.stableSuspensionCompCurvedDuplexSplitStableToHomotopyIso (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] : ⋯.stableSuspension.comp (curvedDuplexSplitStableToHomotopy C w) ≅ (curvedDuplexSplitStableToHomotopy C w).comp (CurvedDuplex.HomotopyCategory.parityShiftEquivalence C w).functor

The comparison from the componentwise split stable category to the homotopy category of curved duplexes intertwines stable suspension with the parity shift.

Equations

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

theorem TauCeti.ExactStructure.stableSuspensionCompCurvedDuplexSplitStableToHomotopyIso_hom_app (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] (X : CurvedDuplex C w) : (stableSuspensionCompCurvedDuplexSplitStableToHomotopyIso C w).hom.app (((split C).curvedDuplex w).projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CurvedDuplex.nullHomotopic C w).quotientFunctor.map ((⋯.suspensionPresentation X).cokernelMap (curvedDuplexSplitSuspensionPresentation X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯))

On the stable image of a curved duplex X, the intertwining isomorphism is the homotopy class of the map induced by the identity of X from the chosen suspension presentation to the disk-sum presentation.

@[instance_reducible]

noncomputable def TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopyCommShift (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] : (curvedDuplexSplitStableToHomotopy C w).CommShift ℤ

The comparison from the componentwise split stable category to the homotopy category of curved duplexes commutes with the shifts by ℤ: the one generated by stable suspension and the one generated by the parity shift.

Equations

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

theorem TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopyCommShift_iso_one (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] : CategoryTheory.Functor.commShiftIso (curvedDuplexSplitStableToHomotopy C w) 1 = CategoryTheory.Functor.isoWhiskerRight ⋯.stableShiftFunctorOneIso (curvedDuplexSplitStableToHomotopy C w) ≪≫ stableSuspensionCompCurvedDuplexSplitStableToHomotopyIso C w ≪≫ (curvedDuplexSplitStableToHomotopy C w).isoWhiskerLeft (CurvedDuplex.HomotopyCategory.shiftFunctorOneIso C w).symm

In degree one, the shift compatibility of the stable-to-homotopy comparison is the identification of stable suspension with the parity shift.