The signed Poincaré polynomial of a linear resolution

If M has a linear graded projective resolution and N is concentrated in internal degree zero, then Extⁿ(M,N{j}) vanishes unless j = n. Its target-shift graded dimension is therefore the single monomial dim Extⁿ(M,N{n}) q⁻ⁿ.

For an Euler-admissible pair and any uniform cohomological vanishing bound b, this gives χ_q(M,N) = ∑ n < b, (-1)ⁿ dim Extⁿ(M,N{n}) q⁻ⁿ. Equivalently, applying LaurentPolynomial.invert to χ_q evaluates the diagonal Ext Poincaré polynomial TauCeti.diagonalExtPoincarePolynomial, ∑ n < b, dim Extⁿ(M,N{n}) tⁿ, at t = -q. This identifies the polynomial substitution and involution used to compare graded Cartan and Poincaré matrices. Finiteness and eventual vanishing are explicit hypotheses; a linear resolution alone does not imply them.

The statements include cohomological degree zero and do not require a nonnegative algebra grading, semisimplicity, or finite-dimensionality of the algebra.

References

• A. Beilinson, V. Ginzburg and W. Soergel, "Koszul duality patterns in representation theory", Section 1.2, for the diagonal Ext criterion and the Cartan/Poincaré series identity.
• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Section 2.2, for the target-shift q-Euler convention.

theorem TauCeti.GradedProjectiveResolution.IsLinear.gradedExtDimension_eq {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece ℤ p = ⊥) (n : ℕ) (h : HasFiniteLaurentSupport k (GradedExt (GradedModuleCat.shift 𝒜) M N n)) : gradedExtDimension k (GradedModuleCat.shift 𝒜) h = LaurentPolynomial.C ↑(Module.finrank k (CategoryTheory.Abelian.Ext M (N.shiftObj ↑n) n)) * LaurentPolynomial.T (-↑n)

The graded dimension of Ext from a linearly resolved module into a degree-zero target is a single monomial, with exponent the negative cohomological degree.

theorem TauCeti.GradedProjectiveResolution.IsLinear.gradedExtEuler_eq_sum {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece ℤ p = ⊥) (h : IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) M N) {b : ℕ} (hb : IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) M N b) : gradedExtEuler k (GradedModuleCat.shift 𝒜) h = ∑ n ∈ Finset.range b, (-1) ^ n • (LaurentPolynomial.C ↑(Module.finrank k (CategoryTheory.Abelian.Ext M (N.shiftObj ↑n) n)) * LaurentPolynomial.T (-↑n))

For a linear resolution and a degree-zero target, the q-Euler value is the finite signed diagonal Ext polynomial in q⁻¹. Any uniform cohomological vanishing bound may be used.

theorem TauCeti.GradedProjectiveResolution.IsLinear.coeff_gradedExtEuler_neg_natCast {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece ℤ p = ⊥) (h : IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) M N) (n : ℕ) : (gradedExtEuler k (GradedModuleCat.shift 𝒜) h).coeff (-↑n) = (-1) ^ n * ↑(Module.finrank k (CategoryTheory.Abelian.Ext M (N.shiftObj ↑n) n))

The coefficient of q⁻ⁿ in the q-Euler value is the signed dimension of diagonal Ext. No choice of truncation bound occurs in this coefficient formula.

theorem TauCeti.GradedProjectiveResolution.IsLinear.invert_gradedExtEuler_eq_eval₂ {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece ℤ p = ⊥) (h : IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) M N) {b : ℕ} (hb : IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) M N b) : LaurentPolynomial.invert (gradedExtEuler k (GradedModuleCat.shift 𝒜) h) = Polynomial.eval₂ LaurentPolynomial.C (-LaurentPolynomial.T 1) (diagonalExtPoincarePolynomial k M N b)

Inverting the q-Euler value of a linearly resolved module against a degree-zero target is evaluation of the diagonal Ext Poincaré polynomial at -q.