Homogeneous polynomials #

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

Main definitions/lemmas #

• IsHomogeneous φ n: a predicate that asserts that φ is homogeneous of degree n.
• homogeneousSubmodule σ R n: the submodule of homogeneous polynomials of degree n.
• homogeneousComponent n: the additive morphism that projects polynomials onto their summand that is homogeneous of degree n.
• sum_homogeneousComponent: every polynomial is the sum of its homogeneous components.
def MvPolynomial.IsHomogeneous {σ : Type u_1} {R : Type u_3} [] (φ : ) (n : ) :

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

Equations
• φ.IsHomogeneous n =
Instances For
theorem MvPolynomial.weightedTotalDegree_one {σ : Type u_1} {R : Type u_3} [] (φ : ) :
= φ.totalDegree
def MvPolynomial.homogeneousSubmodule (σ : Type u_1) (R : Type u_3) [] (n : ) :

The submodule of homogeneous MvPolynomials of degree n.

Equations
• = { carrier := {x : | x.IsHomogeneous n}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem MvPolynomial.weightedHomogeneousSubmodule_one (σ : Type u_1) (R : Type u_3) [] (n : ) :
@[simp]
theorem MvPolynomial.mem_homogeneousSubmodule {σ : Type u_1} {R : Type u_3} [] (n : ) (p : ) :
p.IsHomogeneous n
theorem MvPolynomial.homogeneousSubmodule_eq_finsupp_supported (σ : Type u_1) (R : Type u_3) [] (n : ) :
= Finsupp.supported R R {d : σ →₀ | d.degree = n}

While equal, the former has a convenient definitional reduction.

theorem MvPolynomial.homogeneousSubmodule_mul {σ : Type u_1} {R : Type u_3} [] (m : ) (n : ) :
theorem MvPolynomial.isHomogeneous_monomial {σ : Type u_1} {R : Type u_3} [] {d : σ →₀ } (r : R) {n : } (hn : d.degree = n) :
().IsHomogeneous n
theorem MvPolynomial.totalDegree_eq_zero_iff (σ : Type u_1) {R : Type u_3} [] (p : ) :
p.totalDegree = 0 mp.support, ∀ (x : σ), m x = 0
theorem MvPolynomial.totalDegree_zero_iff_isHomogeneous (σ : Type u_1) {R : Type u_3} [] {p : } :
p.totalDegree = 0 p.IsHomogeneous 0
theorem MvPolynomial.isHomogeneous_of_totalDegree_zero (σ : Type u_1) {R : Type u_3} [] {p : } :
p.totalDegree = 0p.IsHomogeneous 0

Alias of the forward direction of MvPolynomial.totalDegree_zero_iff_isHomogeneous.

theorem MvPolynomial.isHomogeneous_C (σ : Type u_1) {R : Type u_3} [] (r : R) :
(MvPolynomial.C r).IsHomogeneous 0
theorem MvPolynomial.isHomogeneous_zero (σ : Type u_1) (R : Type u_3) [] (n : ) :
theorem MvPolynomial.isHomogeneous_one (σ : Type u_1) (R : Type u_3) [] :
theorem MvPolynomial.isHomogeneous_X {σ : Type u_1} (R : Type u_3) [] (i : σ) :
().IsHomogeneous 1
theorem MvPolynomial.IsHomogeneous.coeff_eq_zero {σ : Type u_1} {R : Type u_3} [] {φ : } {n : } (hφ : φ.IsHomogeneous n) {d : σ →₀ } (hd : d.degree n) :
= 0
theorem MvPolynomial.IsHomogeneous.inj_right {σ : Type u_1} {R : Type u_3} [] {φ : } {m : } {n : } (hm : φ.IsHomogeneous m) (hn : φ.IsHomogeneous n) (hφ : φ 0) :
m = n
theorem MvPolynomial.IsHomogeneous.add {σ : Type u_1} {R : Type u_3} [] {φ : } {ψ : } {n : } (hφ : φ.IsHomogeneous n) (hψ : ψ.IsHomogeneous n) :
(φ + ψ).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.sum {σ : Type u_1} {R : Type u_3} [] {ι : Type u_5} (s : ) (φ : ι) (n : ) (h : is, (φ i).IsHomogeneous n) :
(is, φ i).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.mul {σ : Type u_1} {R : Type u_3} [] {φ : } {ψ : } {m : } {n : } (hφ : φ.IsHomogeneous m) (hψ : ψ.IsHomogeneous n) :
(φ * ψ).IsHomogeneous (m + n)
theorem MvPolynomial.IsHomogeneous.prod {σ : Type u_1} {R : Type u_3} [] {ι : Type u_5} (s : ) (φ : ι) (n : ι) (h : is, (φ i).IsHomogeneous (n i)) :
(is, φ i).IsHomogeneous (is, n i)
theorem MvPolynomial.IsHomogeneous.C_mul {σ : Type u_1} {R : Type u_3} [] {φ : } {m : } (hφ : φ.IsHomogeneous m) (r : R) :
(MvPolynomial.C r * φ).IsHomogeneous m
theorem MvPolynomial.isHomogeneous_C_mul_X {σ : Type u_1} {R : Type u_3} [] (r : R) (i : σ) :
(MvPolynomial.C r * ).IsHomogeneous 1
@[deprecated MvPolynomial.isHomogeneous_C_mul_X]
theorem MvPolynomial.C_mul_X {σ : Type u_1} {R : Type u_3} [] (r : R) (i : σ) :
(MvPolynomial.C r * ).IsHomogeneous 1

Alias of MvPolynomial.isHomogeneous_C_mul_X.

theorem MvPolynomial.IsHomogeneous.pow {σ : Type u_1} {R : Type u_3} [] {φ : } {m : } (hφ : φ.IsHomogeneous m) (n : ) :
(φ ^ n).IsHomogeneous (m * n)
theorem MvPolynomial.isHomogeneous_X_pow {σ : Type u_1} {R : Type u_3} [] (i : σ) (n : ) :
().IsHomogeneous n
theorem MvPolynomial.isHomogeneous_C_mul_X_pow {σ : Type u_1} {R : Type u_3} [] (r : R) (i : σ) (n : ) :
(MvPolynomial.C r * ).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] {φ : } {m : } {n : } (hφ : φ.IsHomogeneous m) (f : R →+* ) (g : σ) (hf : ∀ (r : R), (f r).IsHomogeneous 0) (hg : ∀ (i : σ), (g i).IsHomogeneous n) :
().IsHomogeneous (n * m)
theorem MvPolynomial.IsHomogeneous.map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] {φ : } {n : } (hφ : φ.IsHomogeneous n) (f : R →+* S) :
(() φ).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] {φ : } {m : } {n : } [Algebra R S] (hφ : φ.IsHomogeneous m) (g : σ) (hg : ∀ (i : σ), (g i).IsHomogeneous n) :
( φ).IsHomogeneous (n * m)
theorem MvPolynomial.IsHomogeneous.neg {R : Type u_5} {σ : Type u_6} [] {φ : } {n : } (hφ : φ.IsHomogeneous n) :
(-φ).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.sub {R : Type u_5} {σ : Type u_6} [] {φ : } {ψ : } {n : } (hφ : φ.IsHomogeneous n) (hψ : ψ.IsHomogeneous n) :
(φ - ψ).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.totalDegree_le {σ : Type u_1} {R : Type u_3} [] {φ : } {n : } (hφ : φ.IsHomogeneous n) :
φ.totalDegree n

