Detecting linear graded resolutions

A graded projective resolution is linear when its term in homological degree n is generated in internal degree n. For a nonnegatively graded algebra, graded Nakayama detects this condition on the quotient of each term by the positive-degree action A₊: the resolution is linear exactly when the quotient of its nth term is concentrated in internal degree n.

This criterion is stated both with explicit termwise lower bounds and for terms finite over the grading's scalar ring. It is the generation-theoretic bridge from computations of a minimal resolution modulo A₊ to linearity of that resolution.

Half of linearity holds for every minimal resolution: if the resolved module starts in degree c, the term in homological degree n starts in degree c + n. This is the triangularity that lets numerical invariants of minimal resolutions detect linearity.

Main results

• TauCeti.GradedProjectiveResolution.isLinear_iff_piece_le_positive_smul_top: the bounded-below criterion.
• TauCeti.GradedProjectiveResolution.isLinear_iff_piece_le_positive_smul_top_of_finite: the finite-term criterion.
• TauCeti.GradedProjectiveResolution.IsMinimal.piece_eq_bot_of_lt: the terms of a minimal resolution start in their homological degree.

References

• A. Beilinson, V. Ginzburg and W. Soergel, "Koszul duality patterns in representation theory", Section 1.2, for detecting linear resolutions from their generating degrees.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded Nakayama.

theorem TauCeti.GradedProjectiveResolution.isLinear_iff_piece_le_positive_smul_top {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M ℤ} {r : GradedProjectiveResolution 𝒜 G} (h𝒜 : ∀ i < 0, 𝒜 i = ⊥) (b : ℕ → ℤ) (hbelow : ∀ (n : ℕ), ∀ p < b n, (r.grading n).piece ℤ p = ⊥) : r.IsLinear ↔ ∀ (n : ℕ) (p : ℤ), p ≠ ↑n → (r.grading n).piece ℤ p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

A resolution is linear exactly when every term modulo A₊ is concentrated in its homological degree, provided each term is bounded below. The explicit lower bounds may depend on the homological degree.

theorem TauCeti.GradedProjectiveResolution.isLinear_iff_piece_le_positive_smul_top_of_finite {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M ℤ} {r : GradedProjectiveResolution 𝒜 G} [∀ (n : ℕ), Module.Finite k (r.X n)] (h𝒜 : ∀ i < 0, 𝒜 i = ⊥) : r.IsLinear ↔ ∀ (n : ℕ) (p : ℤ), p ≠ ↑n → (r.grading n).piece ℤ p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

For a resolution whose terms are finite over the grading's scalar ring, linearity is equivalent to concentration of each term modulo A₊ in its homological degree. Finiteness supplies the lower bounds required by graded Nakayama.

theorem TauCeti.GradedProjectiveResolution.IsMinimal.piece_eq_bot_of_lt {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M ℤ} {r : GradedProjectiveResolution 𝒜 G} (hr : r.IsMinimal) {c : ℤ} (hG : ∀ p < c, G.piece ℤ p = ⊥) (b : ℕ → ℤ) (hbelow : ∀ (n : ℕ), ∀ p < b n, (r.grading n).piece ℤ p = ⊥) (n : ℕ) {p : ℤ} : p < c + ↑n → (r.grading n).piece ℤ p = ⊥

The terms of a minimal resolution start in their homological degree. If the resolved module has no nonzero homogeneous elements below degree c and every term of a minimal resolution is bounded below, then the term in homological degree n has no nonzero homogeneous elements below degree c + n. The algebra grading need not be nonnegative.