# Documentation

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

# 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).

Instances For
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.

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.

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 : ) :
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.

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.

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 : ∀ (i : ι), i s) :

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} :
(∀ (i : ι), i sMvPolynomial.IsWeightedHomogeneous w (φ i) (n i)) → MvPolynomial.IsWeightedHomogeneous w (Finset.prod s fun i => φ i) (Finset.sum s fun i => 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.

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.

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) (φ : ) [] :
= Finset.sum (Finset.filter (fun d => = n) ()) fun d => ↑() ()
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.

@[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 : σ →₀ ), 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} (φ : ) :
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.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 CanonicallyOrderedAddMonoid, then the weightedHomogeneousComponent of weighted degree 0 of a polynomial is its constant coefficient.