Simple targets detect linearity of minimal resolutions with finite-dimensional terms

For a nonnegatively graded algebra over a field, a minimal graded projective resolution with finite-dimensional terms is linear exactly when Ext against finite simple objects concentrated in one internal degree vanishes off the diagonal. Thus arbitrary concentrated targets in the diagonal criterion can be replaced by simple ones. The equivalent formulation tests internal shifts of degree-zero simple modules.

The same test without the diagonal restriction detects vanishing terms: if Extⁿ(M, N) vanishes for every finite simple N, the term in homological degree n is zero. Eventual vanishing of Ext against simples therefore truncates the minimal resolution.

Neither semisimplicity of the degree-zero algebra nor a splitting-field assumption is needed. The statement concerns a given minimal resolution, and does not assert existence of such a resolution or eventual Ext vanishing.

References

• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Section 1.2, for the simple-target 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.piece_le_positive_smul_top_of_subsingleton_ext_simple {k : Type uk} [Field 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 = ⊥) (n : ℕ) [Module.Finite k (r.X n)] (p : ℤ) (hExt : ∀ (N : GradedModuleCat 𝒜), Module.Finite k N.carrier → CategoryTheory.Simple N → (∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) → Subsingleton (CategoryTheory.Abelian.Ext M N n)) : (r.grading n).piece ℤ p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

Simple targets detect one piece of a term modulo A₊. For a minimal resolution whose term Xₙ in homological degree n is finite-dimensional, if Extⁿ(M,N) vanishes for every finite simple graded module N concentrated in degree p, then the degree-p piece of Xₙ lies in A₊ Xₙ.

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

A minimal resolution with finite-dimensional terms is linear exactly when Ext against every finite simple graded module concentrated in degree p vanishes in cohomological degrees different from p. This includes degree zero and works over arbitrary fields.

theorem TauCeti.GradedProjectiveResolution.IsMinimal.subsingleton_of_subsingleton_ext_simple {k : Type uk} [Field 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 = ⊥) (n : ℕ) [Module.Finite k (r.X n)] (hExt : ∀ (N : GradedModuleCat 𝒜), Module.Finite k N.carrier → CategoryTheory.Simple N → Subsingleton (CategoryTheory.Abelian.Ext M N n)) : Subsingleton (r.X n)

Simple targets detect vanishing terms of a minimal resolution. For a minimal resolution over a nonnegatively graded algebra whose term Xₙ in homological degree n is finite-dimensional, if Extⁿ(M,N) vanishes for every finite simple graded module N, then Xₙ is zero.

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

Equivalently, test internal shifts of finite simple modules concentrated in degree zero. The shift convention is Extⁿ(M,S{p}) = 0 for n ≠ p.