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} [AddCommMonoid M] (w : σ → M) : (σ →₀ ℕ) →+ M

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

Equations

• MvPolynomial.weightedDegree w = LinearMap.toAddMonoidHom (Finsupp.total σ M ℕ w)

theorem MvPolynomial.weightedDegree_apply {M : Type u_2} {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (f : σ →₀ ℕ) : (MvPolynomial.weightedDegree w) f = Finsupp.sum f fun (i : σ) (c : ℕ) => c • w i

def MvPolynomial.weightedTotalDegree' {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] (w : σ → M) (p : MvPolynomial σ R) : WithBot M

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

Equations

• MvPolynomial.weightedTotalDegree' w p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => ↑((MvPolynomial.weightedDegree w) s)

theorem MvPolynomial.weightedTotalDegree'_eq_bot_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] (w : σ → M) (p : MvPolynomial σ R) : MvPolynomial.weightedTotalDegree' w 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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] (w : σ → M) : MvPolynomial.weightedTotalDegree' w 0 = ⊥

The weightedTotalDegree' of the zero polynomial is ⊥.

def MvPolynomial.weightedTotalDegree {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] [OrderBot M] (w : σ → M) (p : MvPolynomial σ 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

• MvPolynomial.weightedTotalDegree w p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => (MvPolynomial.weightedDegree w) s

theorem MvPolynomial.weightedTotalDegree_coe {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] [OrderBot M] (w : σ → M) (p : MvPolynomial σ R) (hp : p ≠ 0) : MvPolynomial.weightedTotalDegree' w p = ↑(MvPolynomial.weightedTotalDegree w p)

This lemma relates weightedTotalDegree and weightedTotalDegree'.

theorem MvPolynomial.weightedTotalDegree_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] [OrderBot M] (w : σ → M) : MvPolynomial.weightedTotalDegree w 0 = ⊥

The weightedTotalDegree of the zero polynomial is ⊥.

theorem MvPolynomial.le_weightedTotalDegree {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] [OrderBot M] (w : σ → M) {φ : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : d ∈ MvPolynomial.support φ) : (MvPolynomial.weightedDegree w) d ≤ MvPolynomial.weightedTotalDegree w φ

