# Weighted homogeneous polynomials #

It is possible to assign weights (in a commutative additive monoid M) to the variables of a multivariate polynomial ring, so that monomials of the ring then have a weighted degree with respect to the weights of the variables. The weights are represented by a function w : σ → M, where σ are the indeterminates.

A multivariate polynomial φ is weighted homogeneous of weighted degree m : M if all monomials occurring in φ have the same weighted degree m.

## Main definitions/lemmas #

• weightedTotalDegree' w φ : the weighted total degree of a multivariate polynomial with respect to the weights w, taking values in WithBot M.

• weightedTotalDegree w φ : When M has a ⊥ element, we can define the weighted total degree of a multivariate polynomial as a function taking values in M.

• IsWeightedHomogeneous w φ m: a predicate that asserts that φ is weighted homogeneous of weighted degree m with respect to the weights w.

• weightedHomogeneousSubmodule R w m: the submodule of homogeneous polynomials of weighted degree m.

• weightedHomogeneousComponent w m: the additive morphism that projects polynomials onto their summand that is weighted homogeneous of degree n with respect to w.

• sum_weightedHomogeneousComponent: every polynomial is the sum of its weighted homogeneous components.

### weightedDegree#

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

The weightedDegree of the finitely supported function s : σ →₀ ℕ is the sum ∑(s i)•(w i).

Equations
Instances For
theorem MvPolynomial.weightedDegree_apply {M : Type u_2} {σ : Type u_3} [] (w : σM) (f : σ →₀ ) :
= f.sum fun (i : σ) (c : ) => c w i
def MvPolynomial.weightedTotalDegree' {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] (w : σM) (p : ) :

The weighted total degree of a multivariate polynomial, taking values in WithBot M.

Equations
Instances For
theorem MvPolynomial.weightedTotalDegree'_eq_bot_iff {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] (w : σM) (p : ) :
p = 0

The weightedTotalDegree' of a polynomial p is ⊥ if and only if p = 0.

theorem MvPolynomial.weightedTotalDegree'_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] (w : σM) :

The weightedTotalDegree' of the zero polynomial is ⊥.

def MvPolynomial.weightedTotalDegree {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] [] (w : σM) (p : ) :
M

When M has a ⊥ element, we can define the weighted total degree of a multivariate polynomial as a function taking values in M.

Equations
Instances For
theorem MvPolynomial.weightedTotalDegree_coe {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] [] (w : σM) (p : ) (hp : p 0) :

This lemma relates weightedTotalDegree and weightedTotalDegree'.

theorem MvPolynomial.weightedTotalDegree_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] [] (w : σM) :

The weightedTotalDegree of the zero polynomial is ⊥.