The homogeneous degree bounds the total degree.

See also MvPolynomial.IsHomogeneous.totalDegree when φ is non-zero.

theorem MvPolynomial.IsHomogeneous.totalDegree {σ : Type u_1} {R : Type u_3} [] {φ : } {n : } (hφ : φ.IsHomogeneous n) (h : φ 0) :
φ.totalDegree = n
theorem MvPolynomial.IsHomogeneous.rename_isHomogeneous {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {φ : } {n : } {f : στ} (h : φ.IsHomogeneous n) :
( φ).IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {φ : } {n : } {f : στ} (hf : ) :
( φ).IsHomogeneous n φ.IsHomogeneous n
theorem MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous {R : Type u_3} [] {N : } {φ : MvPolynomial (Fin (N + 1)) R} {n : } (hφ : φ.IsHomogeneous n) (i : ) (j : ) (h : i + j = n) :
(( φ).coeff i).IsHomogeneous j
theorem MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm {σ : Type u_1} {R : Type u_3} [] {n : } [hσ : ] {p : Polynomial ()} (hp : (.symm p).IsHomogeneous n) (i : ) (j : ) (h : i + j = n) :
(p.coeff i).IsHomogeneous j
theorem MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card {R : Type u_5} {σ : Type u_6} [] [] {F : } {n : } (hF : F.IsHomogeneous n) (h : ∀ (r : σR), F = 0) (hnR : n ) :
F = 0

See MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero for a version that assumes Infinite R.

theorem MvPolynomial.IsHomogeneous.funext_of_le_card {R : Type u_5} {σ : Type u_6} [] [] {F : } {G : } {n : } (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ (r : σR), F = G) (hnR : n ) :
F = G

See MvPolynomial.IsHomogeneous.funext for a version that assumes Infinite R.

theorem MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero {R : Type u_5} {σ : Type u_6} [] [] [] {F : } {n : } (hF : F.IsHomogeneous n) (h : ∀ (r : σR), F = 0) :
F = 0

See MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card for a version that assumes n ≤ #R.

theorem MvPolynomial.IsHomogeneous.funext {R : Type u_5} {σ : Type u_6} [] [] [] {F : } {G : } {n : } (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ (r : σR), F = G) :
F = G

See MvPolynomial.IsHomogeneous.funext_of_le_card for a version that assumes n ≤ #R.

The homogeneous submodules form a graded ring. This instance is used by DirectSum.commSemiring and DirectSum.algebra.

Equations
• =
def MvPolynomial.homogeneousComponent {σ : Type u_1} {R : Type u_3} [] (n : ) :

homogeneousComponent n φ is the part of φ that is homogeneous of degree n. See sum_homogeneousComponent for the statement that φ is equal to the sum of all its homogeneous components.

Equations
Instances For
theorem MvPolynomial.homogeneousComponent_mem {σ : Type u_1} {R : Type u_3} [] (n : ) (φ : ) :
theorem MvPolynomial.coeff_homogeneousComponent {σ : Type u_1} {R : Type u_3} [] (n : ) (φ : ) (d : σ →₀ ) :
= if d.degree = n then else 0
theorem MvPolynomial.homogeneousComponent_apply {σ : Type u_1} {R : Type u_3} [] (n : ) (φ : ) :
= dFinset.filter (fun (d : σ →₀ ) => d.degree = n) φ.support, ()
theorem MvPolynomial.homogeneousComponent_isHomogeneous {σ : Type u_1} {R : Type u_3} [] (n : ) (φ : ) :
.IsHomogeneous n
@[simp]
theorem MvPolynomial.homogeneousComponent_zero {σ : Type u_1} {R : Type u_3} [] (φ : ) :
= MvPolynomial.C ()
@[simp]
theorem MvPolynomial.homogeneousComponent_C_mul {σ : Type u_1} {R : Type u_3} [] (φ : ) (n : ) (r : R) :
(MvPolynomial.C r * φ) = MvPolynomial.C r *
theorem MvPolynomial.homogeneousComponent_eq_zero' {σ : Type u_1} {R : Type u_3} [] (n : ) (φ : ) (h : dφ.support, d.degree n) :
theorem MvPolynomial.homogeneousComponent_eq_zero {σ : Type u_1} {R : Type u_3} [] (n : ) (φ : ) (h : φ.totalDegree < n) :
theorem MvPolynomial.sum_homogeneousComponent {σ : Type u_1} {R : Type u_3} [] (φ : ) :
iFinset.range (φ.totalDegree + 1), = φ
theorem MvPolynomial.homogeneousComponent_of_mem {σ : Type u_1} {R : Type u_3} [] {m : } {n : } {p : } (h : ) :
= if m = n then p else 0
theorem MvPolynomial.HomogeneousSubmodule.gradedMonoid {σ : Type u_1} {R : Type u_3} [] :

The homogeneous submodules form a graded ring. This instance is used by DirectSum.commSemiring and DirectSum.algebra.

@[reducible, inline]
abbrev MvPolynomial.decomposition {σ : Type u_1} {R : Type u_3} [] :

The decomposition of MvPolynomial σ R into homogeneous submodules.

Equations
• MvPolynomial.decomposition =
Instances For
@[reducible, inline]
abbrev MvPolynomial.gradedAlgebra {σ : Type u_1} {R : Type u_3} [] :

MvPolynomial σ R as a graded algebra, graded by the degree. We do not make this a global instance because one may want to consider a different graded algebra structure on MvPolynomial σ R, induced by another weight function. To make it a local instance, you may use attribute [local instance] MvPolynomial.gradedAlgebra.

Equations