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.

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

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

Equations

Instances For

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

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

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

Instances For

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

weightedTotalDegree' w p = ↑(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) :

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

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

Equations

Instances For

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

Instances For

@[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 ∈ weightedHomogeneousSubmodule R w m ↔ 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) :

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

weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤ 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) :

IsWeightedHomogeneous w ((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 : weightedTotalDegree w p = ⊥) :

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

IsWeightedHomogeneous w (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) :

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

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

IsWeightedHomogeneous w (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φ : IsWeightedHomogeneous w φ n) (d : σ →₀ ℕ) (hd : (Finsupp.weight w) d ≠ n) :

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 : IsWeightedHomogeneous w φ m) (hn : 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φ : IsWeightedHomogeneous w φ n) (hψ : IsWeightedHomogeneous w ψ n) :

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, IsWeightedHomogeneous w (φ i) n) :

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φ : IsWeightedHomogeneous w φ m) (hψ : IsWeightedHomogeneous w ψ n) :

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φ : IsWeightedHomogeneous w φ m) (n : ℕ) :

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, IsWeightedHomogeneous w (φ i) (n i)) → 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φ : IsWeightedHomogeneous w φ n) (h : φ ≠ 0) :

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 (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

Instances For

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 : σ →₀ ℕ) :

coeff d ((weightedHomogeneousComponent w n) φ) = if (Finsupp.weight w) d = n then 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] :

(weightedHomogeneousComponent w n) φ = ∑ d ∈ φ.support with (Finsupp.weight w) d = n, (monomial d) (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) :

IsWeightedHomogeneous w ((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) :

(weightedHomogeneousComponent w m) φ ∈ 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) :

(weightedHomogeneousComponent w n) (C r * φ) = C r * (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) :

(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 : weightedTotalDegree w φ < n) :

(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) => (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), (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), (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 : IsWeightedHomogeneous w p m) :

(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 : IsWeightedHomogeneous w p m) :

n ≠ m → (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 ∈ weightedHomogeneousSubmodule R w n) :

(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 : IsWeightedHomogeneous w p m) :

(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 : IsWeightedHomogeneous w p m) (hn : n ≠ m) :

(weightedHomogeneousComponent w n) p = 0

theorem MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum (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) => ↥(weightedHomogeneousSubmodule R w i)) :

(DirectSum.coeLinearMap fun (i : M) => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun (x : M) (x_1 : ↥(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) => ↥(weightedHomogeneousSubmodule R w i)) :

(DirectSum.coeAddMonoidHom fun (i : M) => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun (x : M) (x_1 : ↥(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) => ↥(weightedHomogeneousSubmodule R w i)) :

(DirectSum.coeLinearMap fun (i : M) => 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) => ↥(weightedHomogeneousSubmodule R w i)) (m : M) :

(weightedHomogeneousComponent w m) ((DirectSum.coeLinearMap fun (i : M) => 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} [AddCommMonoid M] [PartialOrder M] {w : σ → M} (φ : MvPolynomial σ R) [CanonicallyOrderedAdd M] [NoZeroSMulDivisors ℕ M] (hw : ∀ (i : σ), w i ≠ 0) :

(weightedHomogeneousComponent w 0) φ = C (coeff 0 φ)

If M is a canonically OrderedAddCommMonoid, then the weightedHomogeneousComponent of weighted degree 0 of a polynomial is its constant coefficient.

def MvPolynomial.NonTorsionWeight {M : Type u_2} {σ : Type u_3} [AddCommMonoid M] (w : σ → M) :

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

Equations

Instances For

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

NonTorsionWeight w

theorem MvPolynomial.weightedDegree_eq_zero_iff {M : Type u_2} {σ : Type u_3} [AddCommMonoid M] [PartialOrder M] {w : σ → M} [CanonicallyOrderedAdd M] (hw : 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} [AddCommMonoid M] [LinearOrder M] [OrderBot M] [CanonicallyOrderedAdd M] {w : σ → M} {p : MvPolynomial σ R} :

IsWeightedHomogeneous w p 0 ↔ weightedTotalDegree w p = 0

A multivariate 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} [AddCommMonoid M] [LinearOrder M] [OrderBot M] [CanonicallyOrderedAdd M] {w : σ → M} (hw : NonTorsionWeight w) (p : MvPolynomial σ R) :

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

(weightedHomogeneousComponent w i) φ = 0

@[deprecated MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem (since := "2025-05-23")]

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

(weightedHomogeneousComponent w i) φ = 0

Alias of MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem.

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) => ↥(weightedHomogeneousSubmodule R w i)

The decompose' argument of weightedDecomposition.

Equations

Instances For

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

↑((decompose' R w φ) m) = (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 (weightedHomogeneousSubmodule R w)

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

Equations

Instances For

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

GradedAlgebra (weightedHomogeneousSubmodule R w)

Given a weight, MvPolynomial as a graded algebra

Equations

Instances For

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) => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(Finsupp.weight w)) φ.support)) fun (m : ↑↑(Finset.image (⇑(Finsupp.weight w)) φ.support)) => ⟨(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) = (weightedHomogeneousComponent w m) φ