The shift on the stable category of a Frobenius exact category

Let E be a Frobenius exact structure. Stable suspension is an additive autoequivalence of the projective stable category, with quasi-inverse the stable loop functor. This file equips the stable category with the shift by ℤ that this autoequivalence generates: its shift by 1 is stable suspension Σ, its shift by -1 is the stable loop functor Ω, and all its shift functors are additive. This is the translation functor with respect to which the stable category is triangulated by Happel's standard triangles X ⟶ Y ⟶ Z ⟶ X⟦1⟧.

The shift depends on the Frobenius hypothesis hE, which is a proposition rather than a class, so it is a definition and not an instance; statements about it install it with letI := hE.stableHasShift.

Main definitions

• TauCeti.ExactStructure.IsFrobenius.stableHasShift: the shift by ℤ on the stable category generated by stable suspension.
• TauCeti.ExactStructure.IsFrobenius.stableShiftFunctorOneIso: its shift by 1 is stable suspension.
• TauCeti.ExactStructure.IsFrobenius.stableShiftFunctorNegOneIso: its shift by -1 is the stable loop functor.
• TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift: the chosen suspension object represents the shift by 1.

Main results

• TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift_hom_naturality: the comparison from chosen suspension objects to the shift is natural.
• TauCeti.ExactStructure.IsFrobenius.stableShiftFunctor_additive: every shift functor of the stable category is additive.

References

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

@[instance_reducible]

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableHasShift {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.HasShift E.ProjectiveStableCategory ℤ

The shift by ℤ on the stable category of a Frobenius exact structure generated by the stable suspension autoequivalence.

Equations

• hE.stableHasShift = hE.stableSuspension.asEquivalence.hasShift

@[instance_reducible]

noncomputable def TauCeti.ExactStructure.IsFrobenius.commShiftOfStableSuspension {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) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} (hE' : E'.IsFrobenius) (F : CategoryTheory.Functor E.ProjectiveStableCategory E'.ProjectiveStableCategory) (hF : F.CommShift ℤ) : F.CommShift ℤ

Transport shift compatibility for a stable functor from the suspension-generated shift to the chosen stable shift.

Equations

• hE.commShiftOfStableSuspension hE' F hF = id hF

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableShiftFunctorOneIso {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.shiftFunctor E.ProjectiveStableCategory 1 ≅ hE.stableSuspension

The shift by 1 on the stable category of a Frobenius exact structure is stable suspension.

Equations

• hE.stableShiftFunctorOneIso = hE.stableSuspension.asEquivalence.shiftFunctorOneIso

theorem TauCeti.ExactStructure.IsFrobenius.commShiftOfStableSuspension_iso_one {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) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} (hE' : E'.IsFrobenius) (F : CategoryTheory.Functor E.ProjectiveStableCategory E'.ProjectiveStableCategory) (α : hE.stableSuspension.comp F ≅ F.comp hE'.stableSuspension) : CategoryTheory.Functor.commShiftIso F 1 = CategoryTheory.Functor.isoWhiskerRight hE.stableShiftFunctorOneIso F ≪≫ α ≪≫ F.isoWhiskerLeft hE'.stableShiftFunctorOneIso.symm

In degree one, transported stable shift compatibility recovers the supplied suspension comparison.

@[instance_reducible]

noncomputable def TauCeti.ExactStructure.IsFrobenius.commShiftOfIntertwiningStableSuspension {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) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (e : D ≌ D) (F : CategoryTheory.Functor E.ProjectiveStableCategory D) (α : hE.stableSuspension.comp F ≅ F.comp e.functor) : F.CommShift ℤ

A functor out of the stable category which intertwines stable suspension with an autoequivalence e of its target commutes coherently with the stable shift and the shift by ℤ generated by e.

Equations

• hE.commShiftOfIntertwiningStableSuspension e F α = id (F.commShiftOfIntertwining hE.stableSuspension.asEquivalence e α)

theorem TauCeti.ExactStructure.IsFrobenius.commShiftOfIntertwiningStableSuspension_iso_one {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) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (e : D ≌ D) (F : CategoryTheory.Functor E.ProjectiveStableCategory D) (α : hE.stableSuspension.comp F ≅ F.comp e.functor) : CategoryTheory.Functor.commShiftIso F 1 = CategoryTheory.Functor.isoWhiskerRight hE.stableShiftFunctorOneIso F ≪≫ α ≪≫ F.isoWhiskerLeft e.shiftFunctorOneIso.symm

In degree one, the shift compatibility of a functor intertwining stable suspension with an autoequivalence e recovers the supplied intertwining isomorphism.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableShiftFunctorNegOneIso {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.shiftFunctor E.ProjectiveStableCategory (-1) ≅ ⋯.stableLoop

The shift by -1 on the stable category of a Frobenius exact structure is the stable loop functor.

Equations

• hE.stableShiftFunctorNegOneIso = hE.stableSuspension.asEquivalence.shiftFunctorNegOneIso hE.stableLoopCompStableSuspensionIso

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift {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 : C) : E.projectiveStableFunctor.obj (hE.suspensionObj X) ≅ (CategoryTheory.shiftFunctor E.ProjectiveStableCategory 1).obj (E.projectiveStableFunctor.obj X)

The chosen suspension object representing X⟦1⟧ is isomorphic to the shift of X in the stable category.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift_hom {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 : C) : (hE.stableSuspensionObjIsoShift X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (hE.stableShiftFunctorOneIso.inv.app (E.projectiveStableFunctor.obj X))

The forward map from the chosen suspension object to the shift.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift_inv {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 : C) : (hE.stableSuspensionObjIsoShift X).inv = CategoryTheory.CategoryStruct.comp (hE.stableShiftFunctorOneIso.hom.app (E.projectiveStableFunctor.obj X)) (CategoryTheory.eqToHom ⋯)

The inverse map from the shift to the chosen suspension object.

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift_hom_naturality {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 : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)) (hE.stableSuspensionObjIsoShift Y).hom = CategoryTheory.CategoryStruct.comp (hE.stableSuspensionObjIsoShift X).hom ((CategoryTheory.shiftFunctor E.ProjectiveStableCategory 1).map (E.projectiveStableFunctor.map f))

The comparison from a chosen suspension object to the shift is natural in morphisms of the exact category.

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionObjIsoShift_hom_naturality_assoc {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 : C} (f : X ⟶ Y) {Z : E.ProjectiveStableCategory} (h : (CategoryTheory.shiftFunctor E.ProjectiveStableCategory 1).obj (E.projectiveStableFunctor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)) (CategoryTheory.CategoryStruct.comp (hE.stableSuspensionObjIsoShift Y).hom h) = CategoryTheory.CategoryStruct.comp (hE.stableSuspensionObjIsoShift X).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E.ProjectiveStableCategory 1).map (E.projectiveStableFunctor.map f)) h)

The comparison from a chosen suspension object to the shift is natural in morphisms of the exact category.

theorem TauCeti.ExactStructure.IsFrobenius.stableShiftFunctor_additive {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) (n : ℤ) : (CategoryTheory.shiftFunctor E.ProjectiveStableCategory n).Additive

Every shift functor on the stable category of a Frobenius exact structure is additive.