mathlib3 documentation

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_degree' #

noncomputable def mv_polynomial.weighted_degree' {M : Type u_2} {σ : Type u_3} [add_comm_monoid M] (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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] [semilattice_sup M] (w : σ M) (p : mv_polynomial σ R) :

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

Equations

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

The weighted_total_degree' of the zero polynomial is .

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

This lemma relates weighted_total_degree and weighted_total_degree'.

The weighted_total_degree of the zero polynomial is .

def mv_polynomial.is_weighted_homogeneous {R : Type u_1} {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (w : σ M) (φ : mv_polynomial σ 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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (w : σ M) (m : M) :

The submodule of homogeneous mv_polynomials of degree n.

Equations
Instances for mv_polynomial.weighted_homogeneous_submodule

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.

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.

Monomials are weighted homogeneous.

A polynomial of weighted_total_degree is weighted_homogeneous of degree .

Constant polynomials are weighted homogeneous of degree 0.

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

0 is weighted homogeneous of any degree.

1 is weighted homogeneous of degree 0.

theorem mv_polynomial.is_weighted_homogeneous_X (R : Type u_1) {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {φ : mv_polynomial σ R} {n : M} {w : σ M} (hφ : mv_polynomial.is_weighted_homogeneous w φ n) (d : σ →₀ ) (hd : (mv_polynomial.weighted_degree' w) d n) :

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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {φ : mv_polynomial σ R} {m n : M} {w : σ M} (hφ : φ 0) (hm : mv_polynomial.is_weighted_homogeneous w φ m) (hn : mv_polynomial.is_weighted_homogeneous w φ n) :
m = n

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

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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {ι : Type u_4} (s : finset ι) (φ : ι mv_polynomial σ R) (n : M) {w : σ M} (h : (i : ι), i s mv_polynomial.is_weighted_homogeneous w (φ i) n) :
mv_polynomial.is_weighted_homogeneous w (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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {φ ψ : mv_polynomial σ R} {m n : M} {w : σ M} (hφ : mv_polynomial.is_weighted_homogeneous w φ m) (hψ : mv_polynomial.is_weighted_homogeneous w ψ 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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {ι : Type u_4} (s : finset ι) (φ : ι mv_polynomial σ R) (n : ι M) {w : σ M} :
( (i : ι), i s mv_polynomial.is_weighted_homogeneous w (φ i) (n i)) mv_polynomial.is_weighted_homogeneous w (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.

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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (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

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

theorem mv_polynomial.sum_weighted_homogeneous_component {R : Type u_1} {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (w : σ M) (φ : mv_polynomial σ R) :

Every polynomial is the sum of its weighted homogeneous components.

The weighted homogeneous components of a weighted homogeneous polynomial.

@[simp]

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