The graded-split stable category is the curved homotopy category

A null-homotopic closed map factors through the cone of the identity of its source. Conversely, every map factoring through a contractible module is zero in the homotopy category. Since the relative projectives of the graded-split exact structure are exactly the contractible modules, its stable ideal is the kernel of the existing closed-to-homotopy functor. The resulting comparison is an additive linear equivalence, without introducing another homotopy category.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.
• The Tau Ceti contributors, TauCeti.Algebra.Homology.Curved.Frobenius: the stable ideal and comparison proofs adapt the corresponding componentwise split construction.

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_projectiveStableIdeal_eq_kerIdeal {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.projectiveStableIdeal = (dgClosedToHomotopy R).kerIdeal

The projective stable ideal of the graded-split exact structure is the kernel of the canonical functor to the curved homotopy category.

noncomputable def TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy {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 gradedSplitExact.ProjectiveStableCategory (DGHomotopyCategory R (CurvedDGRightModuleCat h))

The canonical additive comparison from the graded-split stable category to the existing curved homotopy category.

theorem TauCeti.CurvedDGRightModuleCat.projectiveStableFunctor_comp_gradedSplitStableToHomotopy {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 gradedSplitStableToHomotopy = dgClosedToHomotopy R

The stable comparison restricts to the canonical homotopy quotient.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy_obj_projectiveStableFunctor_obj {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)) : gradedSplitStableToHomotopy.obj (gradedSplitExact.projectiveStableFunctor.obj X) = (dgClosedToHomotopy R).obj X

The stable comparison sends a closed object's stable image to its homotopy class.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy_map_projectiveStableFunctor_map {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 Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (f : X ⟶ Y) : gradedSplitStableToHomotopy.map (gradedSplitExact.projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map f) (CategoryTheory.eqToHom ⋯))

On the class of a closed map, the stable comparison is the canonical homotopy quotient.

instance TauCeti.CurvedDGRightModuleCat.instAdditiveProjectiveStableCategoryForgetEnrichmentCochainComplexModuleCatIntGradedSplitExactDGHomotopyCategoryGradedSplitStableToHomotopy {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.Additive

instance TauCeti.CurvedDGRightModuleCat.instLinearProjectiveStableCategoryForgetEnrichmentCochainComplexModuleCatIntGradedSplitExactDGHomotopyCategoryGradedSplitStableToHomotopy {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.Linear R gradedSplitStableToHomotopy

instance TauCeti.CurvedDGRightModuleCat.instIsEquivalenceProjectiveStableCategoryForgetEnrichmentCochainComplexModuleCatIntGradedSplitExactDGHomotopyCategoryGradedSplitStableToHomotopy {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.IsEquivalence

noncomputable def TauCeti.CurvedDGRightModuleCat.gradedSplitStableHomotopyEquivalence {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.ProjectiveStableCategory ≌ DGHomotopyCategory R (CurvedDGRightModuleCat h)

The linear equivalence between the graded-split stable category and the existing curved homotopy category.