Ext Poincaré series

For objects X and Y of a k-linear abelian category with a grading-shift autoequivalence e, the bigraded Ext Poincaré series records every finite dimension dim_k Extⁿ(X,Y{j}) in bidegree (n,j). It is truncated below a cohomological degree b; when b is a vanishing bound, it records the complete bigraded Ext space. Its support is diagonal exactly when all off-diagonal groups Extⁿ(X,Y{j}), n ≠ j, vanish.

For graded modules M and N, the diagonal Ext Poincaré polynomial TauCeti.diagonalExtPoincarePolynomial is ∑ n < b, finrank_k Extⁿ(M,N{n}) tⁿ, truncated below a cohomological degree b. It records only the diagonal bigraded pieces Ext^{n,n}(M,N). The coefficients use the Module.finrank convention: they are the dimensions dim_k Extⁿ(M,N{n}) when these Ext spaces are finite-dimensional, and an infinite-dimensional Ext group contributes 0. For a family S of graded modules, TauCeti.diagonalExtPoincareMatrix collects these polynomials into a matrix with (i, j) entry the polynomial of (Sᵢ, Sⱼ).

The bigraded series takes the finite-internal-support witness needed to make every coefficient finite and every slice finitely supported. It is independent of b past a cohomological vanishing bound (TauCeti.bigradedExtPoincareSeries_eq_of_le). The diagonal polynomial and matrix are defined for arbitrary graded modules and are likewise independent of a sufficiently large b (TauCeti.diagonalExtPoincarePolynomial_eq_of_le and TauCeti.diagonalExtPoincareMatrix_eq_of_le).

Main definitions and results

• TauCeti.bigradedExtPoincareSeries: the complete truncated bigraded dimension of Ext, with its defining double sum TauCeti.bigradedExtPoincareSeries_def.
• TauCeti.bigradedExtPoincareMatrix: the full bigraded Ext Poincaré matrix of a family.
• TauCeti.isDiagonal_bigradedExtPoincareSeries_iff: diagonal support is equivalent to off-diagonal Ext-vanishing when the truncation is a vanishing bound.
• TauCeti.invert_gradedExtEuler_eq_euler_bigradedExtPoincareSeries: the q-Euler characteristic is the Euler characteristic of the bigraded series, up to q ↦ q⁻¹.
• TauCeti.diagonalExtPoincarePolynomial and TauCeti.diagonalExtPoincareMatrix: the one-variable diagonal series and its matrix for a family of modules.

References

• A. Beilinson, V. Ginzburg and W. Soergel, "Koszul duality patterns in representation theory", Sections 1.2 and 2.11, for bigraded Ext, its diagonal, and the Poincaré series of diagonal Ext.

