Multigraded polynomial modules

DefinitionExponent vectors as integer vectors#✓fully proved

For an exponent vector \(a = (a_1, \dots, a_n) \in \mathbb{N}^n\) of a monomial, this is the vector \((a_1, \dots, a_n) \in \mathbb{Z}^n\) obtained by viewing each entry \(a_i\) as an integer.

public noncomputable def natDegreeToInt {n : ℕ} (a : Fin n →₀ ℕ) : Fin n →₀ ℤ :=
  Finsupp.mapRange (fun x : ℕ => (x : ℤ)) (by simp) a

Used by 3

Used byBase change of a homogeneous element along zero evaluation · Existence of finite multigraded free resolutions · Multigraded modules over a polynomial ring

StructureMultigraded modules over a polynomial ring#✓fully proved

Let \(K\) be a field, \(n \in \mathbb{N}\) and \(R = K[x_1, \dots, x_n]\), and let \(M\) be an \(R\)-module that is also a \(K\)-vector space. A \(\mathbb{Z}^n\)-grading of \(M\) compatible with monomial multiplication consists of \(K\)-subspaces \(M_\alpha \subseteq M\), one for each \(\alpha \in \mathbb{Z}^n\), such that \(M\) is the direct sum of the \(M_\alpha\), the action of each \(k \in K\) on \(M\) agrees with multiplication by the constant polynomial \(k \in R\), and for every \(a \in \mathbb{N}^n\), every \(c \in K\) and every \(\alpha \in \mathbb{Z}^n\), multiplication by the monomial \(c x^a = c x_1^{a_1} \cdots x_n^{a_n}\) maps \(M_\alpha\) into \(M_{\alpha + a}\), where \(a\) is viewed as an element of \(\mathbb{Z}^n\).

public structure MultigradedPolynomialModule (M : Type*) [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M] where
  /-- The homogeneous `K`-submodule in degree `α`. -/
  component : (Fin n →₀ ℤ) → Submodule K M
  /-- The homogeneous pieces decompose `M` as a direct sum. -/
  decomposition : DirectSum.Decomposition component
  /-- Scalar multiplication by `k : K` agrees with the `MvPolynomial.C k` action. -/
  smul_via_C : ∀ (k : K) (m : M), k • m = ((MvPolynomial.C k : MvPolynomial (Fin n) K)) • m
  /-- Monomials shift homogeneous degrees by the embedded exponent. -/
  monomial_mem : ∀ (a : Fin n →₀ ℕ) (c : K) (α : Fin n →₀ ℤ) (m : M),
    m ∈ component α →
      ((MvPolynomial.monomial a c : MvPolynomial (Fin n) K)) • m ∈
        component (α + natDegreeToInt a)

Uses 1 · Used by 26

Statement usesExponent vectors as integer vectors

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 · 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 · Existence of finite multigraded free resolutions · Finite homogeneous generating sets · Betti numbers agree across comparable resolutions · Multigraded resolution comparison · Betti numbers do not depend on the choice of base change data · Degree pieces of the base-changed resolution · Multigraded base change data · Multigraded Betti number · Degree-zero homomorphisms of multigraded modules · Multigraded free module · Multigraded free resolution · 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

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.