feat(RingTheory/MvPolynomial): powers of ideal of variables (leanprover-community#33539)

1. Added a new file `Algebra/Group/TypeTags/Pointwise.lean` to provide more helper results about pointwise operations on sets
2. Provided more APIs for `MvPolynomial.restrictSupport` and defined `restrictSupportIdeal` to be the ideal determined by `restrictSupport R s` when `s` is an upper set
3. Defined `MvPolynomial.idealOfVars` to be the ideal spanned by all variables in `MvPolynomial` and provided results about its powers
4. Provided some relavent helper results while golfing

Author: BryceT233

Mathlib.lean

@@ -467,6 +467,7 @@ public import Mathlib.Algebra.Group.Translate
 public import Mathlib.Algebra.Group.TypeTags.Basic
 public import Mathlib.Algebra.Group.TypeTags.Finite
 public import Mathlib.Algebra.Group.TypeTags.Hom
+public import Mathlib.Algebra.Group.TypeTags.Pointwise
 public import Mathlib.Algebra.Group.ULift
 public import Mathlib.Algebra.Group.UniqueProds.Basic
 public import Mathlib.Algebra.Group.UniqueProds.VectorSpace

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -985,6 +985,13 @@ lemma image_pow [MonoidHomClass F α β] (f : F) (s : Set α) : ∀ n, f '' (s ^
   | 0 => by simp [singleton_one]
   | n + 1 => image_pow_of_ne_zero n.succ_ne_zero ..
 
+@[to_additive]
+lemma preimage_pow_subset [MonoidHomClass F α β] (f : F) (s : Set β) :
+    ∀ n, (f ⁻¹' s) ^ n ⊆ f ⁻¹' (s ^ n)
+  | 0 => by simp [Set.subset_def]
+  | n + 1 => by simpa [pow_succ] using Subset.trans (mul_subset_mul_right
+    (preimage_pow_subset f s n)) (preimage_mul_preimage_subset f)
+
 end Monoid
 
 section Group

Mathlib/Algebra/Group/TypeTags/Pointwise.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Group.Pointwise.Set.Basic
+public import Mathlib.Algebra.Group.TypeTags.Basic
+
+/-!
+# Lemmas about pointwise operations in the presence of `Multiplicative` and `Additive`.
+-/
+
+public section
+
+open Pointwise
+
+variable {M : Type*}
+
+namespace Multiplicative
+
+variable [AddMonoid M]
+
+@[simp]
+lemma ofAdd_image_setAdd (s t : Set M) :
+    ofAdd '' (s + t) = ofAdd '' s * ofAdd '' t := by
+  rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]
+
+@[simp]
+lemma ofAdd_image_nsmul (n : ℕ) (s : Set M) :
+    ofAdd '' (n • s) = (ofAdd '' s) ^ n := by
+  induction n with
+  | zero => simp; rfl
+  | succ n IH => simp [succ_nsmul, pow_succ, IH]
+
+@[simp]
+lemma toAdd_image_setMul (s t : Set (Multiplicative M)) :
+    toAdd '' (s * t) = (toAdd '' s) + (toAdd '' t) := by
+  rw [← Set.image2_mul, Set.image_image2_distrib toAdd_mul, Set.image2_add]
+
+@[simp]
+lemma toAdd_image_nsmul (n : ℕ) (s : Set (Multiplicative M)) :
+    toAdd '' (s ^ n) = n • (toAdd '' s) := by
+  induction n with
+  | zero => simp; rfl
+  | succ n IH => simp [succ_nsmul, pow_succ, IH]
+
+end Multiplicative

Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

@@ -879,4 +879,29 @@ theorem inv_Iio₀ {a : α} (ha : a < 0) : (Iio a)⁻¹ = Ioo a⁻¹ 0 := by
 
 end LinearOrderedField
 
+section CanonicallyOrdered
+
+variable {α : Type*} [Monoid α]
+variable [Preorder α] [CanonicallyOrderedMul α] [MulRightMono α]
+
+@[to_additive]
+theorem Ici_mul_Ici_eq {a b : α} :
+    Ici a * Ici b = Ici (a * b) := by
+  refine Subset.antisymm (Ici_mul_Ici_subset' ..) (subset_def ▸ fun c c_in ↦
+    mem_mul.mpr ⟨a, ⟨by simp, ?_⟩⟩)
+  obtain ⟨d, hd⟩ := exists_mul_of_le <| mem_Ici.mp c_in
+  exact ⟨b * d, by simp [← mul_assoc, hd]⟩
+
+@[to_additive]
+theorem Ici_pow_eq {a : α} :
+    ∀ n ≠ 0, Ici a ^ n = Ici (a ^ n)
+  | 1, _ => by simp
+  | n + 2, _ => by simp [pow_succ _ n.succ, Ici_pow_eq, Ici_mul_Ici_eq]
+
+omit [MulRightMono α] in
+@[to_additive]
+lemma Ici_one_eq_univ : Set.Ici (1 : α) = Set.univ := by aesop
+
+end CanonicallyOrdered
+
 end Set

Mathlib/Data/Finsupp/Weight.lean

@@ -9,6 +9,8 @@ public import Mathlib.Data.Finsupp.Antidiagonal
 public import Mathlib.Data.Finsupp.Order
 public import Mathlib.LinearAlgebra.Finsupp.LinearCombination
 
+import Mathlib.Algebra.Group.TypeTags.Pointwise
+
 /-! # weights of Finsupp functions
 
 The theory of multivariate polynomials and power series is built
@@ -261,4 +263,61 @@ lemma range_single_one :
     obtain ⟨a, rfl⟩ := (Finsupp.sum_eq_one_iff _).mp hp
     use a
 
+lemma degree_mono {R : Type*} [AddCommMonoid R] [PartialOrder R] [CanonicallyOrderedAdd R] :
+    Monotone (Finsupp.degree (σ := σ) (R := R)) :=
+  fun _ _ e ↦
+    (Finset.sum_le_sum_of_subset (support_mono e)).trans (Finset.sum_le_sum fun _ _ ↦ e _)
+
+lemma exists_le_degree_eq {σ : Type*} (f : σ →₀ ℕ) (n : ℕ) (hn : n ≤ f.degree) :
+    ∃ g ≤ f, g.degree = n := by
+  induction n with
+  | zero => simp [degree_eq_zero_iff]
+  | succ n IH =>
+    obtain ⟨g, hgf, rfl⟩ := IH (by lia)
+    obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf
+    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
+    exact ⟨g + .single i 1, add_le_add_right (by simp; grind) _, by simp⟩
+
+open scoped Pointwise in
+lemma degree_preimage_add {σ : Type*} (s t : Set ℕ) :
+    degree (σ := σ) ⁻¹' (s + t) = degree (σ := σ) ⁻¹' s + degree (σ := σ) ⁻¹' t := by
+  refine (Set.preimage_add_preimage_subset ..).antisymm' ?_
+  rintro f ⟨m, hm, n, hn, e : m + n = _⟩
+  obtain ⟨g, hgf, rfl⟩ := exists_le_degree_eq f m (by grind)
+  obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf
+  exact Set.add_mem_add hm (by simp_all)
+
+open scoped Pointwise in
+lemma degree_preimage_nsmul {σ : Type*} (s : Set ℕ) (n : ℕ) (hn : n ≠ 0) :
+    degree (σ := σ) ⁻¹' (n • s) = n • degree (σ := σ) ⁻¹' s := by
+  obtain (_ | n) := n; · contradiction
+  induction n <;> simp_all [succ_nsmul, degree_preimage_add]
+
+open scoped Pointwise in
+lemma nsmul_single_one_image {α : Type*} {n : ℕ} {s : Set α} :
+    n • (single · 1) '' s = {x : α →₀ ℕ | x.degree = n ∧ ↑x.support ⊆ s} := by
+  classical
+  induction n with
+  | zero => aesop (add simp degree_eq_zero_iff)
+  | succ n ih =>
+    rw [succ_nsmul, ih]
+    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
+    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
+    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
+    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
+      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
+    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩
+
+open scoped Pointwise in
+theorem image_pow_eq_finsuppProd_image {α β : Type*} [CommMonoid β] {f : α → β} {n} {s : Set α} :
+    (f '' s) ^ n = (·.prod (f · ^ ·)) '' {x : α →₀ ℕ | x.degree = n ∧ ↑x.support ⊆ s} := by
+  classical
+  suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
+    simp [← nsmul_single_one_image, ← this, Set.image_image]
+  intro s
+  refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
+    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
+  simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
+    Set.image_id _]
+
 end Finsupp

Mathlib/RingTheory/MvPolynomial/Basic.lean

@@ -103,6 +103,62 @@ def basisRestrictSupport (s : Set (σ →₀ ℕ)) : Basis s R (restrictSupport
 theorem restrictSupport_mono {s t : Set (σ →₀ ℕ)} (h : s ⊆ t) :
     restrictSupport R s ≤ restrictSupport R t := Finsupp.supported_mono h
 
+lemma restrictSupport_eq_span (s : Set (σ →₀ ℕ)) :
+    restrictSupport R s = .span _ ((monomial · 1) '' s) := Finsupp.supported_eq_span_single ..
+
+lemma mem_restrictSupport_iff {s : Set (σ →₀ ℕ)} {r : MvPolynomial σ R} :
+    r ∈ restrictSupport R s ↔ ↑r.support ⊆ s := .rfl
+
+@[simp]
+lemma monomial_mem_restrictSupport {s : Set (σ →₀ ℕ)} {m} {r : R} :
+    monomial m r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0 := by
+  classical
+  by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]
+
+open Pointwise in
+lemma restrictSupport_add (s t : Set (σ →₀ ℕ)) :
+    restrictSupport R (s + t) = restrictSupport R s * restrictSupport R t := by
+  apply le_antisymm
+  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff, Set.add_subset_iff]
+    intro x hx y hy
+    simp [show monomial (x + y) (1 : R) = monomial x 1 * monomial y 1 by simp, -monomial_mul,
+      *, Submodule.mul_mem_mul]
+  · rw [restrictSupport_eq_span, restrictSupport_eq_span, Submodule.span_mul_span,
+      Submodule.span_le, Set.mul_subset_iff]
+    simp +contextual [Set.add_mem_add]
+
+open Pointwise in
+@[simp] lemma restrictSupport_zero : restrictSupport R (0 : Set (σ →₀ ℕ)) = 1 := by
+  classical
+  apply le_antisymm
+  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
+    simpa using ⟨1, by simp⟩
+  · rintro _ ⟨x, rfl⟩
+    simp [mem_restrictSupport_iff, Set.subset_def, coeff_one]
+
+@[simp]
+lemma restrictSupport_univ : restrictSupport R (.univ : Set (σ →₀ ℕ)) = ⊤ := by
+  ext; simp [mem_restrictSupport_iff]
+
+open Pointwise in
+lemma restrictSupport_nsmul (n : ℕ) (s : Set (σ →₀ ℕ)) :
+    restrictSupport R (n • s) = restrictSupport R s ^ n := by
+  induction n <;> simp [add_smul, restrictSupport_add, *, pow_succ]
+
+/-- The ideal defined by `restrictSupport R s` when `s` is an upper set. -/
+def restrictSupportIdeal (s : Set (σ →₀ ℕ)) (hs : IsUpperSet s) :
+    Ideal (MvPolynomial σ R) where
+  __ := restrictSupport R s
+  smul_mem' x y hy m (hm : m ∈ (x * y).support) := by
+    classical
+    simp only [mem_support_iff, coeff_mul, ne_eq] at hm
+    obtain ⟨⟨i, j⟩, hij, e⟩ := Finset.exists_ne_zero_of_sum_ne_zero hm
+    refine hs (by simp_all [eq_comm]) (hy (show j ∈ y.support by aesop))
+
+@[simp]
+lemma restrictScalars_restrictSupportIdeal (s : Set (σ →₀ ℕ)) (hs) :
+  (restrictSupportIdeal (R := R) s hs).restrictScalars R = restrictSupport R s := by rfl
+
 variable (σ)
 
 /-- The submodule of polynomials of total degree less than or equal to `m`. -/