noncomputable def TauCeti.bigradedExtPoincareSeries {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (e : C ≌ C) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (b : ℕ) : Bigraded.Series

The bigraded Ext Poincaré series of two objects, truncated below cohomological degree b. Its coefficient in bidegree (n,j) is dim_k Extⁿ(X,Y{j}) for n < b and zero otherwise, where {j} is the j-fold power of the grading-shift autoequivalence e. The finite internal support hypothesis makes every cohomological slice a genuine finite sum.

theorem TauCeti.bigradedExtPoincareSeries_def {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (e : C ≌ C) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (b : ℕ) : bigradedExtPoincareSeries k e h b = ∑ n ∈ Finset.range b, ∑ j ∈ ⋯.toFinset, AddMonoidAlgebra.single (↑n, j) (Module.finrank k (GradedExt e X Y n j))

The bigraded Ext Poincaré series is the truncated double sum of the monomials dim_k Extⁿ(X,Y{j}) · (n,j) over the finite internal support of each cohomological degree.

@[simp]

theorem TauCeti.coeff_bigradedExtPoincareSeries {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (e : C ≌ C) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (b n : ℕ) (j : ℤ) : (bigradedExtPoincareSeries k e h b).coeff (↑n, j) = if n < b then Module.finrank k (GradedExt e X Y n j) else 0

The coefficient of the bigraded Ext Poincaré series in bidegree (n,j) is dim_k Extⁿ(X,Y{j}) below the truncation degree and zero from it on.

@[simp]

theorem TauCeti.coeff_bigradedExtPoincareSeries_negSucc {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (e : C ≌ C) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (b n : ℕ) (j : ℤ) : (bigradedExtPoincareSeries k e h b).coeff (Int.negSucc n, j) = 0

The bigraded Ext Poincaré series has no negative cohomological degrees.

theorem TauCeti.bigradedExtPoincareSeries_eq_of_le {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) {b b' : ℕ} (hb : IsGradedExtBoundedBy e X Y b) (hbb' : b ≤ b') : bigradedExtPoincareSeries k e h b' = bigradedExtPoincareSeries k e h b

Raising the truncation degree past a cohomological vanishing bound does not change the bigraded Ext Poincaré series.

theorem TauCeti.isDiagonal_bigradedExtPoincareSeries_iff {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) {b : ℕ} (hb : IsGradedExtBoundedBy e X Y b) : Bigraded.IsDiagonal (bigradedExtPoincareSeries k e h b) ↔ ∀ (n : ℕ) (j : ℤ), ↑n ≠ j → Subsingleton (GradedExt e X Y n j)

With a genuine cohomological vanishing bound, the bigraded Ext Poincaré series is diagonal exactly when every off-diagonal bigraded Ext group vanishes.

theorem TauCeti.invert_gradedExtEuler_eq_euler_bigradedExtPoincareSeries {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (e : C ≌ C) {X Y : C} (h : IsGradedEulerAdmissible k e X Y) {b : ℕ} (hb : IsGradedExtBoundedBy e X Y b) : LaurentPolynomial.invert (gradedExtEuler k e h) = Bigraded.euler (bigradedExtPoincareSeries k e ⋯ b)

The q-Euler characteristic is the Euler characteristic of the bigraded Ext Poincaré series. Applying LaurentPolynomial.invert to χ_q(X,Y) gives the Alexander-graded Euler characteristic ∑ (-1)ⁿ dim_k Extⁿ(X,Y{j}) T^j of the bigraded Ext Poincaré series, truncated at any cohomological vanishing bound.

noncomputable def TauCeti.bigradedExtPoincareMatrix {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {I : Type u_1} (S : I → C) (h : ∀ (i j : I), IsGradedExtInternallyFinite k e (S i) (S j)) (b : ℕ) : Matrix I I Bigraded.Series

The full bigraded Ext Poincaré matrix of a family, truncated below a common cohomological degree b. Its (i,j) entry records all dimensions dim_k Ext^n(S_i,S_j{p}), not only the diagonal terms n = p.

@[simp]

theorem TauCeti.bigradedExtPoincareMatrix_apply {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {I : Type u_1} (S : I → C) (h : ∀ (i j : I), IsGradedExtInternallyFinite k e (S i) (S j)) (b : ℕ) (i j : I) : bigradedExtPoincareMatrix S h b i j = bigradedExtPoincareSeries k e ⋯ b

An entry of the full bigraded Ext Poincaré matrix is the bigraded Ext Poincaré series of the corresponding pair.

theorem TauCeti.bigradedExtPoincareMatrix_eq_of_le {C : Type u} [CategoryTheory.Category.{v', u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {I : Type u_1} (S : I → C) (h : ∀ (i j : I), IsGradedExtInternallyFinite k e (S i) (S j)) {b b' : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy e (S i) (S j) b) (hbb' : b ≤ b') : bigradedExtPoincareMatrix S h b' = bigradedExtPoincareMatrix S h b

Raising the common truncation degree past a common cohomological vanishing bound does not change the full bigraded Ext Poincaré matrix.

noncomputable def TauCeti.diagonalExtPoincarePolynomial (k : Type uk) [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (M N : GradedModuleCat 𝒜) (b : ℕ) : Polynomial ℤ

The diagonal Ext Poincaré polynomial ∑ n < b, finrank_k Extⁿ(M,N{n}) tⁿ of two graded modules, truncated below the cohomological degree b. Its coefficients are Module.finrank, so they are the dimensions dim_k Extⁿ(M,N{n}) when these are finite-dimensional and 0 otherwise. It records only the diagonal bigraded pieces Ext^{n,n}(M,N); when M has a linear resolution and N is concentrated in degree zero, these are the only nonzero pieces.

theorem TauCeti.diagonalExtPoincarePolynomial_def (k : Type uk) [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (M N : GradedModuleCat 𝒜) (b : ℕ) : diagonalExtPoincarePolynomial k M N b = ∑ n ∈ Finset.range b, (Polynomial.monomial n) ↑(Module.finrank k (CategoryTheory.Abelian.Ext M (N.shiftObj ↑n) n))

The diagonal Ext Poincaré polynomial is the truncated sum of the monomials finrank_k Extⁿ(M,N{n}) tⁿ.

@[simp]

theorem TauCeti.coeff_diagonalExtPoincarePolynomial (k : Type uk) [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (M N : GradedModuleCat 𝒜) (b n : ℕ) : (diagonalExtPoincarePolynomial k M N b).coeff n = if n < b then ↑(Module.finrank k (CategoryTheory.Abelian.Ext M (N.shiftObj ↑n) n)) else 0

The coefficient of tⁿ in the diagonal Ext Poincaré polynomial is finrank_k Extⁿ(M,N{n}) (the dimension when this Ext space is finite-dimensional, 0 otherwise) below the truncation degree, and zero from it on.

theorem TauCeti.diagonalExtPoincarePolynomial_eq_of_le {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {b b' : ℕ} (hb : IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) M N b) (hbb' : b ≤ b') : diagonalExtPoincarePolynomial k M N b' = diagonalExtPoincarePolynomial k M N b

The diagonal Ext Poincaré polynomial is unchanged by raising its truncation degree past a cohomological vanishing bound.

noncomputable def TauCeti.diagonalExtPoincareMatrix (k : Type uk) [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type u_1} (S : I → GradedModuleCat 𝒜) (b : ℕ) : Matrix I I (Polynomial ℤ)

The diagonal Ext Poincaré matrix of a family S of graded modules, truncated below the cohomological degree b: its (i, j) entry is the diagonal Ext Poincaré polynomial ∑ n < b, finrank_k Extⁿ(Sᵢ, Sⱼ{n}) tⁿ, whose coefficients are Ext dimensions when these are finite-dimensional (Module.finrank convention).

@[simp]

theorem TauCeti.diagonalExtPoincareMatrix_apply (k : Type uk) [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type u_1} (S : I → GradedModuleCat 𝒜) (b : ℕ) (i j : I) : diagonalExtPoincareMatrix k S b i j = diagonalExtPoincarePolynomial k (S i) (S j) b

An entry of the diagonal Ext Poincaré matrix is the diagonal Ext Poincaré polynomial of the corresponding pair.

theorem TauCeti.diagonalExtPoincareMatrix_eq_of_le {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type u_1} {S : I → GradedModuleCat 𝒜} {b b' : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i) (S j) b) (hbb' : b ≤ b') : diagonalExtPoincareMatrix k S b' = diagonalExtPoincareMatrix k S b

The diagonal Ext Poincaré matrix is unchanged by raising its truncation degree past a common cohomological vanishing bound of all pairs in the family.