Invariance of multigraded Betti numbers across graded free resolutions

StructureMultigraded resolution comparison#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) be a \(\mathbb{Z}^n\)-graded \(R\)-module with two multigraded free resolutions, each equipped with multigraded base change data, whose degree-\(\alpha\) component complexes are \(C^\alpha\) and \(D^\alpha\) for \(\alpha \in \mathbb{Z}^n\). A comparison between the two base change data is a choice, for every \(\alpha \in \mathbb{Z}^n\), of a chain-homotopy equivalence between \(C^\alpha\) and \(D^\alpha\).

A homotopy equivalence, rather than a bare quasi-isomorphism, is the comparison-theorem input: it induces an isomorphism on homology. Existence and uniqueness of such a comparison are not claimed here.

public structure MultigradedResolutionComparison
    {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₂) where
  /-- Chain-homotopy equivalence between the degree-`α` component complexes. -/
  componentHomotopyEquiv : ∀ α, HomotopyEquiv (data₁.comp α) (data₂.comp α)

Uses 3 · Used by 2

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

Used byBetti numbers agree across comparable resolutions · Resolution comparisons preserve multigraded Poincaré coefficients

TheoremBetti numbers agree across comparable resolutions#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) be a \(\mathbb{Z}^n\)-graded \(R\)-module with two multigraded free resolutions, each equipped with multigraded base change data, whose degree-\(\alpha\) component complexes are \(C^\alpha\) and \(D^\alpha\) for \(\alpha \in \mathbb{Z}^n\). If the two are related by a multigraded resolution comparison, that is, for every \(\alpha\) a chain-homotopy equivalence between \(C^\alpha\) and \(D^\alpha\), then the multigraded Betti numbers defined by the two base change data agree in every multidegree \(\alpha \in \mathbb{Z}^n\) and every homological index \(i \in \mathbb{N}\).

MetaMathlibExt.multigradedBettiNumber_eq_of_resolutionComparison · 15 lines

public theorem multigradedBettiNumber_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₂)
    (α : Fin n →₀ Int) (i : ℕ) :
    multigradedBettiNumber data₁ α i = multigradedBettiNumber data₂ α i

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 866--874. This is conditional only: it assumes the comparison and claims no existence, uniqueness, minimality, finite support, Poincaré polynomiality or rationality, or Hilbert syzygy.

Uses 5 · Used by 1

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

Used byResolution comparisons preserve multigraded Poincaré coefficients

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.