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_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} [add_comm_monoid M] (w : σ → M) :

(σ →₀ ℕ) →+ M

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

Equations

mv_polynomial.weighted_degree' w = (finsupp.total σ M ℕ w).to_add_monoid_hom

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

mv_polynomial.weighted_total_degree' w p = p.support.sup (λ (s : σ →₀ ℕ), ↑(⇑(mv_polynomial.weighted_degree' w) s))

theorem mv_polynomial.weighted_total_degree'_eq_bot_iff {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) :

mv_polynomial.weighted_total_degree' w p = ⊥ ↔ 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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] [semilattice_sup M] (w : σ → M) :

mv_polynomial.weighted_total_degree' w 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

mv_polynomial.weighted_total_degree w p = p.support.sup (λ (s : σ →₀ ℕ), ⇑(mv_polynomial.weighted_degree' w) s)

theorem mv_polynomial.weighted_total_degree_coe {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) (hp : p ≠ 0) :

mv_polynomial.weighted_total_degree' w p = ↑(mv_polynomial.weighted_total_degree w p)

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

mv_polynomial.weighted_total_degree w 0 = ⊥

The weighted_total_degree of the zero polynomial is ⊥.

theorem mv_polynomial.le_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) {φ : mv_polynomial σ R} {d : σ →₀ ℕ} (hd : d ∈ φ.support) :

⇑(mv_polynomial.weighted_degree' w) d ≤ mv_polynomial.weighted_total_degree w φ

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

mv_polynomial.is_weighted_homogeneous w φ m = ∀ ⦃d : σ →₀ ℕ⦄, mv_polynomial.coeff d φ ≠ 0 → ⇑(mv_polynomial.weighted_degree' w) d = m

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

submodule R (mv_polynomial σ R)

The submodule of homogeneous mv_polynomials of degree n.

Equations

mv_polynomial.weighted_homogeneous_submodule R w m = {carrier := {x : mv_polynomial σ R | mv_polynomial.is_weighted_homogeneous w x m}, add_mem' := _, zero_mem' := _, smul_mem' := _}

Instances for mv_polynomial.weighted_homogeneous_submodule

mv_polynomial.is_weighted_homogeneous.weighted_homogeneous_submodule.gcomm_monoid

@[simp]

theorem mv_polynomial.mem_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) (p : mv_polynomial σ R) :

p ∈ mv_polynomial.weighted_homogeneous_submodule R w m ↔ mv_polynomial.is_weighted_homogeneous w p m

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

mv_polynomial.weighted_homogeneous_submodule R w m = finsupp.supported R R {d : σ →₀ ℕ | ⇑(mv_polynomial.weighted_degree' w) 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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (w : σ → M) (m n : M) :

mv_polynomial.weighted_homogeneous_submodule R w m * mv_polynomial.weighted_homogeneous_submodule R w n ≤ mv_polynomial.weighted_homogeneous_submodule R w (m + n)

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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] (w : σ → M) (d : σ →₀ ℕ) (r : R) {m : M} (hm : ⇑(mv_polynomial.weighted_degree' w) d = m) :

mv_polynomial.is_weighted_homogeneous w (⇑(mv_polynomial.monomial d) r) m

Monomials are weighted homogeneous.

theorem mv_polynomial.is_weighted_homogeneous_of_total_degree_zero {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} (hp : mv_polynomial.weighted_total_degree w p = ⊥) :

mv_polynomial.is_weighted_homogeneous w p ⊥

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

mv_polynomial.is_weighted_homogeneous w (⇑mv_polynomial.C r) 0

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

mv_polynomial.is_weighted_homogeneous w 0 m

0 is weighted homogeneous of any degree.

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

mv_polynomial.is_weighted_homogeneous w 1 0

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

mv_polynomial.is_weighted_homogeneous w (mv_polynomial.X i) (w 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) :

mv_polynomial.coeff d φ = 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} [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.

theorem mv_polynomial.is_weighted_homogeneous.add {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) (hψ : mv_polynomial.is_weighted_homogeneous w ψ n) :

mv_polynomial.is_weighted_homogeneous w (φ + ψ) 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} [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) :

mv_polynomial.is_weighted_homogeneous w (φ * ψ) (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} [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.

theorem mv_polynomial.is_weighted_homogeneous.weighted_total_degree {R : Type u_1} {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {φ : mv_polynomial σ R} {n : M} [semilattice_sup M] {w : σ → M} (hφ : mv_polynomial.is_weighted_homogeneous w φ n) (h : φ ≠ 0) :

mv_polynomial.weighted_total_degree' w φ = ↑n

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

@[protected, instance]

def mv_polynomial.is_weighted_homogeneous.weighted_homogeneous_submodule.gcomm_monoid {R : Type u_1} {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {w : σ → M} :

set_like.graded_monoid (mv_polynomial.weighted_homogeneous_submodule R w)

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

mv_polynomial σ R →ₗ[R] mv_polynomial σ R

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

mv_polynomial.weighted_homogeneous_component w n = (finsupp.supported R R {d : σ →₀ ℕ | ⇑(mv_polynomial.weighted_degree' w) d = n}).subtype.comp (finsupp.restrict_dom R R {d : σ →₀ ℕ | ⇑(mv_polynomial.weighted_degree' w) d = n})

theorem mv_polynomial.coeff_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) (φ : mv_polynomial σ R) [decidable_eq M] (d : σ →₀ ℕ) :

mv_polynomial.coeff d (⇑(mv_polynomial.weighted_homogeneous_component w n) φ) = ite (⇑(mv_polynomial.weighted_degree' w) d = n) (mv_polynomial.coeff d φ) 0

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

⇑(mv_polynomial.weighted_homogeneous_component w n) φ = (finset.filter (λ (d : σ →₀ ℕ), ⇑(mv_polynomial.weighted_degree' w) d = n) φ.support).sum (λ (d : σ →₀ ℕ), ⇑(mv_polynomial.monomial d) (mv_polynomial.coeff d φ))

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

mv_polynomial.is_weighted_homogeneous w (⇑(mv_polynomial.weighted_homogeneous_component w n) φ) n

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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {w : σ → M} (φ : mv_polynomial σ R) (n : M) (r : R) :

⇑(mv_polynomial.weighted_homogeneous_component w n) (⇑mv_polynomial.C r * φ) = ⇑mv_polynomial.C r * ⇑(mv_polynomial.weighted_homogeneous_component w n) φ

theorem mv_polynomial.weighted_homogeneous_component_eq_zero' {R : Type u_1} {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {w : σ → M} (n : M) (φ : mv_polynomial σ R) (h : ∀ (d : σ →₀ ℕ), d ∈ φ.support → ⇑(mv_polynomial.weighted_degree' w) d ≠ n) :

⇑(mv_polynomial.weighted_homogeneous_component w n) φ = 0

theorem mv_polynomial.weighted_homogeneous_component_eq_zero {R : Type u_1} {M : Type u_2} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {w : σ → M} (n : M) (φ : mv_polynomial σ R) [semilattice_sup M] [order_bot M] (h : mv_polynomial.weighted_total_degree w φ < n) :

⇑(mv_polynomial.weighted_homogeneous_component w n) φ = 0

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

(function.support (λ (m : M), ⇑(mv_polynomial.weighted_homogeneous_component w m) φ)).finite

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

finsum (λ (m : M), ⇑(mv_polynomial.weighted_homogeneous_component w 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} [comm_semiring R] {σ : Type u_3} [add_comm_monoid M] {w : σ → M} [decidable_eq M] (m n : M) (p : mv_polynomial σ R) (h : p ∈ mv_polynomial.weighted_homogeneous_submodule R w n) :

⇑(mv_polynomial.weighted_homogeneous_component w m) 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} [comm_semiring R] {σ : Type u_3} [canonically_ordered_add_monoid M] {w : σ → M} (φ : mv_polynomial σ R) [no_zero_smul_divisors ℕ M] (hw : ∀ (i : σ), w i ≠ 0) :

⇑(mv_polynomial.weighted_homogeneous_component w 0) φ = ⇑mv_polynomial.C (mv_polynomial.coeff 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.