Stable functors commute with the integral shift #
An exact functor between Frobenius exact categories that preserves projective-injective objects
descends to the stable categories and carries suspension to suspension. Since suspension generates
the integral shift on each stable category, this comparison extends coherently to all shifts by
ℤ. Thus the descended functor has the Functor.CommShift ℤ structure required of a
triangulated functor.
Main definitions #
TauCeti.StableConflationExact.stableFunctorCommShift: the coherent compatibility of the descended stable functor with all integral shifts.
References #
- Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
@[instance_reducible]
noncomputable def
TauCeti.StableConflationExact.stableFunctorCommShift
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
:
(hF.stableFunctor hE).CommShift ℤ
The stable functor induced by a stable conflation-exact functor commutes coherently with the integral shifts generated by suspension.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TauCeti.StableConflationExact.stableFunctorCommShift_iso_one
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
:
CategoryTheory.Functor.commShiftIso (hF.stableFunctor hE) 1 = CategoryTheory.Functor.isoWhiskerRight hE.stableShiftFunctorOneIso (hF.stableFunctor hE) ≪≫ hF.stableSuspensionCompStableFunctorIso hE hE' ≪≫ (hF.stableFunctor hE).isoWhiskerLeft hE'.stableShiftFunctorOneIso.symm
In degree one, stable-functor shift compatibility is the suspension comparison used to construct it.