Suspension in the opposite stable category

For a Frobenius exact category, the comparison from the stable category of the opposite to the opposite stable category carries suspension to the opposite loop functor. Thus duality reverses the direction of translation. The comparison is canonical despite the independent choices of presentations: an opposite loop presentation is an injective presentation, and the stable comparison of injective presentations identifies it with the chosen suspension presentation.

This file constructs that natural isomorphism and gives its components on representatives. Compatibility with distinguished triangles is a separate assertion.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
• TauCeti.CategoryTheory.Exact.Stable.Presentation: the canonical stable comparison of injective presentations used here.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompProjectiveStableOpFunctorIso {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) : ⋯.stableSuspension.comp (E.projectiveStableOpFunctor ⋯) ≅ (E.projectiveStableOpFunctor ⋯).comp ⋯.stableLoop.op

The canonical opposite stable comparison carries suspension in the opposite exact category to the opposite of the loop functor in the original exact category.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompProjectiveStableOpFunctorIso_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.stableSuspensionCompProjectiveStableOpFunctorIso.hom.app (E.op.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((E.projectiveStableOpFunctor ⋯).map (E.op.projectiveStableFunctor.map ((⋯.suspensionPresentation X).cokernelMap (⋯.projectivePresentation (Opposite.unop X)).op (CategoryTheory.CategoryStruct.id X)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)))))

On a represented object, the comparison is the image of the canonical comparison from the chosen opposite suspension presentation to the opposite loop presentation.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableSuspensionCompProjectiveStableOpFunctorIso_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.stableSuspensionCompProjectiveStableOpFunctorIso.inv.app (E.op.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((E.projectiveStableOpFunctor ⋯).map (E.op.projectiveStableFunctor.map ((⋯.projectivePresentation (Opposite.unop X)).op.cokernelMap (⋯.suspensionPresentation X) (CategoryTheory.CategoryStruct.id X)))) (CategoryTheory.eqToHom ⋯)))))

The inverse component is induced by the comparison from the opposite loop presentation to the chosen opposite suspension presentation.