Mathlib/RingTheory/MvPolynomial/Ideal.lean

@@ -8,6 +8,9 @@ module
 public import Mathlib.Algebra.MonoidAlgebra.Ideal
 public import Mathlib.Algebra.MvPolynomial.Division
 public import Mathlib.RingTheory.MvPolynomial.MonomialOrder
+public import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
+import Mathlib.RingTheory.Ideal.Operations
 
 /-!
 # Lemmas about ideals of `MvPolynomial`
@@ -18,6 +21,7 @@ Notably this contains results about monomial ideals.
 
 * `MvPolynomial.mem_ideal_span_monomial_image`
 * `MvPolynomial.mem_ideal_span_X_image`
+* `MvPolynomial.mem_pow_idealOfVars_iff`
 -/
 
 public section
@@ -54,6 +58,65 @@ theorem mem_ideal_span_X_image {x : MvPolynomial σ R} {s : Set σ} :
   refine this.trans ?_
   simp [Nat.one_le_iff_ne_zero]
 
+section idealOfVars
+
+open Finset Finsupp
+
+variable (σ R) in
+/-- The ideal spanned by all variables. -/
+def idealOfVars : Ideal (MvPolynomial σ R) := .span (.range X)
+
+lemma idealOfVars_eq_restrictSupportIdeal :
+    idealOfVars σ R = restrictSupportIdeal _ _ ((isUpperSet_Ici 1).preimage degree_mono) := by
+  apply le_antisymm
+  · simp [idealOfVars, Ideal.span_le, Set.range_subset_iff, restrictSupportIdeal, X]
+  · simp only [SetLike.le_def, restrictSupportIdeal, Submodule.mem_mk, Submodule.mem_toAddSubmonoid,
+      ← Submodule.restrictScalars_mem R (idealOfVars σ R)]
+    rw [← SetLike.le_def, restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
+    intro x hx
+    obtain ⟨i, hi⟩ : x.support.Nonempty := by aesop
+    obtain ⟨c, rfl⟩ := le_iff_exists_add'.mp (show single i 1 ≤ x by simp_all; lia)
+    simpa [monomial_add_single] using Ideal.mul_mem_left _ _ (Ideal.subset_span (by simp))
+
+open Pointwise in
+theorem pow_idealOfVars (n : ℕ) :
+    idealOfVars σ R ^ n = restrictSupportIdeal _ _ ((isUpperSet_Ici n).preimage degree_mono) := by
+  rw [idealOfVars_eq_restrictSupportIdeal]
+  apply Submodule.restrictScalars_injective R
+  by_cases hn : n = 0
+  · simp [hn, Set.Ici_zero_eq_univ]
+  rw [Submodule.restrictScalars_pow hn]
+  refine (restrictSupport_nsmul ..).symm.trans (congr_arg (restrictSupport R) ?_)
+  simp [← degree_preimage_nsmul, hn, Set.Ici_nsmul_eq]
+
+/-- The `n`th power of `idealOfVars` is spanned by all monic monomials of total degree `n`. -/
+theorem pow_idealOfVars_eq_span (n) : idealOfVars σ R ^ n =
+    .span ((monomial · 1) '' (degree ⁻¹' {n})) := by
+  rw [idealOfVars, Ideal.span, Submodule.span_pow, ← Set.image_univ,
+    image_pow_eq_finsuppProd_image]
+  simp [monomial_eq, Set.preimage, degree]
+
+theorem mem_pow_idealOfVars_iff (n : ℕ) (p : MvPolynomial σ R) :
+    p ∈ idealOfVars σ R ^ n ↔ ∀ x ∈ p.support, n ≤ degree x := by
+  rw [pow_idealOfVars]
+  simp [restrictSupportIdeal, mem_restrictSupport_iff, Set.subset_def]
+
+theorem mem_pow_idealOfVars_iff' (n : ℕ) (p : MvPolynomial σ R) :
+    p ∈ idealOfVars σ R ^ n ↔ ∀ x, degree x < n → p.coeff x = 0 := by
+  grind only [mem_pow_idealOfVars_iff, mem_support_iff]
+
+theorem monomial_mem_pow_idealOfVars_iff (n : ℕ) (x : σ →₀ ℕ) {r : R} (h : r ≠ 0) :
+    monomial x r ∈ idealOfVars σ R ^ n ↔ n ≤ degree x := by
+  classical
+  grind only [mem_pow_idealOfVars_iff, mem_support_iff, coeff_monomial]
+
+theorem C_mem_pow_idealOfVars_iff (n r) : C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0 := by
+  by_cases h : r = 0
+  · simp [h]
+  simpa [h] using monomial_mem_pow_idealOfVars_iff (σ := σ) n 0 h
+
+end idealOfVars
+
 end MvPolynomial
 
 namespace MonomialOrder