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 σ, 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 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 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.

Equations

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

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) (single 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] [NoZeroSMulDivisors 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 - single 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

instance Finsupp.instSMulPosMonoNat {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] : SMulPosMono ℕ M

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] (d : σ →₀ R) : R

The degree of a finsupp function.

Equations

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

@[simp]

theorem Finsupp.degree_add {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] (a b : σ →₀ R) : (a + b).degree = a.degree + b.degree

@[simp]

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

@[simp]

theorem Finsupp.degree_zero {σ : Type u_1} {R : Type u_4} [AddCommMonoid R] : degree 0 = 0

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

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

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 : σ →₀ ℕ | f.degree ≤ n}.Finite