Ideal of MvPolynomial of high degree

Stream: maths

[Jireh Loreaux]

The following is a Submodule R (MvPolynomial σ R), but I claim it is actually an Ideal (MvPolynomial σ R). What's the easiest proof? (In fact, I also claim that it is equal to Ideal.span {(X i) ^ n | (i : σ)})

import Mathlib

variable (σ R : Type*) [CommRing R]

/-- The `R`-submodule spanned by monomials where one of the variables has multiplicity at least `n`. -/
def MvPolynomial.exceedDegree (n : ℕ) : Submodule R (MvPolynomial σ R) :=
  restrictSupport R {f : σ →₀ ℕ | ∃ i, n < f i}

My algebra-fu is weak apparently.

[Andrew Yang]

Does this help?

import Mathlib.RingTheory.MvPolynomial.Basic
import Mathlib.RingTheory.MvPolynomial.Ideal

open MvPolynomial

example (σ R : Type*) [CommRing R] (n : ℕ) :
    restrictSupport R {f : σ →₀ ℕ | ∃ i, n < f i} =
      (Ideal.span ((monomial · (1 : R)) '' {f : σ →₀ ℕ | ∃ i, n < f i})).restrictScalars R := by
  ext a
  rw [restrictSupport, Finsupp.mem_supported, ← MvPolynomial.support]
  simp only [Submodule.restrictScalars_mem, mem_ideal_span_monomial_image, Set.subset_def]
  congr! with f _
  exact ⟨fun ⟨i, hi⟩ ↦ ⟨f, ⟨i, hi⟩, le_rfl⟩, fun ⟨g, ⟨i, hi⟩, h⟩ ↦ ⟨i, hi.trans_le (h i)⟩⟩

[Andrew Yang]

The key is probably docs#MvPolynomial.mem_ideal_span_monomial_image

[Andrew Yang]

Or maybe

example (σ R : Type*) [CommRing R] (n : ℕ) :
    restrictSupport R {f : σ →₀ ℕ | ∃ i, n ≤ f i} =
      (Ideal.span {(X i) ^ n | (i : σ)}).restrictScalars R := by
  trans (Ideal.span ((monomial · (1 : R)) '' {Finsupp.single i n | (i : σ)})).restrictScalars R
  · ext a
    rw [restrictSupport, Finsupp.mem_supported, ← MvPolynomial.support]
    simp only [Set.subset_def, Submodule.restrictScalars_mem, mem_ideal_span_monomial_image]
    simp
  · congr
    ext
    simp [X_pow_eq_monomial]

(Note that the LHS is now ≤ and not <)

[Jireh Loreaux]

Thanks! I'll have a look.

[Jireh Loreaux]

Ah indeed, the < was a typo.

[Jireh Loreaux]

@Jack Knittle you will be interested in the above.