Multigraded Poincaré-series coefficient family

DefinitionMultigraded Poincaré coefficients#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, and let \(D\) be base-change data for a multigraded free resolution of \(M\). The multigraded Poincaré coefficient family of \(D\) is the function \(\mathbb{N} \times \mathbb{Z}^n \to \mathbb{N}\) sending \((i, \alpha)\) to the multigraded Betti number \(\beta_{i,\alpha}(D)\) of \(D\) in homological degree \(i\) and multidegree \(\alpha\).

A plain function records every coefficient without asserting finite support, convergence, polynomiality, or rationality.

public noncomputable def multigradedPoincareCoefficients
    {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι : ℕ → Type u}
    {res : MultigradedFreeResolution K n M targetGraded resolution ι}
    (data : MultigradedBaseChange targetGraded resolution ι res) :
    ℕ × (Fin n →₀ Int) → ℕ :=
  fun p => multigradedBettiNumber data p.2 p.1

Uses 4 · Used by 5

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded Betti number

Used byMultigraded Poincaré polynomial · Coefficients of the multigraded Poincaré polynomial · Multigraded Poincaré coefficients are Betti numbers · Resolution comparisons preserve multigraded Poincaré coefficients · Finite support of the multigraded Poincaré coefficients

TheoremMultigraded Poincaré coefficients are Betti numbers#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, and let \(D\) be base-change data for a multigraded free resolution of \(M\). For every \(i \in \mathbb{N}\) and \(\alpha \in \mathbb{Z}^n\), the multigraded Poincaré coefficient family of \(D\) takes the value \(\beta_{i,\alpha}(D)\) at \((i, \alpha)\), where \(\beta_{i,\alpha}(D)\) is the multigraded Betti number of \(D\) in homological degree \(i\) and multidegree \(\alpha\).

public theorem multigradedPoincareCoefficients_apply
    {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι : ℕ → Type u}
    {res : MultigradedFreeResolution K n M targetGraded resolution ι}
    (data : MultigradedBaseChange targetGraded resolution ι res)
    (i : ℕ) (α : Fin n →₀ Int) :
    multigradedPoincareCoefficients data (i, α) =
      multigradedBettiNumber data α i

Uses 5 · Used by 1

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded Betti number · Multigraded Poincaré coefficients

Used byCoefficients of the multigraded Poincaré polynomial

TheoremResolution comparisons preserve multigraded Poincaré coefficients#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, and let \(D\) and \(D'\) be base-change data for two multigraded free resolutions of \(M\). Given a multigraded resolution comparison between \(D\) and \(D'\), that is, for every \(\alpha \in \mathbb{Z}^n\) a chain-homotopy equivalence between the degree-\(\alpha\) component complexes of \(D\) and \(D'\), the multigraded Poincaré coefficient families of \(D\) and \(D'\) are equal.

MetaMathlibExt.multigradedPoincareCoefficients_eq_of_resolutionComparison · 15 lines

public theorem multigradedPoincareCoefficients_eq_of_resolutionComparison
    {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution₁ resolution₂ : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι₁ ι₂ : ℕ → Type u}
    {res₁ : MultigradedFreeResolution K n M targetGraded resolution₁ ι₁}
    {res₂ : MultigradedFreeResolution K n M targetGraded resolution₂ ι₂}
    {data₁ : MultigradedBaseChange targetGraded resolution₁ ι₁ res₁}
    {data₂ : MultigradedBaseChange targetGraded resolution₂ ι₂ res₂}
    (comparison : MultigradedResolutionComparison data₁ data₂) :
    multigradedPoincareCoefficients data₁ =
      multigradedPoincareCoefficients data₂

Sources

• Benjamin Braun and Brian Davis, “Antichain Simplices,” Journal of Integer Sequences 23 (2020), https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex, exact lines 870--874. This is conditional only: it assumes the comparison and claims no existence, unconditional independence, finite support, polynomiality, rationality, or convergence.

Uses 6

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded resolution comparison · Multigraded Poincaré coefficients

Proof usesBetti numbers agree across comparable resolutions

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.