Multigraded Betti numbers after residue-field base change

DefinitionAugmentation of the polynomial ring#✓fully proved

For a field \(K\) and \(n \in \mathbb{N}\), the augmentation \(K[x_1, \dots, x_n] \to K\) is the ring homomorphism sending each polynomial \(p\) to its value \(p(0, \dots, 0)\): it is the identity on constants and sends every variable to \(0\).

public noncomputable def zeroEval {K : Type u} [Field K] {n : ℕ} :
    MvPolynomial (Fin n) K →+* K :=
  MvPolynomial.eval₂Hom (RingHom.id K) (0 : Fin n → K)

Used by 7

Used byBase change of a homogeneous element along zero evaluation · Multidegree decomposition of the base-changed resolution · Finite bases give finite-dimensional multidegree pieces · The base-changed differential preserves multidegree · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution · Finite support of the multigraded Poincaré coefficients

DefinitionBase change of a resolution to the residue field#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) be an \(R\)-module. Given a projective resolution \(P_\bullet \to M\) over \(R\), its base change is the chain complex of \(K\)-vector spaces \(K \otimes_R P_\bullet\), indexed by \(\mathbb{N}\) with differentials lowering the index, obtained by extending scalars termwise along the augmentation \(R \to K\) that sends every variable to \(0\): its \(i\)th term is \(K \otimes_R P_i\) and its differentials are the maps \(\mathrm{id}_K \otimes d\) for the differentials \(d\) of \(P_\bullet\).

public noncomputable def baseChangedComplex {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    (resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)) :
    HomologicalComplex (ModuleCat.{u, u} K) (ComplexShape.down ℕ) :=
  letI : Algebra (MvPolynomial (Fin n) K) K := zeroEval.toAlgebra
  (CategoryTheory.Functor.mapHomologicalComplex
    (ModuleCat.extendScalars zeroEval) (ComplexShape.down ℕ)).obj resolution.complex

Uses 1 · Used by 12

Statement usesAugmentation of the polynomial ring

Used byMultidegree decomposition of the base-changed resolution · Finite bases give finite-dimensional multidegree pieces · The base-changed differential preserves multidegree · Multidegree component complex of the base-changed resolution · Inclusion of a multidegree component complex · Injectivity of the base-changed degree inclusion · Existence of multigraded base-change data · Range of the base-changed degree inclusion · Betti numbers do not depend on the choice of base change data · Degree pieces of the base-changed resolution · Multigraded base change data · Finite support of the multigraded Poincaré coefficients

DefinitionDegree pieces of the base-changed resolution#✓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 a multigraded free resolution \(P_\bullet \to M\), in which each \(P_i\) has an \(R\)-basis \((e_j)_{j \in J_i}\) with \(e_j\) homogeneous of degree \(\deg e_j \in \mathbb{Z}^n\). For \(i \in \mathbb{N}\) and \(\alpha \in \mathbb{Z}^n\), the degree-\(\alpha\) piece of the \(i\)th term \(K \otimes_R P_i\) of the base-changed complex is the \(K\)-subspace spanned by the vectors \(1 \otimes e_j\) with \(j \in J_i\) and \(\deg e_j = \alpha\).

MetaMathlibExt.baseChangedDegreePiece · 16 lines

public noncomputable def baseChangedDegreePiece {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 ι)
    (i : ℕ) (α : Fin n →₀ Int) :
    Submodule K ↥((baseChangedComplex resolution).X i) :=
  letI : Module K ↥(resolution.complex.X i) :=
    Module.compHom _ (MvPolynomial.C : K →+* MvPolynomial (Fin n) K)
  letI : Algebra (MvPolynomial (Fin n) K) K := zeroEval.toAlgebra
  Submodule.span K
    { y | ∃ j : ι i, (res.termFree i).degree j = α ∧
      y = (res.termFree i).basis.baseChange K j }

Uses 5 · Used by 11

Statement usesMultigraded free module · Multigraded free resolution · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Augmentation of the polynomial ring

Used byMultidegree decomposition of the base-changed resolution · Finite bases give finite-dimensional multidegree pieces · The base-changed differential preserves multidegree · Multidegree component complex of the base-changed resolution · Inclusion of a multidegree component complex · Injectivity of the base-changed degree inclusion · Existence of multigraded base-change data · Range of the base-changed degree inclusion · Betti numbers do not depend on the choice of base change data · Multigraded base change data · Finite support of the multigraded Poincaré coefficients

