weights of Finsupp functions

The theory of multivariate polynomials and power series is built on the type σ →₀ ℕ which gives the exponents of the monomials. Many aspects of the theory (degree, order, graded ring structure) require classifying these exponents according to their total sum ∑ i, f i, or variants, and this file provides some API for that.

Weight

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 : σ →₀ 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.

• Finsupp.le_weight_of_ne_zero' is the same statement for CanonicallyOrderedAddCommMonoid M.

• NonTorsionWeight: all values w s are nontorsion in M.

• Finsupp.weight_eq_zero_iff_eq_zero says that f.weight w = 0 iff 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.

Degree

• 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 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.

TODO

• Maybe Finsupp.weight w and Finsupp.degree should have similar types, both AddMonoidHom or both functions.

noncomputable def Finsupp.weight {σ : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] (w : σ → M) [AddCommMonoid M] [Module R M] : (σ →₀ R) →+ M

The weight of the finitely supported function f : σ →₀ R with respect to w : σ → M is the sum ∑ i, f i • w i.

theorem Finsupp.weight_apply {σ : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] (w : σ → M) [AddCommMonoid M] [Module R M] (f : σ →₀ R) : (weight w) f = f.sum fun (i : σ) (c : R) => c • w i

theorem Finsupp.weight_single_index {σ : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq σ] (s : σ) (c : M) (f : σ →₀ R) : (weight (Pi.single s c)) f = f s • c

theorem Finsupp.weight_single_one_apply {σ : Type u_1} {R : Type u_3} [Semiring R] [DecidableEq σ] (s : σ) (f : σ →₀ R) : (weight (Pi.single s 1)) f = f s

theorem Finsupp.weight_single {σ : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] (w : σ → M) [AddCommMonoid M] [Module R M] (s : σ) (r : R) : ((weight w) fun₀ | s => r) = r • w s

class Finsupp.NonTorsionWeight {σ : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] (w : σ → M) : Prop

A weight function is nontorsion if its values are not torsion.

• eq_zero_of_smul_eq_zero {r : R} {s : σ} (h : r • w s = 0) : r = 0

theorem Finsupp.nonTorsionWeight_of {σ : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] (w : σ → M) [AddCommMonoid M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] (hw : ∀ (i : σ), w i ≠ 0) : NonTorsionWeight R w

Without zero divisors, nonzero weight is a NonTorsionWeight

theorem Finsupp.NonTorsionWeight.ne_zero {σ : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] (w : σ → M) [AddCommMonoid M] [Module R M] [Nontrivial R] [NonTorsionWeight R w] (s : σ) : w s ≠ 0

theorem Finsupp.weight_sub_single_add {σ : Type u_1} {M : Type u_2} {w : σ → M} [AddCommMonoid M] {f : σ →₀ ℕ} {i : σ} (hi : f i ≠ 0) : (weight w) (f - fun₀ | i => 1) + w i = (weight w) f

theorem Finsupp.le_weight {σ : Type u_1} (w : σ → ℕ) {s : σ} (hs : w s ≠ 0) (f : σ →₀ ℕ) : f s ≤ (weight w) f

