Suspension and loops are inverse autoequivalences of a Frobenius stable category

Let E be a Frobenius exact structure, with chosen conflations X ⟶ I(X) ⟶ ΣX and ΩX ⟶ P(X) ⟶ X whose middle terms are projective-injective. This file proves that the stable suspension and stable loop functors are quasi-inverse, and packages them as an additive autoequivalence of the projective stable category.

The comparisons are the classical ones. Since P(X) is injective, the loop inflation ΩX ⟶ P(X) extends along ΩX ⟶ I(ΩX), which induces ΣΩX ⟶ X on cokernels; its inverse in the stable category is the connecting map X ⟶ ΣΩX of the loop conflation. Dually, since I(X) is projective, the suspension deflation I(X) ⟶ ΣX lifts along P(ΣX) ⟶ ΣX, which induces X ⟶ ΩΣX on kernels, and P(ΣX) lifts along I(X) ⟶ ΣX to give the inverse ΩΣX ⟶ X. All the required identities in the stable category follow from ExactStructure.projectiveStableFunctor_map_τ₃_eq_of_τ₁_eq and its dual: maps of conflations agreeing at one end agree at the other end modulo a projective middle term.

Main definitions

• TauCeti.ExactStructure.IsFrobenius.fromSuspensionLoop: the comparison ΣΩX ⟶ X.
• TauCeti.ExactStructure.IsFrobenius.toLoopSuspension: the comparison X ⟶ ΩΣX.
• TauCeti.ExactStructure.IsFrobenius.fromLoopSuspension: its inverse ΩΣX ⟶ X in the stable category.
• TauCeti.ExactStructure.IsFrobenius.stableLoopCompStableSuspensionIso: Ω ⋙ Σ ≅ 𝟭.
• TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompStableLoopIso: Σ ⋙ Ω ≅ 𝟭.
• TauCeti.ExactStructure.IsFrobenius.stableSuspensionEquivalence: suspension as an autoequivalence of the stable category, with inverse the loop functor.

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.

The comparison ΣΩX ≅ X

noncomputable def TauCeti.ExactStructure.IsFrobenius.fromSuspensionLoop {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.suspensionObj (⋯.loopObj X) ⟶ X

The comparison map ΣΩX ⟶ X, induced on cokernels by the chosen middle map. It is an isomorphism in the stable category.

Equations

• hE.fromSuspensionLoop X = ⋯.desc (CategoryTheory.CategoryStruct.comp (TauCeti.ExactStructure.IsFrobenius.suspensionLoopMiddleMap✝ hE X) (⋯.loopDeflation X)) ⋯

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_comp_fromSuspensionLoop {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.map (CategoryTheory.CategoryStruct.comp (hE.connectingMap ⋯) (hE.fromSuspensionLoop X)) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj { X₁ := ⋯.loopObj X, X₂ := ⋯.loopProjective X, X₃ := X, f := ⋯.loopInflation X, g := ⋯.loopDeflation X, zero := ⋯ }.X₃)

In the stable category, the connecting map X ⟶ ΣΩX of the loop conflation is a right inverse of fromSuspensionLoop.

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_fromSuspensionLoop_comp_connectingMap {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.map (CategoryTheory.CategoryStruct.comp (hE.fromSuspensionLoop X) (hE.connectingMap ⋯)) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj (hE.suspensionObj (⋯.loopObj X)))

In the stable category, the connecting map X ⟶ ΣΩX of the loop conflation is a left inverse of fromSuspensionLoop.

noncomputable def TauCeti.ExactStructure.IsFrobenius.suspensionLoopIso {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 (⋯.loopObj X)) ≅ E.projectiveStableFunctor.obj X

The comparison ΣΩX ≅ X in the stable category.

Equations

• hE.suspensionLoopIso X = { hom := E.projectiveStableFunctor.map (hE.fromSuspensionLoop X), inv := E.projectiveStableFunctor.map (hE.connectingMap ⋯), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.suspensionLoopIso_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.suspensionLoopIso X).hom = E.projectiveStableFunctor.map (hE.fromSuspensionLoop X)

The comparison ΣΩX ≅ X is induced by fromSuspensionLoop.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.suspensionLoopIso_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.suspensionLoopIso X).inv = E.projectiveStableFunctor.map (hE.connectingMap ⋯)

The inverse comparison X ≅ ΣΩX is induced by the connecting map of the loop conflation.

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_fromSuspensionLoop_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) : E.projectiveStableFunctor.map (CategoryTheory.CategoryStruct.comp ((hE.suspensionPresentation (⋯.loopObj X)).cokernelMap (hE.suspensionPresentation (⋯.loopObj Y)) (⋯.loopMap f)) (hE.fromSuspensionLoop Y)) = E.projectiveStableFunctor.map (CategoryTheory.CategoryStruct.comp (hE.fromSuspensionLoop X) f)

The comparison ΣΩX ⟶ X is natural in the stable category.

