Detecting linear resolutions by bigraded Ext Poincaré series

For a minimal graded projective resolution with finite-dimensional terms over a nonnegatively graded algebra, linearity is equivalent to diagonal support of the full bigraded Ext Poincaré series against every finite simple target concentrated in degree zero. The coefficient in bidegree (n,j) is dim_k Extⁿ(M,S{j}), so diagonal support retains precisely the off-diagonal vanishing data needed for the converse; the one-variable diagonal Poincaré polynomial alone does not retain that data.

The statement assumes graded Euler-admissibility for the simple targets being tested. This makes the Poincaré series finite without replacing Ext-vanishing by a totalized infinite sum.

For an exhaustive family of finite simple modules concentrated in degree zero, the pointwise criterion assembles into simultaneous linearity exactly when every entry of the family's full bigraded Ext Poincaré matrix is diagonal.

Main results

• TauCeti.GradedProjectiveResolution.IsMinimal.isLinear_iff_isDiagonal_bigradedExtPoincareSeries: diagonal support of the bigraded Ext Poincaré series detects linearity.
• TauCeti.GradedProjectiveResolution.IsMinimal.coeff_bigradedExtPoincareSeries_eq_zero_of_lt: for a minimal resolution of a module starting in degree zero, the series has no coefficients below the diagonal.
• TauCeti.forall_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal: simultaneous linearity of chosen minimal resolutions is equivalent to diagonal support of every matrix entry.
• TauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal: over a semisimple degree-zero part, the same criterion without a preselected family of resolutions.

References

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

theorem TauCeti.GradedProjectiveResolution.IsMinimal.isLinear_iff_isDiagonal_bigradedExtPoincareSeries {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 = ⊥) (hadm : ∀ (N : GradedModuleCat 𝒜), Module.Finite k N.carrier → CategoryTheory.Simple N → (∀ (q : ℤ), q ≠ 0 → N.grading.piece ℤ q = ⊥) → IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) M N) : r.IsLinear ↔ ∀ (N : GradedModuleCat 𝒜) (hNfinite : Module.Finite k N.carrier) (hNsimple : CategoryTheory.Simple N) (hNzero : ∀ (q : ℤ), q ≠ 0 → N.grading.piece ℤ q = ⊥) (b : ℕ), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) M N b → Bigraded.IsDiagonal (bigradedExtPoincareSeries k (GradedModuleCat.shift 𝒜) ⋯ b)

A minimal resolution is linear exactly when its simple-target bigraded Ext Poincaré series are diagonal. The targets range over finite simple graded modules concentrated in degree zero. Graded Euler-admissibility makes each full bigraded series finite; any valid cohomological truncation bound computes the same series.

theorem TauCeti.GradedProjectiveResolution.IsMinimal.coeff_bigradedExtPoincareSeries_eq_zero_of_lt {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) {c : ℤ} (hM : ∀ p < c, M.grading.piece ℤ p = ⊥) {N : GradedModuleCat 𝒜} (hN : ∀ (q : ℤ), q ≠ 0 → N.grading.piece ℤ q = ⊥) (h : IsGradedExtInternallyFinite k (GradedModuleCat.shift 𝒜) M N) (b : ℕ) {m j : ℤ} (hjm : j < c + m) : (bigradedExtPoincareSeries k (GradedModuleCat.shift 𝒜) h b).coeff (m, j) = 0

The bigraded Ext Poincaré series of a minimally resolved module vanishes below a diagonal. If M has no nonzero homogeneous elements below degree c and its minimal resolution has finite-dimensional terms, then the coefficient dim_k Extᵐ(M,N{j}) vanishes for j < c + m whenever N is concentrated in degree zero. For c = 0 there are no coefficients below the diagonal.

theorem TauCeti.forall_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) (hS : IsExhaustiveGradedSimpleFamily S) (hSzero : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (r : (i : I) → GradedProjectiveResolution 𝒜 (S i).obj.grading) [∀ (i : I) (n : ℕ), Module.Finite k ((r i).X n)] (hr : ∀ (i : I), (r i).IsMinimal) (hneg : ∀ p < 0, 𝒜 p = ⊥) {b : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) : (∀ (i : I), (r i).IsLinear) ↔ ∀ (i j : I), Bigraded.IsDiagonal (bigradedExtPoincareMatrix (fun (i : I) => (S i).obj) ⋯ b i j)

Chosen minimal resolutions of an exhaustive simple family are linear exactly when every entry of its full bigraded Ext Poincaré matrix is diagonal. The family is exhaustive up to internal shift, while its chosen representatives are concentrated in degree zero. The matrix uses any common cohomological Ext bound.

theorem TauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] (S : I → (gradedFiniteModules 𝒜).FullSubcategory) (hS : IsExhaustiveGradedSimpleFamily S) (hSzero : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (hneg : ∀ p < 0, 𝒜 p = ⊥) {b : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) : (∀ (i : I), ∃ (r : GradedProjectiveResolution 𝒜 (S i).obj.grading), r.IsLinear) ↔ ∀ (i j : I), Bigraded.IsDiagonal (bigradedExtPoincareMatrix (fun (i : I) => (S i).obj) ⋯ b i j)

Bigraded Ext detects linear resolutions over a semisimple degree-zero part. Suppose that A is finite-dimensional and nonnegatively graded, with semisimple degree-zero part. For an exhaustive family of finite simple modules concentrated in degree zero, every simple admits a linear graded projective resolution if and only if every entry of the full bigraded Ext Poincare matrix has diagonal support.

Unlike TauCeti.forall_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal, this statement does not take a preselected family of minimal resolutions: their existence, with finite-dimensional terms, follows from semisimplicity of the degree-zero part.