def MvPolynomial.IsWeightedHomogeneous {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (φ : MvPolynomial σ R) (m : M) : Prop

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

Equations

• MvPolynomial.IsWeightedHomogeneous w φ m = ∀ ⦃d : σ →₀ ℕ⦄, MvPolynomial.coeff d φ ≠ 0 → (MvPolynomial.weightedDegree w) d = m

def MvPolynomial.weightedHomogeneousSubmodule (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (m : M) : Submodule R (MvPolynomial σ R)

The submodule of homogeneous MvPolynomials of degree n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MvPolynomial.mem_weightedHomogeneousSubmodule (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (m : M) (p : MvPolynomial σ R) : p ∈ MvPolynomial.weightedHomogeneousSubmodule R w m ↔ MvPolynomial.IsWeightedHomogeneous w p m

theorem MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (m : M) : MvPolynomial.weightedHomogeneousSubmodule R w m = Finsupp.supported R R {d : σ →₀ ℕ | (MvPolynomial.weightedDegree w) 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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (m : M) (n : M) : MvPolynomial.weightedHomogeneousSubmodule R w m * MvPolynomial.weightedHomogeneousSubmodule R w n ≤ MvPolynomial.weightedHomogeneousSubmodule 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 MvPolynomial.isWeightedHomogeneous_monomial {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (d : σ →₀ ℕ) (r : R) {m : M} (hm : (MvPolynomial.weightedDegree w) d = m) : MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.monomial d) r) m

Monomials are weighted homogeneous.

theorem MvPolynomial.isWeightedHomogeneous_of_total_degree_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] [SemilatticeSup M] [OrderBot M] (w : σ → M) {p : MvPolynomial σ R} (hp : MvPolynomial.weightedTotalDegree w p = ⊥) : MvPolynomial.IsWeightedHomogeneous w p ⊥

A polynomial of weightedTotalDegree ⊥ is weighted_homogeneous of degree ⊥.

theorem MvPolynomial.isWeightedHomogeneous_C {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (m : M) : MvPolynomial.IsWeightedHomogeneous w 0 m

0 is weighted homogeneous of any degree.

theorem MvPolynomial.isWeightedHomogeneous_one (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) : MvPolynomial.IsWeightedHomogeneous w 1 0

1 is weighted homogeneous of degree 0.

theorem MvPolynomial.isWeightedHomogeneous_X (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (i : σ) : MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.X i) (w 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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {φ : MvPolynomial σ R} {n : M} {w : σ → M} (hφ : MvPolynomial.IsWeightedHomogeneous w φ n) (d : σ →₀ ℕ) (hd : (MvPolynomial.weightedDegree w) d ≠ n) : MvPolynomial.coeff d φ = 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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {φ : MvPolynomial σ R} {m : M} {n : M} {w : σ → M} (hφ : φ ≠ 0) (hm : MvPolynomial.IsWeightedHomogeneous w φ m) (hn : MvPolynomial.IsWeightedHomogeneous w φ n) : 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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} {n : M} {w : σ → M} (hφ : MvPolynomial.IsWeightedHomogeneous w φ n) (hψ : MvPolynomial.IsWeightedHomogeneous w ψ n) : MvPolynomial.IsWeightedHomogeneous w (φ + ψ) n

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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {ι : Type u_4} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : M) {w : σ → M} (h : ∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) n) : MvPolynomial.IsWeightedHomogeneous w (Finset.sum s fun (i : ι) => φ 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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} {m : M} {n : M} {w : σ → M} (hφ : MvPolynomial.IsWeightedHomogeneous w φ m) (hψ : MvPolynomial.IsWeightedHomogeneous w ψ n) : MvPolynomial.IsWeightedHomogeneous w (φ * ψ) (m + n)

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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {ι : Type u_4} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → M) {w : σ → M} : (∀ i ∈ s, MvPolynomial.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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {φ : MvPolynomial σ R} {n : M} [SemilatticeSup M] {w : σ → M} (hφ : MvPolynomial.IsWeightedHomogeneous w φ n) (h : φ ≠ 0) : MvPolynomial.weightedTotalDegree' w φ = ↑n

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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} : SetLike.GradedMonoid (MvPolynomial.weightedHomogeneousSubmodule R w)

The weighted homogeneous submodules form a graded monoid.

Equations

• ⋯ = ⋯

def MvPolynomial.weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (n : M) : MvPolynomial σ R →ₗ[R] MvPolynomial σ R

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.

theorem MvPolynomial.coeff_weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (n : M) (φ : MvPolynomial σ R) [DecidableEq M] (d : σ →₀ ℕ) : MvPolynomial.coeff d ((MvPolynomial.weightedHomogeneousComponent w n) φ) = if (MvPolynomial.weightedDegree w) d = n then MvPolynomial.coeff d φ else 0

theorem MvPolynomial.weightedHomogeneousComponent_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (n : M) (φ : MvPolynomial σ R) [DecidableEq M] : (MvPolynomial.weightedHomogeneousComponent w n) φ = Finset.sum (Finset.filter (fun (d : σ →₀ ℕ) => (MvPolynomial.weightedDegree w) d = n) (MvPolynomial.support φ)) fun (d : σ →₀ ℕ) => (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)

theorem MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (n : M) (φ : MvPolynomial σ R) : MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.weightedHomogeneousComponent w n) φ) n

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} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (φ : MvPolynomial σ R) (m : M) : (MvPolynomial.weightedHomogeneousComponent w m) φ ∈ MvPolynomial.weightedHomogeneousSubmodule R w m

@[simp]