The comparison X ≅ ΩΣX

noncomputable def TauCeti.ExactStructure.IsFrobenius.toLoopSuspension {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 ⟶ ⋯.loopObj (hE.suspensionObj X)

The comparison map X ⟶ ΩΣX, induced on kernels by the chosen middle map. It is an isomorphism in the stable category.

Equations

• hE.toLoopSuspension X = ⋯.lift (CategoryTheory.CategoryStruct.comp (hE.suspensionInflation X) (TauCeti.ExactStructure.IsFrobenius.loopSuspensionMiddleMap✝ hE X)) ⋯

noncomputable def TauCeti.ExactStructure.IsFrobenius.fromLoopSuspension {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) : ⋯.loopObj (hE.suspensionObj X) ⟶ X

The comparison map ΩΣX ⟶ X, induced on kernels by the chosen middle map. It is the inverse of toLoopSuspension in the stable category.

Equations

• hE.fromLoopSuspension X = ⋯.lift (CategoryTheory.CategoryStruct.comp (⋯.loopInflation (hE.suspensionObj X)) (TauCeti.ExactStructure.IsFrobenius.loopSuspensionInvMiddleMap✝ hE X)) ⋯

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_toLoopSuspension_comp_fromLoopSuspension {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.map (CategoryTheory.CategoryStruct.comp (hE.toLoopSuspension X) (hE.fromLoopSuspension X)) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj X)

In the stable category, fromLoopSuspension is a left inverse of toLoopSuspension.

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_fromLoopSuspension_comp_toLoopSuspension {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.map (CategoryTheory.CategoryStruct.comp (hE.fromLoopSuspension X) (hE.toLoopSuspension X)) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj (⋯.loopObj (hE.suspensionObj X)))

In the stable category, fromLoopSuspension is a right inverse of toLoopSuspension.

noncomputable def TauCeti.ExactStructure.IsFrobenius.loopSuspensionIso {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 X ≅ E.projectiveStableFunctor.obj (⋯.loopObj (hE.suspensionObj X))

The comparison X ≅ ΩΣX in the stable category.

Equations

• hE.loopSuspensionIso X = { hom := E.projectiveStableFunctor.map (hE.toLoopSuspension X), inv := E.projectiveStableFunctor.map (hE.fromLoopSuspension X), hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

The comparison X ⟶ ΩΣX is natural in the stable category.

The autoequivalence

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableLoopCompStableSuspensionIso {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) : ⋯.stableLoop.comp hE.stableSuspension ≅ CategoryTheory.Functor.id E.ProjectiveStableCategory

Loops followed by suspension is isomorphic to the identity of the stable category.

Equations

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

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompStableLoopIso {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.comp ⋯.stableLoop ≅ CategoryTheory.Functor.id E.ProjectiveStableCategory

Suspension followed by loops is isomorphic to the identity of the stable category.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableLoopCompStableSuspensionIso_hom_app {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.stableLoopCompStableSuspensionIso.hom.app (E.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (E.projectiveStableFunctor.map (hE.fromSuspensionLoop X))

On a represented object, the isomorphism ΣΩX ≅ X is fromSuspensionLoop.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableLoopCompStableSuspensionIso_inv_app {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.stableLoopCompStableSuspensionIso.inv.app (E.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap ⋯)) (CategoryTheory.eqToHom ⋯)

On a represented object, the inverse isomorphism X ≅ ΣΩX is the connecting map of the chosen loop conflation.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompStableLoopIso_hom_app {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.stableSuspensionCompStableLoopIso.hom.app (E.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (E.projectiveStableFunctor.map (hE.fromLoopSuspension X))

On a represented object, the isomorphism ΩΣX ≅ X is fromLoopSuspension.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompStableLoopIso_inv_app {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.stableSuspensionCompStableLoopIso.inv.app (E.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.toLoopSuspension X)) (CategoryTheory.eqToHom ⋯)

On a represented object, the inverse isomorphism X ≅ ΩΣX is toLoopSuspension.

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

Suspension is an autoequivalence of the stable category of a Frobenius exact structure, with quasi-inverse the loop functor.

Equations

• hE.stableSuspensionEquivalence = CategoryTheory.Equivalence.mk hE.stableSuspension ⋯.stableLoop hE.stableSuspensionCompStableLoopIso.symm hE.stableLoopCompStableSuspensionIso

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionEquivalence_functor {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.stableSuspensionEquivalence.functor = hE.stableSuspension

The functor of stableSuspensionEquivalence is stable suspension.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionEquivalence_inverse {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.stableSuspensionEquivalence.inverse = ⋯.stableLoop

The inverse of stableSuspensionEquivalence is the stable loop functor.

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

Stable suspension is an equivalence of categories.

instance TauCeti.ExactStructure.IsFrobenius.isEquivalence_stableLoop {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) : ⋯.stableLoop.IsEquivalence

The stable loop functor of a Frobenius exact structure is an equivalence of categories.