The closed category of curved right modules is abelian

Kernels and cokernels carry their inherited differentials. The faithful graded forgetful functor preserves these constructions and reflects isomorphisms. The coimage-to-image comparison in the closed category is an isomorphism, as detected in the abelian graded module category. This characterizes the abelian structure on the closed category of curved modules.

The graded forgetful functor preserves finite limits and colimits. This ambient abelian category and its forgetful functor support the graded-split exact structure on curved modules.

References

• The Tau Ceti contributors, TauCeti.Algebra.Category.GradedModuleCat.Abelian.
• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.

instance TauCeti.CurvedDGRightModuleCat.instIsIsoForgetEnrichmentCochainComplexModuleCatIntCoimageImageComparison {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 : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (f : M ⟶ N) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)

The closed category's coimage-to-image comparison is an isomorphism.

@[instance_reducible]

noncomputable instance TauCeti.CurvedDGRightModuleCat.instAbelianClosedCategory {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.Abelian (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))

The closed category of curved right modules is abelian, as detected by graded modules.

instance TauCeti.CurvedDGRightModuleCat.instPreservesFiniteLimitsForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionForgetDifferential {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.Limits.PreservesFiniteLimits forgetDifferential

The graded forgetful functor preserves finite limits of closed curved-module diagrams.

instance TauCeti.CurvedDGRightModuleCat.instPreservesFiniteColimitsForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionForgetDifferential {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.Limits.PreservesFiniteColimits forgetDifferential

The graded forgetful functor preserves finite colimits of closed curved-module diagrams.