Weights of finitely supported functions

If every variable has weight at most c, then the weight of a monomial f : σ →₀ ℕ is at most degree f • c. With c = -1 over ℤ, this says that a monomial all of whose variables have negative weight has weight at most minus its total degree, which is how negatively graded variables bound the degree of elements of powers of the ideal of the variables.

Weights also respect scaling of the weight vector and decompose into contributions before, at, and after a chosen coordinate in a linear order. These identities support comparisons between lexicographic order and weighted degree.

Main results

• Finsupp.weight_le_degree_nsmul: if w s ≤ c for all s, then weight w f ≤ degree f • c.
• Finsupp.weight_filter_gt_add_smul_add_weight_filter_lt: split a weight at a coordinate.
• Finsupp.weight_smul_left: scaling the weight vector scales the weight.

theorem Finsupp.weight_le_degree_nsmul {σ : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [AddLeftMono M] (f : σ →₀ ℕ) {w : σ → M} {c : M} (hw : ∀ (s : σ), w s ≤ c) : (weight w) f ≤ degree f • c

If every variable has weight at most c, then the weight of f is at most its degree times c.

theorem Finsupp.filter_gt_add_single_add_filter_lt {σ : Type u_1} {M : Type u_2} [LinearOrder σ] [AddZeroClass M] (f : σ →₀ M) (i : σ) : filter (fun (x : σ) => x < i) f + single i (f i) + filter (fun (x : σ) => i < x) f = f

A finitely supported function splits into its values before i, at i, and after i.

theorem Finsupp.weight_filter_gt_add_smul_add_weight_filter_lt {σ : Type u_1} {M : Type u_2} [LinearOrder σ] [AddCommMonoid M] (c : σ → M) (w : σ →₀ ℕ) (i : σ) : (weight c) (filter (fun (x : σ) => x < i) w) + w i • c i + (weight c) (filter (fun (x : σ) => i < x) w) = (weight c) w

The c-weight of an exponent w splits into the weights of its coordinates before i, at i, and after i.

theorem Finsupp.weight_smul_left {σ : Type u_1} {M : Type u_2} {R : Type u_3} {S : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] (s : S) (c : σ → M) (w : σ →₀ R) : (weight (s • c)) w = s • (weight c) w

Scaling the weight vector scales the weight.