theorem MvPolynomial.weightedHomogeneousComponent_C_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (φ : MvPolynomial σ R) (n : M) (r : R) : (MvPolynomial.weightedHomogeneousComponent w n) (MvPolynomial.C r * φ) = MvPolynomial.C r * (MvPolynomial.weightedHomogeneousComponent w n) φ

theorem MvPolynomial.weightedHomogeneousComponent_eq_zero' {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (n : M) (φ : MvPolynomial σ R) (h : ∀ d ∈ MvPolynomial.support φ, (MvPolynomial.weightedDegree w) d ≠ n) : (MvPolynomial.weightedHomogeneousComponent w n) φ = 0

theorem MvPolynomial.weightedHomogeneousComponent_eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (n : M) (φ : MvPolynomial σ R) [SemilatticeSup M] [OrderBot M] (h : MvPolynomial.weightedTotalDegree w φ < n) : (MvPolynomial.weightedHomogeneousComponent w n) φ = 0

theorem MvPolynomial.weightedHomogeneousComponent_finsupp {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} (φ : MvPolynomial σ R) : Set.Finite (Function.support fun (m : M) => (MvPolynomial.weightedHomogeneousComponent w m) φ)

theorem MvPolynomial.sum_weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (φ : MvPolynomial σ R) : (finsum fun (m : M) => (MvPolynomial.weightedHomogeneousComponent w m) φ) = φ

Every polynomial is the sum of its weighted homogeneous components.

theorem MvPolynomial.finsum_weightedHomogeneousComponent {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) (φ : MvPolynomial σ R) : (finsum fun (m : M) => (MvPolynomial.weightedHomogeneousComponent w m) φ) = φ

theorem MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} {m : M} {p : MvPolynomial σ R} (hp : MvPolynomial.IsWeightedHomogeneous w p m) : (MvPolynomial.weightedHomogeneousComponent w m) p = p

theorem MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} {m : M} (n : M) {p : MvPolynomial σ R} (hp : MvPolynomial.IsWeightedHomogeneous w p m) : n ≠ m → (MvPolynomial.weightedHomogeneousComponent w n) p = 0

theorem MvPolynomial.weightedHomogeneousComponent_weighted_homogeneous_polynomial {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} [DecidableEq M] (m : M) (n : M) (p : MvPolynomial σ R) (h : p ∈ MvPolynomial.weightedHomogeneousSubmodule R w n) : (MvPolynomial.weightedHomogeneousComponent w m) p = 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} [CommSemiring R] {σ : Type u_3} [CanonicallyOrderedAddCommMonoid M] {w : σ → M} (φ : MvPolynomial σ R) [NoZeroSMulDivisors ℕ M] (hw : ∀ (i : σ), w i ≠ 0) : (MvPolynomial.weightedHomogeneousComponent w 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)

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

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

Equations

• MvPolynomial.NonTorsionWeight w = ∀ (n : ℕ) (x : σ), n • w x = 0 → n = 0

theorem MvPolynomial.nonTorsionWeight_of {M : Type u_2} {σ : Type u_3} [CanonicallyOrderedAddCommMonoid M] {w : σ → M} [NoZeroSMulDivisors ℕ M] (hw : ∀ (i : σ), w i ≠ 0) : MvPolynomial.NonTorsionWeight w

theorem MvPolynomial.weightedDegree_eq_zero_iff {M : Type u_2} {σ : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] {w : σ → M} (hw : MvPolynomial.NonTorsionWeight w) {m : σ →₀ ℕ} : (MvPolynomial.weightedDegree w) 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} [CommSemiring R] {σ : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] {w : σ → M} {p : MvPolynomial σ R} : MvPolynomial.IsWeightedHomogeneous w p 0 ↔ MvPolynomial.weightedTotalDegree w p = 0

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} [CommSemiring R] {σ : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] {w : σ → M} (hw : MvPolynomial.NonTorsionWeight w) (p : MvPolynomial σ R) : MvPolynomial.weightedTotalDegree w p = 0 ↔ ∀ m ∈ MvPolynomial.support p, ∀ (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.