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.

weight

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 = p.support.sup fun (s : σ →₀ ℕ) => ↑((Finsupp.weight 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 = p.support.sup fun (s : σ →₀ ℕ) => (Finsupp.weight 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 ∈ φ.support) : (Finsupp.weight 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 → (Finsupp.weight 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

• MvPolynomial.weightedHomogeneousSubmodule R w m = { carrier := {x : MvPolynomial σ R | MvPolynomial.IsWeightedHomogeneous w x m}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[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 : σ →₀ ℕ | (Finsupp.weight 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 | weight 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 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 : (Finsupp.weight 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 : (Finsupp.weight 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 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} {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 (∑ i ∈ s, φ 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} {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.pow {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {φ : MvPolynomial σ R} {m : M} {w : σ → M} (hφ : MvPolynomial.IsWeightedHomogeneous w φ m) (n : ℕ) : MvPolynomial.IsWeightedHomogeneous w (φ ^ n) (n • m)

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 (∏ i ∈ s, φ i) (∑ i ∈ s, 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.

theorem MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid {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.

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

• MvPolynomial.weightedHomogeneousComponent w n = (Finsupp.supported R R {d : σ →₀ ℕ | (Finsupp.weight w) d = n}).subtype ∘ₗ Finsupp.restrictDom R R {d : σ →₀ ℕ | (Finsupp.weight w) d = n}

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 (Finsupp.weight 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) φ = ∑ d ∈ Finset.filter (fun (d : σ →₀ ℕ) => (Finsupp.weight w) d = n) φ.support, (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 ∈ φ.support, (Finsupp.weight 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) : (Function.support fun (m : M) => (MvPolynomial.weightedHomogeneousComponent w m) φ).Finite

theorem MvPolynomial.sum_weightedHomogeneousComponent {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) φ = φ

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) : ∑ᶠ (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_of_mem {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} [DecidableEq 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.

theorem MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_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.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] {w : σ → M} {m n : M} {p : MvPolynomial σ R} (hp : MvPolynomial.IsWeightedHomogeneous w p m) (hn : n ≠ m) : (MvPolynomial.weightedHomogeneousComponent w n) p = 0

theorem MvPolynomial.DirectSum.coeLinearMap_eq_dfinsupp_sum (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) [DecidableEq σ] [DecidableEq R] [DecidableEq M] (x : DirectSum M fun (i : M) => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) : (DirectSum.coeLinearMap fun (i : M) => MvPolynomial.weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun (x : M) (x_1 : ↥(MvPolynomial.weightedHomogeneousSubmodule R w x)) => ↑x_1

theorem MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) [DecidableEq σ] [DecidableEq R] [DecidableEq M] (x : DirectSum M fun (i : M) => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) : (DirectSum.coeAddMonoidHom fun (i : M) => MvPolynomial.weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun (x : M) (x_1 : ↥(MvPolynomial.weightedHomogeneousSubmodule R w x)) => ↑x_1

theorem MvPolynomial.DirectSum.coeLinearMap_eq_finsum (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) [DecidableEq M] (x : DirectSum M fun (i : M) => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) : (DirectSum.coeLinearMap fun (i : M) => MvPolynomial.weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)

theorem MvPolynomial.weightedHomogeneousComponent_directSum (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} [AddCommMonoid M] (w : σ → M) [DecidableEq M] (x : DirectSum M fun (i : M) => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) (m : M) : (MvPolynomial.weightedHomogeneousComponent w m) ((DirectSum.coeLinearMap fun (i : M) => MvPolynomial.weightedHomogeneousSubmodule R w i) x) = ↑(x m)

@[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 : σ →₀ ℕ} : (Finsupp.weight 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 ∈ p.support, ∀ (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.

theorem MvPolynomial.weightedHomogeneousComponent_eq_zero_of_not_mem {R : Type u_1} {M : Type u_2} [CommSemiring R] {σ : Type u_3} (w : σ → M) [AddCommMonoid M] [DecidableEq M] (φ : MvPolynomial σ R) (i : M) (hi : i ∉ Finset.image (⇑(Finsupp.weight w)) φ.support) : (MvPolynomial.weightedHomogeneousComponent w i) φ = 0

def MvPolynomial.decompose' (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} (w : σ → M) [AddCommMonoid M] [DecidableEq M] (φ : MvPolynomial σ R) : DirectSum M fun (i : M) => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)

The decompose' argument of weightedDecomposition.

Equations

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

theorem MvPolynomial.decompose'_apply (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} (w : σ → M) [AddCommMonoid M] [DecidableEq M] (φ : MvPolynomial σ R) (m : M) : ↑((MvPolynomial.decompose' R w φ) m) = (MvPolynomial.weightedHomogeneousComponent w m) φ

def MvPolynomial.weightedDecomposition (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} (w : σ → M) [AddCommMonoid M] [DecidableEq M] : DirectSum.Decomposition (MvPolynomial.weightedHomogeneousSubmodule R w)

Given a weight w, the decomposition of MvPolynomial σ R into weighted homogeneous submodules

Equations

• MvPolynomial.weightedDecomposition R w = { decompose' := MvPolynomial.decompose' R w, left_inv := ⋯, right_inv := ⋯ }

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

Given a weight, MvPolynomial as a graded algebra

Equations

• MvPolynomial.weightedGradedAlgebra R w = GradedRing.mk

theorem MvPolynomial.weightedDecomposition.decompose'_eq (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} (w : σ → M) [AddCommMonoid M] [DecidableEq M] : DirectSum.Decomposition.decompose' = fun (φ : MvPolynomial σ R) => (DirectSum.mk (fun (i : M) => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(Finsupp.weight w)) φ.support)) fun (m : ↑↑(Finset.image (⇑(Finsupp.weight w)) φ.support)) => ⟨(MvPolynomial.weightedHomogeneousComponent w ↑m) φ, ⋯⟩

theorem MvPolynomial.weightedDecomposition.decompose'_apply (R : Type u_1) {M : Type u_2} [CommSemiring R] {σ : Type u_3} (w : σ → M) [AddCommMonoid M] [DecidableEq M] (φ : MvPolynomial σ R) (m : M) : ↑((DirectSum.Decomposition.decompose' φ) m) = (MvPolynomial.weightedHomogeneousComponent w m) φ