Suspension on a Frobenius stable category

Let E be a Frobenius exact structure. For every object X, choose a conflation

X ⟶ I(X) ⟶ ΣX

with injective middle term. A morphism f : X ⟶ Y extends to a map I(X) ⟶ I(Y), hence induces a map ΣX ⟶ ΣY. Neither extension is unique in the original category, but any two choices differ by a morphism through an injective, which is projective under the Frobenius hypothesis. The induced map is therefore canonical in the projective stable quotient.

This file carries out that construction and obtains the additive suspension endofunctor of the stable category. The loop functor and the proof that the two are quasi-inverse are developed separately.

The choice of conflation is immaterial: the cokernel term of any relative injective presentation of X is canonically isomorphic to ΣX in the stable category, naturally in X.

Main definitions

• TauCeti.ExactStructure.IsFrobenius.suspensionPresentation: the chosen injective conflation.
• TauCeti.ExactStructure.IsFrobenius.suspensionObj: its cokernel term ΣX.
• TauCeti.ExactStructure.IsFrobenius.stableSuspension: the additive suspension endofunctor of the projective stable category.
• TauCeti.ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj: the comparison of the cokernel term of an arbitrary relative injective presentation with ΣX.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1.

noncomputable def TauCeti.ExactStructure.IsFrobenius.suspensionPresentation {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.InjectivePresentation X

The chosen conflation X ⟶ I(X) ⟶ ΣX used to construct suspension.

Equations

• hE.suspensionPresentation X = ⋯.injectivePresentation X

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.suspensionInjective {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) : C

The chosen injective object in the suspension presentation of X.

Equations

• hE.suspensionInjective X = (hE.suspensionPresentation X).I

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.suspensionObj {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) : C

The suspension object ΣX, defined as the third term of the chosen injective conflation.

Equations

• hE.suspensionObj X = (hE.suspensionPresentation X).K

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.suspensionInflation {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) : X ⟶ hE.suspensionInjective X

The inflation X ⟶ I(X) in the chosen suspension presentation.

Equations

• hE.suspensionInflation X = (hE.suspensionPresentation X).i

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.suspensionDeflation {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.suspensionInjective X ⟶ hE.suspensionObj X

The deflation I(X) ⟶ ΣX in the chosen suspension presentation.

Equations

• hE.suspensionDeflation X = (hE.suspensionPresentation X).p

theorem TauCeti.ExactStructure.IsFrobenius.isInflation_suspensionInflation {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.IsInflation (hE.suspensionInflation X)

The inflation of the chosen suspension presentation of X is an inflation of E.

noncomputable def TauCeti.ExactStructure.IsFrobenius.suspensionToStable {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.Functor C E.ProjectiveStableCategory

Suspension from the exact category to its stable quotient, built from the chosen injective presentations.

Equations

• hE.suspensionToStable = E.suspensionToStableOfPresentations hE.suspensionPresentation ⋯

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.suspensionToStable_obj {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.suspensionToStable.obj X = E.projectiveStableFunctor.obj (hE.suspensionObj X)

Suspension to the stable quotient sends X to the image of ΣX.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.suspensionToStable_map {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) : hE.suspensionToStable.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)) (CategoryTheory.eqToHom ⋯))

Suspension to the stable quotient sends f to the image of the map induced between the chosen injective presentations.

instance TauCeti.ExactStructure.IsFrobenius.suspensionToStable_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) : hE.suspensionToStable.Additive

theorem TauCeti.ExactStructure.IsFrobenius.isProjective_suspensionObj {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} (hX : E.isProjective X) : E.isProjective (hE.suspensionObj X)

The suspension of a projective object is projective. Thus suspension sends every object killed by the stable quotient to another object killed by it.

theorem TauCeti.ExactStructure.IsFrobenius.suspensionToStable_kills_projectiveStableIdeal {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) : E.projectiveStableIdeal ≤ hE.suspensionToStable.kerIdeal

The functor from the exact category to the stable category kills the projective stable ideal, so it descends to an endofunctor of the stable category.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableSuspension {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.Functor E.ProjectiveStableCategory E.ProjectiveStableCategory

The additive suspension endofunctor on the stable category of a Frobenius exact structure.

Equations

• hE.stableSuspension = E.projectiveStableIdeal.lift hE.suspensionToStable ⋯

instance TauCeti.ExactStructure.IsFrobenius.stableSuspension_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) : hE.stableSuspension.Additive

Stable suspension preserves addition of morphisms.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspension_obj_projectiveStableFunctor_obj {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.stableSuspension.obj (E.projectiveStableFunctor.obj X) = E.projectiveStableFunctor.obj (hE.suspensionObj X)

On objects represented by X, stable suspension is represented by ΣX.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspension_map_projectiveStableFunctor_map {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) : hE.stableSuspension.map (E.projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)) (CategoryTheory.eqToHom ⋯))

On represented morphisms, stable suspension is induced by the chosen injective presentations.

noncomputable def TauCeti.ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj {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} (P : E.InjectivePresentation X) : E.projectiveStableFunctor.obj P.K ≅ E.projectiveStableFunctor.obj (hE.suspensionObj X)

The cokernel term of an arbitrary relative injective presentation of X represents the suspension ΣX in the projective stable category: the chosen presentation enjoys no privilege there.

Equations

• hE.projectiveStableIsoSuspensionObj P = P.projectiveStableIso (hE.suspensionPresentation X) ⋯ ⋯

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj_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} (P : E.InjectivePresentation X) : (hE.projectiveStableIsoSuspensionObj P).hom = E.projectiveStableFunctor.map (P.cokernelMap (hE.suspensionPresentation X) (CategoryTheory.CategoryStruct.id X))

The comparison with the suspension is induced by the identity of the presented object.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj_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} (P : E.InjectivePresentation X) : (hE.projectiveStableIsoSuspensionObj P).inv = E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap P (CategoryTheory.CategoryStruct.id X))

The inverse comparison with the suspension is the one induced in the other direction.

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj_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} (P : E.InjectivePresentation X) (Q : E.InjectivePresentation Y) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.cokernelMap Q f)) (hE.projectiveStableIsoSuspensionObj Q).hom = CategoryTheory.CategoryStruct.comp (hE.projectiveStableIsoSuspensionObj P).hom (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f))

Representing the suspension by an arbitrary relative injective presentation is natural: it carries the morphism induced by f on cokernel terms to the suspension of f.

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj_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} (P : E.InjectivePresentation X) (Q : E.InjectivePresentation Y) (f : X ⟶ Y) {Z : E.ProjectiveStableCategory} (h : E.projectiveStableFunctor.obj (hE.suspensionObj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.cokernelMap Q f)) (CategoryTheory.CategoryStruct.comp (hE.projectiveStableIsoSuspensionObj Q).hom h) = CategoryTheory.CategoryStruct.comp (hE.projectiveStableIsoSuspensionObj P).hom (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)) h)

Representing the suspension by an arbitrary relative injective presentation is natural: it carries the morphism induced by f on cokernel terms to the suspension of f.