theorem Finsupp.le_weight_of_ne_zero {σ : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {w : σ → M} (hw : ∀ (s : σ), 0 ≤ w s) {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) : w s ≤ (weight w) f

theorem Finsupp.le_weight_of_ne_zero' {σ : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [CanonicallyOrderedAdd M] (w : σ → M) {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) : w s ≤ (weight w) f

theorem Finsupp.weight_eq_zero_iff_eq_zero {σ : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [CanonicallyOrderedAdd M] (w : σ → M) [NonTorsionWeight ℕ w] {f : σ →₀ ℕ} : (weight w) f = 0 ↔ f = 0

If M is a CanonicallyOrderedAddCommMonoid, then weight f is zero iff f = 0.

theorem Finsupp.finite_of_nat_weight_le {σ : Type u_1} [Finite σ] (w : σ → ℕ) (hw : ∀ (x : σ), w x ≠ 0) (n : ℕ) : {d : σ →₀ ℕ | (weight w) d ≤ n}.Finite

def Finsupp.degree {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] : (σ →₀ R) →+ R

The degree of a finsupp function.

@[deprecated map_add (since := "2025-12-09")]

theorem Finsupp.degree_add {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (x y : M) : f (x + y) = f x + f y

Alias of map_add.

@[deprecated map_zero (since := "2025-12-09")]

theorem Finsupp.degree_zero {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (f : F) : f 0 = 0

Alias of map_zero.

theorem Finsupp.degree_apply {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] (d : σ →₀ R) : degree d = ∑ i ∈ d.support, d i

@[deprecated Finsupp.degree_apply (since := "2025-12-09")]

theorem Finsupp.degree_def {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] (d : σ →₀ R) : degree d = ∑ i ∈ d.support, d i

Alias of Finsupp.degree_apply.

theorem Finsupp.degree_eq_sum {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] [Fintype σ] (f : σ →₀ R) : degree f = ∑ i : σ, f i

@[simp]

theorem Finsupp.degree_single {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] (a : σ) (r : R) : (degree fun₀ | a => r) = r

theorem Finsupp.degree_eq_zero_iff {σ : Type u_1} {R : Type u_5} [AddCommMonoid R] [PartialOrder R] [CanonicallyOrderedAdd R] (d : σ →₀ R) : degree d = 0 ↔ d = 0

theorem Finsupp.le_degree {σ : Type u_1} {R : Type u_5} [AddCommMonoid R] [PartialOrder R] [CanonicallyOrderedAdd R] (s : σ) (f : σ →₀ R) : f s ≤ degree f

theorem Finsupp.degree_eq_weight_one {σ : Type u_1} {R : Type u_5} [Semiring R] : degree = weight fun (x : σ) => 1

theorem Finsupp.finite_of_degree_le {σ : Type u_1} [Finite σ] (n : ℕ) : {f : σ →₀ ℕ | degree f ≤ n}.Finite

theorem Finsupp.range_single_one {σ : Type u_1} : (Set.range fun (a : σ) => fun₀ | a => 1) = {d : σ →₀ ℕ | degree d = 1}

theorem Finsupp.degree_mono {σ : Type u_1} {R : Type u_5} [AddCommMonoid R] [PartialOrder R] [CanonicallyOrderedAdd R] : Monotone ⇑degree

theorem Finsupp.exists_le_degree_eq {σ : Type u_5} (f : σ →₀ ℕ) (n : ℕ) (hn : n ≤ degree f) : ∃ g ≤ f, degree g = n

theorem Finsupp.degree_preimage_add {σ : Type u_5} (s t : Set ℕ) : ⇑degree ⁻¹' (s + t) = ⇑degree ⁻¹' s + ⇑degree ⁻¹' t

theorem Finsupp.degree_preimage_nsmul {σ : Type u_5} (s : Set ℕ) (n : ℕ) (hn : n ≠ 0) : ⇑degree ⁻¹' (n • s) = n • ⇑degree ⁻¹' s

theorem Finsupp.nsmul_single_one_image {α : Type u_5} {n : ℕ} {s : Set α} : n • (fun (x : α) => fun₀ | x => 1) '' s = {x : α →₀ ℕ | degree x = n ∧ ↑x.support ⊆ s}

theorem Finsupp.image_pow_eq_finsuppProd_image {α : Type u_5} {β : Type u_6} [CommMonoid β] {f : α → β} {n : ℕ} {s : Set α} : (f '' s) ^ n = (fun (x : α →₀ ℕ) => x.prod fun (x1 : α) (x2 : ℕ) => f x1 ^ x2) '' {x : α →₀ ℕ | degree x = n ∧ ↑x.support ⊆ s}