Detecting linearity of minimal resolutions by diagonal Ext

Over a nonnegatively graded algebra, a bounded-below minimal graded projective resolution is linear exactly when Ext against modules concentrated in a single internal degree vanishes off the diagonal. Such targets are automatically annihilated by positive-degree scalars. This formulation requires neither a field nor semisimplicity of the degree-zero part; it tests all such targets, rather than only simple targets.

The converse uses the universal degree quotient of each resolution term to detect its pieces modulo positive-degree action. Graded Nakayama then recovers generation in the homological degree. For terms finite over the scalar ring, lower bounds follow from finite grading support. The statements concern a given minimal resolution; they do not construct minimal resolutions.

Below the diagonal no test is needed: Ext out of a minimally resolved module that starts in degree c vanishes in cohomological degree n against every target concentrated below degree c + n.

References

• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Section 1.2, for the diagonal Ext criterion.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded Nakayama.

theorem TauCeti.GradedProjectiveResolution.IsMinimal.subsingleton_ext_of_lt {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) {c : ℤ} (hM : ∀ p < c, M.grading.piece ℤ p = ⊥) (b : ℕ → ℤ) (hbelow : ∀ (n : ℕ), ∀ p < b n, (r.grading n).piece ℤ p = ⊥) {n : ℕ} {p : ℤ} (hp : p < c + ↑n) (N : GradedModuleCat 𝒜) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) : Subsingleton (CategoryTheory.Abelian.Ext M N n)

Ext out of a minimally resolved module vanishes below the diagonal. If M has no nonzero homogeneous elements below degree c and the terms of its minimal resolution are bounded below, then Extⁿ(M,N) = 0 for every target N concentrated in a degree below c + n. The algebra grading need not be nonnegative.

theorem TauCeti.GradedProjectiveResolution.IsMinimal.isLinear_iff_subsingleton_ext {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hneg : ∀ i < 0, 𝒜 i = ⊥) (b : ℕ → ℤ) (hbelow : ∀ (n : ℕ), ∀ p < b n, (r.grading n).piece ℤ p = ⊥) : r.IsLinear ↔ ∀ (n : ℕ) (p : ℤ), ↑n ≠ p → ∀ (N : GradedModuleCat 𝒜), (∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) → Subsingleton (CategoryTheory.Abelian.Ext M N n)

Diagonal Ext detects a bounded-below minimal resolution's linearity. Test every module concentrated in degree p. Neither semisimplicity nor finite generation is needed when termwise lower bounds are supplied.

theorem TauCeti.GradedProjectiveResolution.IsMinimal.isLinear_iff_subsingleton_ext_of_finite {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) [∀ (n : ℕ), Module.Finite k (r.X n)] (hneg : ∀ i < 0, 𝒜 i = ⊥) : r.IsLinear ↔ ∀ (n : ℕ) (p : ℤ), ↑n ≠ p → ∀ (N : GradedModuleCat 𝒜), (∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) → Subsingleton (CategoryTheory.Abelian.Ext M N n)

For a minimal resolution with terms finite over the scalar ring, diagonal Ext vanishing against all concentrated targets is equivalent to linearity. Finiteness replaces the explicit termwise lower bounds.