theorem MvPolynomial.le_weightedTotalDegree {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] [] (w : σM) {φ : } {d : σ →₀ } (hd : d φ.support) :
def MvPolynomial.IsWeightedHomogeneous {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (φ : ) (m : M) :

A multivariate polynomial φ is weighted homogeneous of weighted degree m if all monomials occurring in φ have weighted degree m.

Equations
Instances For
def MvPolynomial.weightedHomogeneousSubmodule (R : Type u_1) {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (m : M) :

The submodule of homogeneous MvPolynomials of degree n.

Equations
• = { carrier := {x : | }, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem MvPolynomial.mem_weightedHomogeneousSubmodule (R : Type u_1) {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (m : M) (p : ) :
theorem MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported (R : Type u_1) {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (m : M) :
= Finsupp.supported R R {d : σ →₀ | = m}

The submodule weightedHomogeneousSubmodule R w m of homogeneous MvPolynomials of degree n is equal to the R-submodule of all p : (σ →₀ ℕ) →₀ R such that p.support ⊆ {d | weightedDegree w d = m}. While equal, the former has a convenient definitional reduction.

theorem MvPolynomial.weightedHomogeneousSubmodule_mul {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (m : M) (n : M) :

The submodule generated by products Pm * Pn of weighted homogeneous polynomials of degrees m and n is contained in the submodule of weighted homogeneous polynomials of degree m + n.

theorem MvPolynomial.isWeightedHomogeneous_monomial {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (d : σ →₀ ) (r : R) {m : M} (hm : = m) :

Monomials are weighted homogeneous.

theorem MvPolynomial.isWeightedHomogeneous_of_total_degree_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] [] [] (w : σM) {p : } (hp : ) :

A polynomial of weightedTotalDegree ⊥ is weighted_homogeneous of degree ⊥.

theorem MvPolynomial.isWeightedHomogeneous_C {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (r : R) :
MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.C r) 0

Constant polynomials are weighted homogeneous of degree 0.

theorem MvPolynomial.isWeightedHomogeneous_zero (R : Type u_1) {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (m : M) :

0 is weighted homogeneous of any degree.

theorem MvPolynomial.isWeightedHomogeneous_one (R : Type u_1) {M : Type u_2} [] {σ : Type u_3} [] (w : σM) :

1 is weighted homogeneous of degree 0.

theorem MvPolynomial.isWeightedHomogeneous_X (R : Type u_1) {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (i : σ) :

An indeterminate i : σ is weighted homogeneous of degree w i.

theorem MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {φ : } {n : M} {w : σM} (hφ : ) (d : σ →₀ ) (hd : n) :
= 0

The weighted degree of a weighted homogeneous polynomial controls its support.

theorem MvPolynomial.IsWeightedHomogeneous.inj_right {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {φ : } {m : M} {n : M} {w : σM} (hφ : φ 0) (hm : ) (hn : ) :
m = n

The weighted degree of a nonzero weighted homogeneous polynomial is well-defined.

theorem MvPolynomial.IsWeightedHomogeneous.add {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {φ : } {ψ : } {n : M} {w : σM} (hφ : ) (hψ : ) :

The sum of two weighted homogeneous polynomials of degree n is weighted homogeneous of weighted degree n.

theorem MvPolynomial.IsWeightedHomogeneous.sum {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {ι : Type u_4} (s : ) (φ : ι) (n : M) {w : σM} (h : is, ) :
MvPolynomial.IsWeightedHomogeneous w (is, φ i) n

The sum of weighted homogeneous polynomials of degree n is weighted homogeneous of weighted degree n.

theorem MvPolynomial.IsWeightedHomogeneous.mul {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {φ : } {ψ : } {m : M} {n : M} {w : σM} (hφ : ) (hψ : ) :

The product of weighted homogeneous polynomials of weighted degrees m and n is weighted homogeneous of weighted degree m + n.

theorem MvPolynomial.IsWeightedHomogeneous.prod {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {ι : Type u_4} (s : ) (φ : ι) (n : ιM) {w : σM} :
(is, MvPolynomial.IsWeightedHomogeneous w (φ i) (n i))MvPolynomial.IsWeightedHomogeneous w (is, φ i) (is, n i)

A product of weighted homogeneous polynomials is weighted homogeneous, with weighted degree equal to the sum of the weighted degrees.

theorem MvPolynomial.IsWeightedHomogeneous.weighted_total_degree {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {φ : } {n : M} [] {w : σM} (hφ : ) (h : φ 0) :

A non zero weighted homogeneous polynomial of weighted degree n has weighted total degree n.

instance MvPolynomial.IsWeightedHomogeneous.WeightedHomogeneousSubmodule.gcomm_monoid {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} :

The weighted homogeneous submodules form a graded monoid.

Equations
• =
def MvPolynomial.weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (n : M) :

weightedHomogeneousComponent w n φ is the part of φ that is weighted homogeneous of weighted degree n, with respect to the weights w. See sum_weightedHomogeneousComponent for the statement that φ is equal to the sum of all its weighted homogeneous components.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MvPolynomial.coeff_weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (n : M) (φ : ) [] (d : σ →₀ ) :
= if = n then else 0
theorem MvPolynomial.weightedHomogeneousComponent_apply {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (n : M) (φ : ) [] :
= dFinset.filter (fun (d : σ →₀ ) => = n) φ.support, ()
theorem MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (n : M) (φ : ) :

The n weighted homogeneous component of a polynomial is weighted homogeneous of weighted degree n.

theorem MvPolynomial.weightedHomogeneousComponent_mem {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (φ : ) (m : M) :
@[simp]
theorem MvPolynomial.weightedHomogeneousComponent_C_mul {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (φ : ) (n : M) (r : R) :
(MvPolynomial.C r * φ) = MvPolynomial.C r *
theorem MvPolynomial.weightedHomogeneousComponent_eq_zero' {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (n : M) (φ : ) (h : dφ.support, n) :
theorem MvPolynomial.weightedHomogeneousComponent_eq_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (n : M) (φ : ) [] [] (h : ) :
theorem MvPolynomial.weightedHomogeneousComponent_finsupp {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} (φ : ) :
(Function.support fun (m : M) => ).Finite
theorem MvPolynomial.sum_weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (φ : ) :
∑ᶠ (m : M), = φ

Every polynomial is the sum of its weighted homogeneous components.

theorem MvPolynomial.finsum_weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] (w : σM) (φ : ) :
∑ᶠ (m : M), = φ
theorem MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} {m : M} {p : } (hp : ) :
theorem MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} {m : M} (n : M) {p : } (hp : ) :
n m
theorem MvPolynomial.weightedHomogeneousComponent_weighted_homogeneous_polynomial {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} [] {w : σM} [] (m : M) (n : M) (p : ) (h : ) :
= if m = n then p else 0

The weighted homogeneous components of a weighted homogeneous polynomial.

@[simp]
theorem MvPolynomial.weightedHomogeneousComponent_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} {w : σM} (φ : ) [] (hw : ∀ (i : σ), w i 0) :
= MvPolynomial.C ()

If M is a CanonicallyOrderedAddCommMonoid, then the weightedHomogeneousComponent of weighted degree 0 of a polynomial is its constant coefficient.

def MvPolynomial.NonTorsionWeight {M : Type u_2} {σ : Type u_3} (w : σM) :

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

Equations
• = ∀ (n : ) (x : σ), n w x = 0n = 0
Instances For
theorem MvPolynomial.nonTorsionWeight_of {M : Type u_2} {σ : Type u_3} {w : σM} [] (hw : ∀ (i : σ), w i 0) :
theorem MvPolynomial.weightedDegree_eq_zero_iff {M : Type u_2} {σ : Type u_3} {w : σM} (hw : ) {m : σ →₀ } :
= 0 ∀ (x : σ), m x = 0

If w is a nontorsion weight function, then the finitely supported function m : σ →₀ ℕ has weighted degree zero if and only if ∀ x : σ, m x = 0.

theorem MvPolynomial.isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} {w : σM} {p : } :

A multivatiate polynomial is weighted homogeneous of weighted degree zero if and only if its weighted total degree is equal to zero.

theorem MvPolynomial.weightedTotalDegree_eq_zero_iff {R : Type u_1} {M : Type u_2} [] {σ : Type u_3} {w : σM} (hw : ) (p : ) :
mp.support, ∀ (x : σ), m x = 0

If w is a nontorsion weight function, then a multivariate polynomial has weighted total degree zero if and only if for every m ∈ p.support and x : σ, m x = 0.