Powers of `Ideal.span`

Stream: Is there code for X?

[Christian Merten]

I need an explicit description of the elements of the power of an ideal I : Ideal R spanned by a S : Set R. Ideally this formulation:

import Mathlib

variable {R : Type*} [CommRing R]

lemma Ideal.mem_span_pow {n : ℕ} (S : Set R) (x : R) :
    x ∈ (Ideal.span S) ^ n ↔ ∃ (p : MvPolynomial S R),
    MvPolynomial.IsHomogeneous p n ∧ MvPolynomial.eval Subtype.val p = x :=
  sorry

Is there something towards this? The forward direction is rather straightforward using induction on n and docs#Submodule.span_induction, the backwards direction seems to be worse.

[Andrew Yang]

import Mathlib

variable {R : Type*} [CommRing R]

lemma Ideal.mem_span_pow {n : ℕ} (S : Set R) (x : R) :
    x ∈ (Ideal.span S) ^ n ↔ ∃ (p : MvPolynomial S R),
    MvPolynomial.IsHomogeneous p n ∧ MvPolynomial.eval Subtype.val p = x := by
  constructor
  · sorry
  · rintro ⟨p, hp, rfl⟩
    rw [← p.sum_single, map_finsupp_sum, Finsupp.sum]
    apply sum_mem
    rintro c hc
    simp only [MvPolynomial.single_eq_monomial, MvPolynomial.eval_monomial]
    apply mul_mem_left
    rw [← @hp c (by simpa using hc), MvPolynomial.weightedDegree_one,
      MvPolynomial.degree, ← Finset.prod_pow_eq_pow_sum, Finsupp.prod]
    apply Ideal.prod_mem_prod
    exact fun x _ ↦ Ideal.pow_mem_pow (subset_span x.2) _

[Christian Merten]

Thanks a lot! I derailed at the goal state (Finsupp.prod c fun n e ↦ ↑n ^ e) ∈ Ideal.span S ^ n which I eventually could prove by induction on n, but your solution is way shorter.