Graded Nakayama and detection of generating degrees

For a bounded-below internally graded module, the positive-degree part of the algebra cannot surject onto the whole module unless the module is zero. More generally, homogeneous generators modulo the positive-degree action generate the module itself. In particular, over a nonnegatively graded algebra, a bounded-below module is generated in degree d exactly when every homogeneous piece outside degree d lies in A₊ M.

The last criterion expresses concentration of M / A₊ M in degree d without choosing a presentation of that quotient. It detects the generating degrees of terms of minimal graded projective resolutions: maps to modules annihilated by A₊ see precisely this quotient. Neither projectivity nor semisimplicity is needed for the generation criterion. Boundedness below is essential; no finite-generation hypothesis is required when a lower bound is supplied.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of graded rings, Section 2.3, for graded modules.
• A. Beilinson, V. Ginzburg and W. Soergel, "Koszul duality patterns in representation theory", Section 1.2, for detection of linearity via the generating degrees of minimal resolutions.

theorem TauCeti.InternalGrading.decompose_mem_of_mem_positive_smul_top {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] (U : Submodule A M) {p : ℤ} (hU : ∀ q < p, ∀ x ∈ G.piece q, x ∈ U) {x : M} (hx : x ∈ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤) : ↑(((DirectSum.decompose G.piece) x) p) ∈ U

A component of A₊ M lies in an A-submodule if all lower-degree pieces do. The positive scalar lowers the degree of the module component needed to compute that component.

theorem TauCeti.InternalGrading.eq_top_of_piece_le_sup_positive_smul_top {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] (U : Submodule A M) (hhom : DirectSum.SetLike.IsHomogeneous G.piece U) (b : ℤ) (hbelow : ∀ p < b, G.piece p = ⊥) (hU : ∀ (p : ℤ), G.piece p ≤ Submodule.restrictScalars k U ⊔ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤) : U = ⊤

Graded Nakayama for homogeneous generators. In a bounded-below graded module, if each homogeneous piece lies in the sum of a homogeneous A-submodule and the positive-degree action on the module, then that submodule is the whole module. This is generation modulo A₊.

theorem TauCeti.InternalGrading.subsingleton_of_positive_smul_top_eq_top {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] (b : ℤ) (hbelow : ∀ p < b, G.piece p = ⊥) (h : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊤) : Subsingleton M

Graded Nakayama. A bounded-below graded module satisfying A₊ M = M is zero.

theorem TauCeti.InternalGrading.isGeneratedInDegree_iff_piece_le_positive_smul_top {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] [GradedAlgebra 𝒜] (h𝒜 : ∀ i < 0, 𝒜 i = ⊥) (b : ℤ) (hbelow : ∀ p < b, G.piece p = ⊥) (d : ℤ) : G.IsGeneratedInDegree A d ↔ ∀ (p : ℤ), p ≠ d → G.piece p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

A bounded-below module over a nonnegatively graded algebra is generated in degree d exactly when its homogeneous pieces outside degree d lie in A₊ M. Equivalently, its quotient by the positive-degree action is concentrated in degree d.

theorem TauCeti.InternalGrading.isGeneratedInDegree_iff_piece_le_positive_smul_top_of_finite {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] [GradedAlgebra 𝒜] [Module.Finite k M] (h𝒜 : ∀ i < 0, 𝒜 i = ⊥) (d : ℤ) : G.IsGeneratedInDegree A d ↔ ∀ (p : ℤ), p ≠ d → G.piece p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

The generating-degree criterion for a module finite over the grading's scalar semiring. Its internal grading has finite support, which supplies the lower bound automatically.