# mathlib3documentation

ring_theory.mv_polynomial.weighted_homogeneous

# Weighted homogeneous polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 occuring in φ have the same weighted degree m.

## Main definitions/lemmas #

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

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

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

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

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

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

### weighted_degree'#

noncomputable def mv_polynomial.weighted_degree' {M : Type u_2} {σ : Type u_3} (w : σ M) :
→₀ ) →+ M

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

Equations
noncomputable def mv_polynomial.weighted_total_degree' {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) (p : R) :

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

Equations
theorem mv_polynomial.weighted_total_degree'_eq_bot_iff {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) (p : R) :
p = 0

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

theorem mv_polynomial.weighted_total_degree'_zero {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) :

The weighted_total_degree' of the zero polynomial is ⊥.

noncomputable def mv_polynomial.weighted_total_degree {R : Type u_1} {M : Type u_2} {σ : Type u_3} [order_bot M] (w : σ M) (p : R) :
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
theorem mv_polynomial.weighted_total_degree_coe {R : Type u_1} {M : Type u_2} {σ : Type u_3} [order_bot M] (w : σ M) (p : R) (hp : p 0) :

This lemma relates weighted_total_degree and weighted_total_degree'.

theorem mv_polynomial.weighted_total_degree_zero {R : Type u_1} {M : Type u_2} {σ : Type u_3} [order_bot M] (w : σ M) :

The weighted_total_degree of the zero polynomial is ⊥.

theorem mv_polynomial.le_weighted_total_degree {R : Type u_1} {M : Type u_2} {σ : Type u_3} [order_bot M] (w : σ M) {φ : R} {d : σ →₀ } (hd : d φ.support) :
def mv_polynomial.is_weighted_homogeneous {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) (φ : R) (m : M) :
Prop

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

Equations
def mv_polynomial.weighted_homogeneous_submodule (R : Type u_1) {M : Type u_2} {σ : Type u_3} (w : σ M) (m : M) :
R)

The submodule of homogeneous mv_polynomials of degree n.

Equations
Instances for mv_polynomial.weighted_homogeneous_submodule
@[simp]
theorem mv_polynomial.mem_weighted_homogeneous_submodule (R : Type u_1) {M : Type u_2} {σ : Type u_3} (w : σ M) (m : M) (p : R) :
theorem mv_polynomial.weighted_homogeneous_submodule_eq_finsupp_supported (R : Type u_1) {M : Type u_2} {σ : Type u_3} (w : σ M) (m : M) :
= {d : σ →₀ | = m}

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

theorem mv_polynomial.weighted_homogeneous_submodule_mul {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ 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 mv_polynomial.is_weighted_homogeneous_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 mv_polynomial.is_weighted_homogeneous_of_total_degree_zero {R : Type u_1} {M : Type u_2} {σ : Type u_3} [order_bot M] (w : σ M) {p : R} (hp : = ) :

A polynomial of weighted_total_degree ⊥ is weighted_homogeneous of degree ⊥.

theorem mv_polynomial.is_weighted_homogeneous_C {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) (r : R) :

Constant polynomials are weighted homogeneous of degree 0.

theorem mv_polynomial.is_weighted_homogeneous_zero (R : Type u_1) {M : Type u_2} {σ : Type u_3} (w : σ M) (m : M) :

0 is weighted homogeneous of any degree.

theorem mv_polynomial.is_weighted_homogeneous_one (R : Type u_1) {M : Type u_2} {σ : Type u_3} (w : σ M) :

1 is weighted homogeneous of degree 0.

theorem mv_polynomial.is_weighted_homogeneous_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 mv_polynomial.is_weighted_homogeneous.coeff_eq_zero {R : Type u_1} {M : Type u_2} {σ : Type u_3} {φ : R} {n : M} {w : σ M} (hφ : n) (d : σ →₀ ) (hd : n) :
= 0

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

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

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

theorem mv_polynomial.is_weighted_homogeneous.add {R : Type u_1} {M : Type u_2} {σ : Type u_3} {φ ψ : R} {n : M} {w : σ M} (hφ : n) (hψ : n) :
n

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

theorem mv_polynomial.is_weighted_homogeneous.sum {R : Type u_1} {M : Type u_2} {σ : Type u_3} {ι : Type u_4} (s : finset ι) (φ : ι ) (n : M) {w : σ M} (h : (i : ι), i s ) :
(s.sum (λ (i : ι), φ i)) n

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

theorem mv_polynomial.is_weighted_homogeneous.mul {R : Type u_1} {M : Type u_2} {σ : Type u_3} {φ ψ : R} {m n : M} {w : σ M} (hφ : m) (hψ : n) :
(m + n)

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

theorem mv_polynomial.is_weighted_homogeneous.prod {R : Type u_1} {M : Type u_2} {σ : Type u_3} {ι : Type u_4} (s : finset ι) (φ : ι ) (n : ι M) {w : σ M} :
( (i : ι), i s (n i)) (s.prod (λ (i : ι), φ i)) (s.sum (λ (i : ι), n i))

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

theorem mv_polynomial.is_weighted_homogeneous.weighted_total_degree {R : Type u_1} {M : Type u_2} {σ : Type u_3} {φ : R} {n : M} {w : σ M} (hφ : n) (h : φ 0) :

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

@[protected, instance]

The weighted homogeneous submodules form a graded monoid.

noncomputable def mv_polynomial.weighted_homogeneous_component {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) (n : M) :

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

Equations
theorem mv_polynomial.coeff_weighted_homogeneous_component {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (n : M) (φ : R) [decidable_eq M] (d : σ →₀ ) :
= ite = n) φ) 0
theorem mv_polynomial.weighted_homogeneous_component_apply {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (n : M) (φ : R) [decidable_eq M] :
= (finset.filter (λ (d : σ →₀ ), = n) φ.support).sum (λ (d : σ →₀ ), φ))
theorem mv_polynomial.weighted_homogeneous_component_is_weighted_homogeneous {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (n : M) (φ : R) :

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

@[simp]
theorem mv_polynomial.weighted_homogeneous_component_C_mul {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (φ : R) (n : M) (r : R) :
theorem mv_polynomial.weighted_homogeneous_component_eq_zero' {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (n : M) (φ : R) (h : (d : σ →₀ ), d φ.support ) :
theorem mv_polynomial.weighted_homogeneous_component_eq_zero {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (n : M) (φ : R) [order_bot M] (h : < n) :
theorem mv_polynomial.weighted_homogeneous_component_finsupp {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (φ : R) :
(function.support (λ (m : M), .finite
theorem mv_polynomial.sum_weighted_homogeneous_component {R : Type u_1} {M : Type u_2} {σ : Type u_3} (w : σ M) (φ : R) :
finsum (λ (m : M), = φ

Every polynomial is the sum of its weighted homogeneous components.

theorem mv_polynomial.weighted_homogeneous_component_weighted_homogeneous_polynomial {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} [decidable_eq M] (m n : M) (p : R) (h : p ) :
= ite (m = n) p 0

The weighted homogeneous components of a weighted homogeneous polynomial.

@[simp]
theorem mv_polynomial.weighted_homogeneous_component_zero {R : Type u_1} {M : Type u_2} {σ : Type u_3} {w : σ M} (φ : R) (hw : (i : σ), w i 0) :

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