Multigraded free modules and graded free resolutions

DefinitionDegree-zero homomorphisms of multigraded modules#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) and \(N\) be multigraded \(R\)-modules with homogeneous pieces \(M_\alpha\) and \(N_\alpha\) for \(\alpha \in \mathbb{Z}^n\). An \(R\)-linear map \(f : M \to N\) is degree-zero when \(f(M_\alpha) \subseteq N_\alpha\) for every \(\alpha \in \mathbb{Z}^n\).

public def IsDegreeZero {M N : Type*} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M] [AddCommGroup N]
    [Module (MvPolynomial (Fin n) K) N] [Module K N]
    (gM : MultigradedPolynomialModule K n M)
    (gN : MultigradedPolynomialModule K n N)
    (f : M →ₗ[MvPolynomial (Fin n) K] N) : Prop :=
  ∀ (α : Fin n →₀ Int) (m : M), m ∈ gM.component α → f m ∈ gN.component α

Uses 1 · Used by 3

Statement usesMultigraded modules over a polynomial ring

Used byThe base-changed differential preserves multidegree · Existence of finite multigraded free resolutions · Multigraded free resolution

StructureMultigraded free module#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(\iota\) be an index type. A multigraded free module structure on an \(R\)-module \(F\) consists of a multigraded \(R\)-module structure on \(F\), with homogeneous pieces \(F_\alpha\) for \(\alpha \in \mathbb{Z}^n\), together with an \(R\)-basis \((b_j)_{j \in \iota}\) of \(F\) and a degree \(d_j \in \mathbb{Z}^n\) for each \(j \in \iota\) such that \(b_j \in F_{d_j}\) for every \(j \in \iota\).

public structure MultigradedFreeModule (K : Type*) [Field K] (n : ℕ)
    (F : Type*) [AddCommGroup F] [Module (MvPolynomial (Fin n) K) F]
    [Module K F] (ι : Type*) where
  /-- The underlying `ℤⁿ`-graded module structure. -/
  graded : MultigradedPolynomialModule K n F
  /-- The actual free basis over `MvPolynomial (Fin n) K`. -/
  basis : Module.Basis ι (MvPolynomial (Fin n) K) F
  /-- The prescribed homogeneous degree of each basis vector. -/
  degree : ι → (Fin n →₀ Int)
  /-- Each basis vector is homogeneous of its prescribed degree. -/
  basis_mem : ∀ (i : ι), basis i ∈ graded.component (degree i)

Uses 1 · Used by 8

Statement usesMultigraded modules over a polynomial ring

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 · Existence of finite multigraded free resolutions · Degree pieces of the base-changed resolution · Multigraded free resolution · Finite support of the multigraded Poincaré coefficients

StructureMultigraded free resolution#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, let \(\cdots \to P_1 \to P_0 \to M\) be a projective resolution of \(M\) over \(R\), and for each \(i \in \mathbb{N}\) let \(\iota_i\) be an index type. A multigraded free resolution structure on this resolution consists of a multigraded free module structure on each \(P_i\) with basis indexed by \(\iota_i\), such that every differential \(P_{i+1} \to P_i\) and the augmentation \(P_0 \to M\) are degree-zero for these gradings and the given grading of \(M\).

Each \(P_i\) is regarded as a \(K\)-vector space by restricting scalars along \(K \to R\).

MetaMathlibExt.MultigradedFreeResolution · 26 lines

public structure MultigradedFreeResolution (K : Type*) [Field K] (n : ℕ)
    (M : Type*) [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*) where
  /-- Each resolution term carries a multigraded free module structure. -/
  termFree : ∀ (i : ℕ),
    letI : Module K ↥(resolution.complex.X i) :=
      Module.compHom _ (MvPolynomial.C : K →+* MvPolynomial (Fin n) K);
    MultigradedFreeModule K n ↥(resolution.complex.X i) (ι i)
  /-- Successor differentials are degree-zero. -/
  diffDegreeZero : ∀ (i : ℕ),
    letI : Module K ↥(resolution.complex.X (i + 1)) :=
      Module.compHom _ (MvPolynomial.C : K →+* MvPolynomial (Fin n) K);
    letI : Module K ↥(resolution.complex.X i) :=
      Module.compHom _ (MvPolynomial.C : K →+* MvPolynomial (Fin n) K);
    IsDegreeZero (termFree (i + 1)).graded (termFree i).graded
      (ModuleCat.Hom.hom (resolution.complex.d (i + 1) i))
  /-- The augmentation map is degree-zero. -/
  augDegreeZero :
    letI : Module K ↥(resolution.complex.X 0) :=
      Module.compHom _ (MvPolynomial.C : K →+* MvPolynomial (Fin n) K);
    IsDegreeZero (termFree 0).graded targetGraded
      (ModuleCat.Hom.hom (resolution.π.f 0))

Uses 3 · Used by 21

Statement usesDegree-zero homomorphisms of multigraded modules · Multigraded free module · Multigraded modules over a 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 · Existence of finite multigraded free resolutions · 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 · 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

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.