Projective objects in the category of graded modules

A graded module whose underlying module is projective is projective in the graded category. An ungraded lift exists by module projectivity; taking its degree-zero part gives a graded lift without changing its composite with the given graded epimorphism.

This makes projective terms in graded module resolutions into categorical projectives, so the categorical Ext-vanishing and projective Euler-evaluation theorems apply to them. The coefficient ring need not be a field, and no finite-generation or boundedness hypothesis is imposed.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.
• Mathlib's ModuleCat.projective_of_categoryTheory_projective supplies the corresponding ungraded lifting argument; here the lift is additionally made homogeneous.

instance TauCeti.GradedModuleCat.projective_of_module_projective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] (P : GradedModuleCat 𝒜) [Module.Projective A P.carrier] : CategoryTheory.Projective P

An ungraded-projective module is a projective object of the graded module category. Taking the degree-zero part of an ungraded lift produces the required graded lift.