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 to classify these exponents according to their total sum ∑ i, f i, or variants, and this files provides some API for that.

Weight

We fix a type σ and an AddCommMonoid M, as well as a function w : σ → M.

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

• For w : σ → ℕ and Finite σ, Finsupp.finite_of_nat_weight_le proves that 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_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

• For Finite σ, Finsupp.finite_of_degree_le proves that 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 Mis an N-module.

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

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

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

Equations

• Finsupp.weight w = (Finsupp.linearCombination ℕ w).toAddMonoidHom

@[deprecated Finsupp.weight]

def MvPolynomial.weightedDegree {σ : Type u_1} {M : Type u_2} (w : σ → M) [AddCommMonoid M] : (σ →₀ ℕ) →+ M

Alias of Finsupp.weight.

---

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

Equations

• @MvPolynomial.weightedDegree = @Finsupp.weight

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

@[deprecated Finsupp.weight_apply]

theorem MvPolynomial.weightedDegree_apply {σ : Type u_1} {M : Type u_2} (w : σ → M) [AddCommMonoid M] (f : σ →₀ ℕ) : (Finsupp.weight w) f = f.sum fun (i : σ) (c : ℕ) => c • w i

Alias of Finsupp.weight_apply.

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

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

• eq_zero_of_smul_eq_zero {n : ℕ} {s : σ} (h : n • w s = 0) : n = 0

theorem Finsupp.nonTorsionWeight_of {σ : Type u_1} {M : Type u_2} (w : σ → M) [AddCommMonoid M] [NoZeroSMulDivisors ℕ M] (hw : ∀ (i : σ), w i ≠ 0) : Finsupp.NonTorsionWeight w

Without zero divisors, nonzero weight is a NonTorsionWeight

theorem Finsupp.NonTorsionWeight.ne_zero {σ : Type u_1} {M : Type u_2} (w : σ → M) [AddCommMonoid M] [Finsupp.NonTorsionWeight 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) : (Finsupp.weight w) (f - Finsupp.single i 1) + w i = (Finsupp.weight w) f

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

instance Finsupp.instSMulPosMonoNat {M : Type u_2} [OrderedAddCommMonoid M] : SMulPosMono ℕ M

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

theorem Finsupp.le_weight_of_ne_zero' {σ : Type u_1} {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] (w : σ → M) {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) : w s ≤ (Finsupp.weight w) f

theorem Finsupp.weight_eq_zero_iff_eq_zero {σ : Type u_1} {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] (w : σ → M) [Finsupp.NonTorsionWeight w] {f : σ →₀ ℕ} : (Finsupp.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 : σ →₀ ℕ | (Finsupp.weight w) d ≤ n}.Finite

def Finsupp.degree {σ : Type u_1} (d : σ →₀ ℕ) : ℕ

The degree of a finsupp function.

Equations

• d.degree = ∑ i ∈ d.support, d i

@[deprecated Finsupp.degree]

def MvPolynomial.degree {σ : Type u_1} (d : σ →₀ ℕ) : ℕ

Alias of Finsupp.degree.

---

The degree of a finsupp function.

Equations

• @MvPolynomial.degree = @Finsupp.degree

@[simp]

theorem Finsupp.degree_add {σ : Type u_1} (a b : σ →₀ ℕ) : (a + b).degree = a.degree + b.degree

@[simp]

theorem Finsupp.degree_single {σ : Type u_1} (a : σ) (m : ℕ) : (Finsupp.single a m).degree = m

theorem Finsupp.degree_eq_zero_iff {σ : Type u_1} (d : σ →₀ ℕ) : d.degree = 0 ↔ d = 0

@[deprecated Finsupp.degree_eq_zero_iff]

theorem MvPolynomial.degree_eq_zero_iff {σ : Type u_1} (d : σ →₀ ℕ) : d.degree = 0 ↔ d = 0

Alias of Finsupp.degree_eq_zero_iff.

@[simp]

theorem Finsupp.degree_zero {σ : Type u_1} : Finsupp.degree 0 = 0

theorem Finsupp.degree_eq_weight_one {σ : Type u_1} : Finsupp.degree = ⇑(Finsupp.weight 1)

@[deprecated Finsupp.degree_eq_weight_one]

theorem MvPolynomial.weightedDegree_one {σ : Type u_1} : Finsupp.degree = ⇑(Finsupp.weight 1)

Alias of Finsupp.degree_eq_weight_one.

theorem Finsupp.le_degree {σ : Type u_1} (s : σ) (f : σ →₀ ℕ) : f s ≤ f.degree

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