Stable suspension of curved right modules is the cohomological shift

The graded-split exact structure on curved right modules is Frobenius, and every module M has the relative injective presentation M ⟶ cone(𝟙 M) ⟶ M[1]: its middle term is contractible. A closed map f induces a map of these cone sequences whose cokernel component is the shift of f. Since stable suspension may be computed from any relative injective presentation, it is naturally the cohomological shift by one in the stable category.

Consequently the stable-to-homotopy equivalence gradedSplitStableToHomotopy intertwines stable suspension with the existing shift by one on the curved homotopy category, and so commutes with all the integral shifts: the one generated by stable suspension and the coherent cohomological shift. This is the shift compatibility along which Happel's triangulation is transported to the curved homotopy category.

Main definitions

• TauCeti.CurvedDGRightModuleCat.gradedSplitStableSuspensionIsoShift: stable suspension of the graded-split exact structure is naturally the image of the cohomological shift by one.
• TauCeti.CurvedDGRightModuleCat.stableSuspensionCompGradedSplitStableToHomotopyIso: the stable-to-homotopy comparison intertwines stable suspension with the shift by one.
• TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopyCommShift: the stable-to-homotopy comparison commutes with the shifts by ℤ.
• TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy_map_connectingMap: identity-cone extensions compute the transported stable connecting arrows of graded-split conflations.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.
• D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2: suspension in the stable category of a Frobenius category.
• The Tau Ceti contributors, TauCeti.Algebra.Homology.Periodic.Suspension: the natural isomorphism and its transport to the homotopy category follow the identity-cone comparison for periodic complexes.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.projectiveStableFunctor_map_coneIdentityInjectivePresentation_cokernelMap {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {M N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : gradedSplitExact.projectiveStableFunctor.map (M.coneIdentityInjectivePresentation.cokernelMap N.coneIdentityInjectivePresentation f) = gradedSplitExact.projectiveStableFunctor.map (f⟦1⟧')

The map induced on the cokernels of identity-cone presentations is the shift of the original closed map, in the projective stable category.

noncomputable def TauCeti.CurvedDGRightModuleCat.gradedSplitStableSuspensionIsoShift {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} : gradedSplitExact.projectiveStableFunctor.comp ⋯.stableSuspension ≅ (CategoryTheory.shiftFunctor (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) 1).comp gradedSplitExact.projectiveStableFunctor

Stable suspension of curved right modules is the cohomological shift. For the graded-split exact structure, the stable suspension of (the image of) a curved module is (the image of) its shift by one, naturally.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableSuspensionIsoShift_hom_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : gradedSplitStableSuspensionIsoShift.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (gradedSplitExact.projectiveStableFunctor.map ((⋯.suspensionPresentation X).cokernelMap (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X).coneIdentityInjectivePresentation (CategoryTheory.CategoryStruct.id X)))

The component of gradedSplitStableSuspensionIsoShift at X is induced by the identity of X, from the chosen suspension presentation to the identity-cone presentation.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableSuspensionIsoShift_inv_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : gradedSplitStableSuspensionIsoShift.inv.app X = CategoryTheory.CategoryStruct.comp (gradedSplitExact.projectiveStableFunctor.map ((CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X).coneIdentityInjectivePresentation.cokernelMap (⋯.suspensionPresentation X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯)

The inverse component of gradedSplitStableSuspensionIsoShift at X is induced by the identity of X, from the identity-cone presentation to the chosen suspension presentation.

noncomputable def TauCeti.CurvedDGRightModuleCat.stableSuspensionCompGradedSplitStableToHomotopyIso {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} : ⋯.stableSuspension.comp gradedSplitStableToHomotopy ≅ gradedSplitStableToHomotopy.comp (CategoryTheory.shiftFunctor (DGHomotopyCategory R (CurvedDGRightModuleCat h)) 1)

The stable-to-homotopy comparison intertwines stable suspension with the shift by one on the curved homotopy category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.stableSuspensionCompGradedSplitStableToHomotopyIso_hom_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : stableSuspensionCompGradedSplitStableToHomotopyIso.hom.app (gradedSplitExact.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (gradedSplitStableToHomotopy.map (gradedSplitStableSuspensionIsoShift.hom.app X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (dgClosedToHomotopy R) 1).hom.app X) (CategoryTheory.eqToHom ⋯)))

On the stable image of a curved module, the intertwining isomorphism is the image of the suspension comparison, followed by the quotient's shift comparison.

@[instance_reducible]

noncomputable def TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopyCommShift {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} : gradedSplitStableToHomotopy.CommShift ℤ

The comparison from the graded-split stable category to the curved homotopy category commutes with the shifts by ℤ: the one generated by stable suspension and the coherent cohomological shift.

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopyCommShift_iso_one {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} : CategoryTheory.Functor.commShiftIso gradedSplitStableToHomotopy 1 = CategoryTheory.Functor.isoWhiskerRight ⋯.stableShiftFunctorOneIso gradedSplitStableToHomotopy ≪≫ stableSuspensionCompGradedSplitStableToHomotopyIso

In degree one, the shift compatibility of the stable-to-homotopy comparison is the identification of stable suspension with the cohomological shift.

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy_map_connectingMap {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : gradedSplitExact.Conflation S) (a : S.X₂ ⟶ (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.I) (δ : S.X₃ ⟶ (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.K) (ha : CategoryTheory.CategoryStruct.comp S.f a = (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.i) (hδ : CategoryTheory.CategoryStruct.comp S.g δ = CategoryTheory.CategoryStruct.comp a (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.p) : CategoryTheory.CategoryStruct.comp (gradedSplitStableToHomotopy.map (CategoryTheory.CategoryStruct.comp (gradedSplitExact.projectiveStableFunctor.map (⋯.connectingMap hS)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (⋯.stableShiftFunctorOneIso.inv.app (gradedSplitExact.projectiveStableFunctor.obj S.X₁))))) ((CategoryTheory.Functor.commShiftIso gradedSplitStableToHomotopy 1).hom.app (gradedSplitExact.projectiveStableFunctor.obj S.X₁)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map δ) (CategoryTheory.eqToHom ⋯))

The stable connecting arrow of a graded-split conflation is the homotopy class of the map induced by an extension to the identity-cone presentation. The canonical suspension and shift comparisons identify its target with the cohomological shift, with positive sign.