Degree components of the base-changed multigraded resolution

DefinitionMultidegree component complex of the base-changed resolution#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded polynomial module over \(R\), and let \(F\) be a multigraded free resolution of \(M\) whose term \(F_i\) has the homogeneous basis \((e_j)_{j \in \iota_i}\). Write \(K \otimes_R F\) for the chain complex of \(K\)-vector spaces obtained from \(F\) by extending scalars along the evaluation \(R \to K\) at \(x = 0\), and for \(\alpha \in \mathbb{Z}^n\) call the \(K\)-span of the vectors \(1 \otimes e_j\) with \(e_j\) of degree \(\alpha\) the degree-\(\alpha\) piece of \((K \otimes_R F)_i\). The degree-\(\alpha\) complex is the chain complex of \(K\)-vector spaces whose term in homological degree \(i\) is the degree-\(\alpha\) piece of \((K \otimes_R F)_i\) and whose differentials are the restrictions of the differentials of \(K \otimes_R F\).

MetaMathlibExt.MultigradedFreeResolution.baseChangedDegreeComplex · 30 lines 
public noncomputable def MultigradedFreeResolution.baseChangedDegreeComplex
    (K : Type u) [Field K] (n : Nat) (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))
    (ι : Nat → Type u)
    (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (α : Fin n →₀ Int) :
    HomologicalComplex (ModuleCat.{u} K) (ComplexShape.down Nat) :=
  ChainComplex.of
    (fun i => ModuleCat.of K
      ↥(baseChangedDegreePiece (K := K) (n := n) (M := M) targetGraded
        resolution ι res i α))
    (fun i => ModuleCat.ofHom (LinearMap.restrict
      (ModuleCat.Hom.hom ((baseChangedComplex resolution).d (i + 1) i))
      (fun x hx =>
        MultigradedFreeResolution.baseChangedDifferential_preservesDegree
          targetGraded resolution ι res i α x hx)))
    (fun n => by
      apply ModuleCat.hom_ext
      apply LinearMap.ext
      intro x
      apply Subtype.ext
      have hbase := (baseChangedComplex resolution).d_comp_d (n + 1 + 1) (n + 1) n
      have hhom : ((baseChangedComplex resolution).d (n + 1) n).hom.comp
          ((baseChangedComplex resolution).d (n + 1 + 1) (n + 1)).hom = 0 := by
        rw [← ModuleCat.hom_comp, hbase, ModuleCat.hom_zero]
      have happ := LinearMap.congr_fun hhom ↑x
      simpa using happ)
Sources
Uses 5 · Used by 4
Statement usesMultigraded free resolution · The base-changed differential preserves multidegree · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution
Used byInclusion 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

DefinitionInclusion of a multidegree component complex#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded polynomial module over \(R\), and let \(F\) be a multigraded free resolution of \(M\) whose term \(F_i\) has the homogeneous basis \((e_j)_{j \in \iota_i}\). Write \(K \otimes_R F\) for the chain complex of \(K\)-vector spaces obtained from \(F\) by extending scalars along the evaluation \(R \to K\) at \(x = 0\), and for \(\alpha \in \mathbb{Z}^n\) call the \(K\)-span of the vectors \(1 \otimes e_j\) with \(e_j\) of degree \(\alpha\) the degree-\(\alpha\) piece of \((K \otimes_R F)_i\). The inclusion of the degree-\(\alpha\) complex is the chain map from the degree-\(\alpha\) complex of \(K \otimes_R F\) to \(K \otimes_R F\) whose component in each homological degree \(i\) is the inclusion of the degree-\(\alpha\) piece of \((K \otimes_R F)_i\) into \((K \otimes_R F)_i\).

MetaMathlibExt.MultigradedFreeResolution.baseChangedDegreeInclusion · 31 lines 
public noncomputable def MultigradedFreeResolution.baseChangedDegreeInclusion
    (K : Type u) [Field K] (n : Nat) (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))
    (ι : Nat → Type u)
    (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (α : Fin n →₀ Int) :
    HomologicalComplex.Hom
      (MultigradedFreeResolution.baseChangedDegreeComplex K n M
        targetGraded resolution ι res α)
      (baseChangedComplex (K := K) (n := n) (M := M) resolution) :=
  ChainComplex.ofHom
    (fun i => by
      letI := ModuleCat.isAddCommGroup ((baseChangedComplex resolution).X i)
      letI := ModuleCat.isModule ((baseChangedComplex resolution).X i)
      exact (ModuleCat.ofHom (Submodule.subtype
        (baseChangedDegreePiece (K := K) (n := n) (M := M) targetGraded
          resolution ι res i α)) :
        ModuleCat.of K
          ↥(baseChangedDegreePiece (K := K) (n := n) (M := M) targetGraded
            resolution ι res i α) ⟶
          ModuleCat.of K ↥((baseChangedComplex resolution).X i)))
    (fun i => by
      simp only [MultigradedFreeResolution.baseChangedDegreeComplex,
        ChainComplex.of_d]
      apply ModuleCat.hom_ext
      apply LinearMap.ext
      intro x
      simp)
Sources
Uses 6 · Used by 3
Statement usesMultigraded free resolution · Multidegree component complex of the base-changed resolution · The base-changed differential preserves multidegree · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution
Used byInjectivity of the base-changed degree inclusion · Existence of multigraded base-change data · Range of the base-changed degree inclusion

TheoremInjectivity of the base-changed degree inclusion#✓fully proved

Each component of the degree inclusion is injective. Source: Benjamin Braun and Brian Davis, "Antichain Simplices," Journal of Integer Sequences 23 (2020), lines 864–867, https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex.

public theorem
    MultigradedFreeResolution.baseChangedDegreeInclusion_injective
    (K : Type u) [Field K] (n : Nat) (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))
    (ι : Nat → Type u)
    (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (α : Fin n →₀ Int) (i : Nat) :
    Function.Injective ⇑(ModuleCat.Hom.hom
      ((MultigradedFreeResolution.baseChangedDegreeInclusion K n M
        targetGraded resolution ι res α).f i))
Uses 6 · Used by 1
Statement usesMultigraded free resolution · Multidegree component complex of the base-changed resolution · Inclusion of a multidegree component complex · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field
Proof usesDegree pieces of the base-changed resolution
Used byExistence of multigraded base-change data

TheoremRange of the base-changed degree inclusion#✓fully proved

Each component of the degree inclusion has range exactly the degree piece baseChangedDegreePiece. Source: Benjamin Braun and Brian Davis, "Antichain Simplices," Journal of Integer Sequences 23 (2020), lines 864–867, https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex.

MetaMathlibExt.MultigradedFreeResolution.baseChangedDegreeInclusion_range · 15 lines 
public theorem
    MultigradedFreeResolution.baseChangedDegreeInclusion_range
    (K : Type u) [Field K] (n : Nat) (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))
    (ι : Nat → Type u)
    (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (α : Fin n →₀ Int) (i : Nat) :
    LinearMap.range (ModuleCat.Hom.hom
      ((MultigradedFreeResolution.baseChangedDegreeInclusion K n M
        targetGraded resolution ι res α).f i)) =
      baseChangedDegreePiece (K := K) (n := n) (M := M)
        targetGraded resolution ι res i α
Uses 6 · Used by 1
Statement usesMultigraded free resolution · Multidegree component complex of the base-changed resolution · Inclusion of a multidegree component complex · 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

TheoremExistence of multigraded base-change data#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded polynomial module over \(R\), and let \(F\) be a multigraded free resolution of \(M\) whose term \(F_i\) has the homogeneous basis \((e_j)_{j \in \iota_i}\), where every index set \(\iota_i\) is finite. Write \(K \otimes_R F\) for the chain complex of \(K\)-vector spaces obtained from \(F\) by extending scalars along the evaluation \(R \to K\) at \(x = 0\), and for \(\alpha \in \mathbb{Z}^n\) call the \(K\)-span of the vectors \(1 \otimes e_j\) with \(e_j\) of degree \(\alpha\) the degree-\(\alpha\) piece of \((K \otimes_R F)_i\). Then multigraded base-change data for \(F\) exist: each \((K \otimes_R F)_i\) is the direct sum of its degree-\(\alpha\) pieces over \(\alpha \in \mathbb{Z}^n\), the differentials of \(K \otimes_R F\) preserve these pieces, and for every \(\alpha\) there is a chain complex \(C^\alpha\) of \(K\)-vector spaces with finite-dimensional homology in every degree, together with a chain map \(C^\alpha \to K \otimes_R F\) that is injective in each homological degree \(i\) with image the degree-\(\alpha\) piece of \((K \otimes_R F)_i\).

public theorem MultigradedFreeResolution.multigradedBaseChange_nonempty
    {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 ι)
    (finiteBasis : ∀ i, Finite (ι i)) :
    Nonempty (MultigradedBaseChange targetGraded resolution ι res)
Sources
Uses 12
Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring
Proof usesMultidegree component complex of the base-changed resolution · Multidegree decomposition of the base-changed resolution · Inclusion of a multidegree component complex · Injectivity of the base-changed degree inclusion · Range of the base-changed degree inclusion · 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
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.