refactor(Data/Finsupp/Weight): generalize and add lemmas (#20635)

This consists on easy generalizations and lemmas relative to the weight of finsupp functions,
that will be used in the formalization of Alon's combinatorial Nullstellensatz #20495




Co-authored-by: Eric Wieser <[email protected]>

Mathlib/Data/Finsupp/Weight.lean

@@ -18,91 +18,102 @@ require to classify these exponents according to their total sum
 
 ## Weight
 
-We fix a type `σ` and an `AddCommMonoid M`, as well as a function `w : σ → M`.
+We fix a type `σ`, a semiring `R`, an `R`-module `M`,
+as well as a function `w : σ → M`. (The important case is `R = ℕ`.)
 
-- `Finsupp.weight` of a finitely supported function `f : σ →₀ ℕ`
-with respect to `w`: it is the sum `∑ (f i) • (w i)`.
-It is an `AddMonoidHom` map defined using `Finsupp.linearCombination`.
+- `Finsupp.weight` of a finitely supported function `f : σ →₀ R`
+  with respect to `w`: it is the sum `∑ (f i) • (w i)`.
+  It is an `AddMonoidHom` map defined using `Finsupp.linearCombination`.
 
 - `Finsupp.le_weight` says that `f s ≤ f.weight w` when `M = ℕ`
 
 - `Finsupp.le_weight_of_ne_zero` says that `w s ≤ f.weight w`
-for `OrderedAddCommMonoid M`, when `f s ≠ 0` and all `w i` are nonnegative.
+  for `OrderedAddCommMonoid M`, when `f s ≠ 0` and all `w i` are nonnegative.
 
 - `Finsupp.le_weight_of_ne_zero'` is the same statement for `CanonicallyOrderedAddCommMonoid M`.
 
 - `NonTorsionWeight`: all values `w s` are non torsion in `M`.
 
 - `Finsupp.weight_eq_zero_iff_eq_zero` says that `f.weight w = 0` iff
-`f = 0` for `NonTorsionWeight w` and `CanonicallyOrderedAddCommMonoid M`.
+  `f = 0` for `NonTorsionWeight w` and `CanonicallyOrderedAddCommMonoid M`.
 
 - For `w : σ → ℕ` and `Finite σ`, `Finsupp.finite_of_nat_weight_le` proves that
-there are finitely many `f : σ →₀ ℕ` of bounded weight.
+  there are finitely many `f : σ →₀ ℕ` of bounded weight.
 
 ## Degree
 
-- `Finsupp.degree`:  the weight when all components of `w` are equal to `1 : ℕ`.
-The present choice is to have it defined as a plain function.
+- `Finsupp.degree f` is the sum of all `f s`, for `s ∈ f.support`.
+  The present choice is to have it defined as a plain function.
 
 - `Finsupp.degree_eq_zero_iff` says that `f.degree = 0` iff `f = 0`.
 
 - `Finsupp.le_degree` says that `f s ≤ f.degree`.
 
-- `Finsupp.degree_eq_weight_one` says `f.degree = f.weight 1`.
-This is useful to access the additivity properties of `Finsupp.degree`
+- `Finsupp.degree_eq_weight_one` says `f.degree = f.weight 1` when `R` is a semiring.
+  This is useful to access the additivity properties of `Finsupp.degree`
 
 - For `Finite σ`, `Finsupp.finite_of_degree_le` proves that
-there are finitely many `f : σ →₀ ℕ` of bounded degree.
-
+  there are finitely many `f : σ →₀ ℕ` of bounded degree.
 
 
 ## TODO
 
-* The relevant generality of these constructions is not clear.
-It could probably be generalized to `w : σ → M` and `f : σ →₀ N`,
-provided `N` is a commutative semiring and `M`is an `N`-module.
-
 * Maybe `Finsupp.weight w` and `Finsupp.degree` should have similar types,
-both `AddCommMonoidHom` or both functions.
+  both `AddMonoidHom` or both functions.
 
 -/
 
-variable {σ M : Type*} (w : σ → M)
+variable {σ M R : Type*} [Semiring R] (w : σ → M)
 
 namespace Finsupp
 
 section AddCommMonoid
 
-variable [AddCommMonoid M]
-/-- The `weight` of the finitely supported function `f : σ →₀ ℕ`
+variable [AddCommMonoid M] [Module R M]
+/-- The `weight` of the finitely supported function `f : σ →₀ R`
 with respect to `w : σ → M` is the sum `∑ i, f i • w i`. -/
-noncomputable def weight : (σ →₀ ℕ) →+ M :=
-  (Finsupp.linearCombination ℕ w).toAddMonoidHom
+noncomputable def weight : (σ →₀ R) →+ M :=
+  (Finsupp.linearCombination R w).toAddMonoidHom
 
 @[deprecated weight (since := "2024-07-20")]
 alias _root_.MvPolynomial.weightedDegree := weight
 
-theorem weight_apply (f : σ →₀ ℕ) :
+theorem weight_apply (f : σ →₀ R) :
     weight w f = Finsupp.sum f (fun i c => c • w i) := rfl
 
 @[deprecated weight_apply (since := "2024-07-20")]
 alias _root_.MvPolynomial.weightedDegree_apply := weight_apply
 
+theorem weight_single_index [DecidableEq σ] (s : σ) (c : M) (f : σ →₀ R) :
+    weight (Pi.single s c) f = f s • c :=
+  linearCombination_single_index σ M R c s f
+
+theorem weight_single_one_apply [DecidableEq σ] (s : σ) (f : σ →₀ R) :
+    weight (Pi.single s 1) f = f s := by
+  rw [weight_single_index, smul_eq_mul, mul_one]
+
+theorem weight_single (s : σ) (r : R) :
+    weight w (Finsupp.single s r) = r • w s :=
+  Finsupp.linearCombination_single _ _ _
+
+variable (R) in
 /-- A weight function is nontorsion if its values are not torsion. -/
 class NonTorsionWeight (w : σ → M) : Prop where
-  eq_zero_of_smul_eq_zero {n : ℕ} {s : σ} (h : n • w s = 0)  : n = 0
+  eq_zero_of_smul_eq_zero {r : R} {s : σ} (h : r • w s = 0) : r = 0
 
+variable (R) in
 /-- Without zero divisors, nonzero weight is a `NonTorsionWeight` -/
-theorem nonTorsionWeight_of [NoZeroSMulDivisors ℕ M] (hw : ∀ i : σ, w i ≠ 0) :
-    NonTorsionWeight w where
+theorem nonTorsionWeight_of [NoZeroSMulDivisors R M] (hw : ∀ i : σ, w i ≠ 0) :
+    NonTorsionWeight R w where
   eq_zero_of_smul_eq_zero {n s} h := by
     rw [smul_eq_zero, or_iff_not_imp_right] at h
     exact h (hw s)
 
-theorem NonTorsionWeight.ne_zero [NonTorsionWeight w] (s : σ) :
+variable (R) in
+theorem NonTorsionWeight.ne_zero [Nontrivial R] [NonTorsionWeight R w] (s : σ) :
     w s ≠ 0 := fun h ↦ by
-  rw [← one_smul ℕ (w s)] at h
-  apply Nat.zero_ne_one.symm
+  rw [← one_smul R (w s)] at h
+  apply zero_ne_one.symm (α := R)
   exact NonTorsionWeight.eq_zero_of_smul_eq_zero h
 
 variable {w} in
@@ -130,6 +141,7 @@ theorem le_weight (w : σ → ℕ) {s : σ} (hs : w s ≠ 0) (f : σ →₀ ℕ)
     apply zero_le
 
 variable [OrderedAddCommMonoid M] (w : σ → M)
+  {R : Type*} [OrderedCommSemiring R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Module R M]
 
 instance : SMulPosMono ℕ M :=
   ⟨fun b hb m m' h ↦ by
@@ -161,15 +173,15 @@ theorem le_weight_of_ne_zero' {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) :
 
 /-- If `M` is a `CanonicallyOrderedAddCommMonoid`, then `weight f` is zero iff `f=0. -/
 theorem weight_eq_zero_iff_eq_zero
-    (w : σ → M) [NonTorsionWeight w] {f : σ →₀ ℕ} :
+    (w : σ → M) [NonTorsionWeight ℕ w] {f : σ →₀ ℕ} :
     weight w f = 0 ↔ f = 0 := by
   classical
   constructor
   · intro h
     ext s
     simp only [Finsupp.coe_zero, Pi.zero_apply]
     by_contra hs
-    apply NonTorsionWeight.ne_zero w s
+    apply NonTorsionWeight.ne_zero ℕ w s
     rw [← nonpos_iff_eq_zero, ← h]
     exact le_weight_of_ne_zero' w hs
   · intro h
@@ -196,49 +208,50 @@ theorem finite_of_nat_weight_le [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x 
 
 end CanonicallyOrderedAddCommMonoid
 
+variable {R : Type*} [AddCommMonoid R]
+
 /-- The degree of a finsupp function. -/
-def degree (d : σ →₀ ℕ) := ∑ i ∈ d.support, d i
+def degree (d : σ →₀ R) : R := ∑ i ∈ d.support, d i
 
 @[deprecated degree (since := "2024-07-20")]
 alias _root_.MvPolynomial.degree := degree
 
 @[simp]
-theorem degree_add (a b : σ →₀ ℕ) : (a + b).degree = a.degree + b.degree :=
+theorem degree_add (a b : σ →₀ R) : (a + b).degree = a.degree + b.degree :=
   sum_add_index' (h := fun _ ↦ id) (congrFun rfl) fun _ _ ↦ congrFun rfl
 
 @[simp]
-theorem degree_single (a : σ) (m : ℕ) : (Finsupp.single a m).degree = m := by
-  rw [degree, Finset.sum_eq_single a]
-  · simp only [single_eq_same]
-  · intro b _ hba
-    exact single_eq_of_ne hba.symm
-  · intro ha
-    simp only [mem_support_iff, single_eq_same, ne_eq, Decidable.not_not] at ha
-    rw [single_eq_same, ha]
-
-lemma degree_eq_zero_iff (d : σ →₀ ℕ) : degree d = 0 ↔ d = 0 := by
-  simp only [degree, Finset.sum_eq_zero_iff, Finsupp.mem_support_iff, ne_eq, Decidable.not_imp_self,
-    DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply]
+theorem degree_single (a : σ) (r : R) : (Finsupp.single a r).degree = r :=
+  Finsupp.sum_single_index (h := fun _ => id) rfl
+
+@[simp]
+theorem degree_zero : degree (0 : σ →₀ R) = 0 := by simp [degree]
+
+lemma degree_eq_zero_iff {R : Type*} [OrderedAddCommMonoid R] [CanonicallyOrderedAdd R]
+    (d : σ →₀ R) :
+    degree d = 0 ↔ d = 0 := by
+  simp only [degree, Finset.sum_eq_zero_iff, mem_support_iff, ne_eq, _root_.not_imp_self,
+    DFunLike.ext_iff, coe_zero, Pi.zero_apply]
 
 @[deprecated degree_eq_zero_iff (since := "2024-07-20")]
 alias _root_.MvPolynomial.degree_eq_zero_iff := degree_eq_zero_iff
 
-@[simp]
-theorem degree_zero : degree (0 : σ →₀ ℕ) = 0 := by rw [degree_eq_zero_iff]
+theorem le_degree {R : Type*} [OrderedAddCommMonoid R] [CanonicallyOrderedAdd R]
+    (s : σ) (f : σ →₀ R) :
+    f s ≤ degree f := by
+  by_cases h : s ∈ f.support
+  · exact CanonicallyOrderedAddCommMonoid.single_le_sum h
+  · simp only [not_mem_support_iff] at h
+    simp only [h, zero_le]
 
-theorem degree_eq_weight_one :
-    degree (σ := σ) = weight 1 := by
+theorem degree_eq_weight_one {R : Type*} [Semiring R] :
+    degree (R := R) (σ := σ) = weight (fun _ ↦ 1) := by
   ext d
   simp only [degree, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum]
 
 @[deprecated degree_eq_weight_one (since := "2024-07-20")]
 alias _root_.MvPolynomial.weightedDegree_one := degree_eq_weight_one
 
-theorem le_degree (s : σ) (f : σ →₀ ℕ) : f s ≤ degree f  := by
-  rw [degree_eq_weight_one]
-  apply le_weight
-  simp only [Pi.one_apply, ne_eq, one_ne_zero, not_false_eq_true]
-
 theorem finite_of_degree_le [Finite σ] (n : ℕ) :
     {f : σ →₀ ℕ | degree f ≤ n}.Finite := by
   simp_rw [degree_eq_weight_one]

Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

@@ -76,6 +76,13 @@ variable (α M)
 theorem linearCombination_zero : linearCombination R (0 : α → M) = 0 :=
   LinearMap.ext (linearCombination_zero_apply R)
 
+@[simp]
+theorem linearCombination_single_index (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
+    linearCombination R (Pi.single a c) f = f a • c := by
+  rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
+  · exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]
+  · exact fun _ ↦ by simp only [single_eq_same, zero_smul]
+
 @[deprecated (since := "2024-08-29")] alias total_zero := linearCombination_zero
 
 variable {α M}

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

@@ -359,7 +359,7 @@ theorem weightedHomogeneousComponent_eq_zero [SemilatticeSup M] [OrderBot M]
 
 theorem weightedHomogeneousComponent_finsupp :
     (Function.support fun m => weightedHomogeneousComponent w m φ).Finite := by
-  apply Finite.subset ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite
+  apply ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite.subset
   intro m hm
   by_contra hm'
   apply hm (weightedHomogeneousComponent_eq_zero' m φ _)

Mathlib/RingTheory/MvPowerSeries/Order.lean

@@ -400,7 +400,7 @@ theorem order_eq_nat {n : ℕ} :
 
 /-- The order of the monomial `a*X^d` is infinite if `a = 0` and `degree d` otherwise.-/
 theorem order_monomial {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] :
-    order (monomial R d a) = if a = 0 then (⊤ : ℕ∞) else degree d := by
+    order (monomial R d a) = if a = 0 then (⊤ : ℕ∞) else ↑(degree d) := by
   rw [degree_eq_weight_one]
   exact weightedOrder_monomial _