Positive-degree action on concentrated graded modules

A graded module concentrated in a single internal degree is its own piece in that degree, and is annihilated by positive-degree scalars. Concentration is preserved by graded surjections. Such modules are the test targets for detecting the generating degrees of minimal projective resolution terms via Ext. The algebra itself need not be nonnegatively graded.

References

• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Section 1.2, for the concentrated targets of the diagonal Ext criterion.

theorem TauCeti.GradedModuleCat.piece_eq_top_of_concentrated {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {N : GradedModuleCat 𝒜} {p : ℤ} (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) : N.grading.piece ℤ p = ⊤

A graded module concentrated in degree p is its own degree-p piece.

theorem TauCeti.GradedModuleCat.positive_smul_top_eq_bot_of_concentrated {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (N : GradedModuleCat 𝒜) (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥

Positive-degree scalars annihilate any module concentrated in one internal degree.