StructureMultigraded base change data#✓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 a multigraded free resolution \(P_\bullet \to M\). Write \(K \otimes_R P_\bullet\) for its base change along the augmentation \(R \to K\) and \((K \otimes_R P_i)_\beta\) for the degree-\(\beta\) piece of its \(i\)th term. Multigraded base change data for \(P_\bullet\) consist of: for each \(i \in \mathbb{N}\), a decomposition of \(K \otimes_R P_i\) as the internal direct sum of the pieces \((K \otimes_R P_i)_\beta\) over \(\beta \in \mathbb{Z}^n\), such that for all \(i\) and \(\beta\) the differential \(K \otimes_R P_{i+1} \to K \otimes_R P_i\) maps \((K \otimes_R P_{i+1})_\beta\) into \((K \otimes_R P_i)_\beta\); and, for each \(\alpha \in \mathbb{Z}^n\), an \(\mathbb{N}\)-indexed chain complex \(C^\alpha\) of \(K\)-vector spaces with a chain map \(C^\alpha \to K \otimes_R P_\bullet\) whose \(i\)th component is injective with image \((K \otimes_R P_i)_\alpha\) for every \(i\), such that every homology \(H_i(C^\alpha)\) exists and is finite-dimensional over \(K\).

MetaMathlibExt.MultigradedBaseChange · 38 lines

public structure MultigradedBaseChange {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 ι) where
  /-- Direct-sum decomposition of each base-changed term over the degree pieces. -/
  decomposition : ∀ (i : ℕ), DirectSum.Decomposition
    (fun β => baseChangedDegreePiece targetGraded resolution ι res i β)
  /-- Successor differentials preserve each degree piece. -/
  diffPreserves : ∀ (i : ℕ) (β : Fin n →₀ Int)
    (x : ↥((baseChangedComplex resolution).X (i + 1))),
    x ∈ baseChangedDegreePiece targetGraded resolution ι res (i + 1) β →
      (ModuleCat.Hom.hom ((baseChangedComplex resolution).d (i + 1) i)) x ∈
        baseChangedDegreePiece targetGraded resolution ι res i β
  /-- Component complex for a fixed multidegree `α`. -/
  comp : (α : Fin n →₀ Int) →
    HomologicalComplex (ModuleCat.{u, u} K) (ComplexShape.down ℕ)
  /-- Inclusion of the `α` component complex into the base-changed complex. -/
  incl : ∀ (α : Fin n →₀ Int), HomologicalComplex.Hom (comp α)
    (baseChangedComplex resolution)
  /-- Each inclusion map is injective. -/
  incl_injective :
    ∀ (α : Fin n →₀ Int) (i : ℕ),
      Function.Injective ⇑(ModuleCat.Hom.hom ((incl α).f i))
  /-- The range of each inclusion is exactly the corresponding degree piece. -/
  range_eq : ∀ (α : Fin n →₀ Int) (i : ℕ),
    LinearMap.range (ModuleCat.Hom.hom ((incl α).f i)) =
      baseChangedDegreePiece targetGraded resolution ι res i α
  /-- Each component complex has homology at every index. -/
  hasHom : ∀ (α : Fin n →₀ Int) (i : ℕ),
    HomologicalComplex.HasHomology (comp α) i
  /-- Each component homology is finite-dimensional over `K`. -/
  finiteDim : ∀ (α : Fin n →₀ Int) (i : ℕ)
    [HomologicalComplex.HasHomology (comp α) i],
    Module.Finite K ↥(HomologicalComplex.homology (comp α) i)

Uses 4 · Used by 11

Statement usesMultigraded free resolution · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution

Used byExistence of multigraded base-change data · Betti numbers agree across comparable resolutions · Multigraded resolution comparison · Betti numbers do not depend on the choice of base change data · Multigraded Betti number · Multigraded Poincaré polynomial · Coefficients of the multigraded Poincaré polynomial · Multigraded Poincaré coefficients · Multigraded Poincaré coefficients are Betti numbers · Resolution comparisons preserve multigraded Poincaré coefficients · Finite support of the multigraded Poincaré coefficients

DefinitionMultigraded Betti number#✓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 a multigraded free resolution \(P_\bullet \to M\). Fix multigraded base change data for \(P_\bullet\); for each \(\alpha \in \mathbb{Z}^n\) they supply a chain complex \(C^\alpha\) of \(K\)-vector spaces embedded in the base-changed complex \(K \otimes_R P_\bullet\) with image its degree-\(\alpha\) pieces. For \(\alpha \in \mathbb{Z}^n\) and \(i \in \mathbb{N}\), the multigraded Betti number of \(M\) in multidegree \(\alpha\) and homological index \(i\), with respect to these data, is the dimension over \(K\) of the homology \(H_i(C^\alpha)\).

public noncomputable def multigradedBettiNumber {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) (i : ℕ) : ℕ :=
  haveI := data.hasHom α i
  haveI := data.finiteDim α i
  Module.finrank K ↥(HomologicalComplex.homology (data.comp α) i)

Uses 3 · Used by 6

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

Used byBetti numbers agree across comparable resolutions · Betti numbers do not depend on the choice of base change data · Coefficients of the multigraded Poincaré polynomial · Multigraded Poincaré coefficients · Multigraded Poincaré coefficients are Betti numbers · Finite support of the multigraded Poincaré coefficients

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.