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 degreen.homogeneousSubmodule σ R n: the submodule of homogeneous polynomials of degreen.homogeneousComponent n: the additive morphism that projects polynomials onto their summand that is homogeneous of degreen.sum_homogeneousComponent: every polynomial is the sum of its homogeneous components.
def
MvPolynomial.IsHomogeneous
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
:
A multivariate polynomial φ is homogeneous of degree n
if all monomials occurring in φ have degree n.
Equations
- φ.IsHomogeneous n = MvPolynomial.IsWeightedHomogeneous 1 φ n
Instances For
theorem
MvPolynomial.weightedTotalDegree_one
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.weightedTotalDegree_rename_of_injective
{R : Type u_3}
[CommSemiring R]
{σ : Type u_5}
{τ : Type u_6}
{e : σ → τ}
{w : τ → ℕ}
{P : MvPolynomial σ R}
(he : Function.Injective e)
:
def
MvPolynomial.homogeneousSubmodule
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
Submodule R (MvPolynomial σ R)
The submodule of homogeneous MvPolynomials of degree n.
Equations
- MvPolynomial.homogeneousSubmodule σ R n = { carrier := {x : MvPolynomial σ R | x.IsHomogeneous n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
MvPolynomial.weightedHomogeneousSubmodule_one
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
@[simp]
theorem
MvPolynomial.mem_homogeneousSubmodule
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
While equal, the former has a convenient definitional reduction.
theorem
MvPolynomial.homogeneousSubmodule_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(m n : ℕ)
:
theorem
MvPolynomial.isHomogeneous_monomial
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{d : σ →₀ ℕ}
(r : R)
{n : ℕ}
(hn : d.degree = n)
:
((monomial d) r).IsHomogeneous n
theorem
MvPolynomial.totalDegree_eq_zero_iff
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.totalDegree_zero_iff_isHomogeneous
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
{p : MvPolynomial σ R}
:
theorem
MvPolynomial.isHomogeneous_of_totalDegree_zero
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
{p : MvPolynomial σ R}
:
p.totalDegree = 0 → p.IsHomogeneous 0
Alias of the forward direction of MvPolynomial.totalDegree_zero_iff_isHomogeneous.
theorem
MvPolynomial.isHomogeneous_C
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
(r : R)
:
(C r).IsHomogeneous 0
theorem
MvPolynomial.isHomogeneous_zero
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
IsHomogeneous 0 n
theorem
MvPolynomial.isHomogeneous_one
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
:
IsHomogeneous 1 0
theorem
MvPolynomial.isHomogeneous_X
{σ : Type u_1}
(R : Type u_3)
[CommSemiring R]
(i : σ)
:
(X i).IsHomogeneous 1
theorem
MvPolynomial.IsHomogeneous.coeff_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
{d : σ →₀ ℕ}
(hd : d.degree ≠ n)
:
theorem
MvPolynomial.IsHomogeneous.inj_right
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m n : ℕ}
(hm : φ.IsHomogeneous m)
(hn : φ.IsHomogeneous n)
(hφ : φ ≠ 0)
:
theorem
MvPolynomial.IsHomogeneous.add
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ ψ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(hψ : ψ.IsHomogeneous n)
:
(φ + ψ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.sum
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{ι : Type u_5}
(s : Finset ι)
(φ : ι → MvPolynomial σ R)
(n : ℕ)
(h : ∀ i ∈ s, (φ i).IsHomogeneous n)
:
(∑ i ∈ s, φ i).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ ψ : MvPolynomial σ R}
{m n : ℕ}
(hφ : φ.IsHomogeneous m)
(hψ : ψ.IsHomogeneous n)
:
(φ * ψ).IsHomogeneous (m + n)
theorem
MvPolynomial.IsHomogeneous.prod
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{ι : Type u_5}
(s : Finset ι)
(φ : ι → MvPolynomial σ R)
(n : ι → ℕ)
(h : ∀ i ∈ s, (φ i).IsHomogeneous (n i))
:
(∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
theorem
MvPolynomial.IsHomogeneous.C_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
(hφ : φ.IsHomogeneous m)
(r : R)
:
(C r * φ).IsHomogeneous m
theorem
MvPolynomial.isHomogeneous_C_mul_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
:
(C r * X i).IsHomogeneous 1
theorem
MvPolynomial.IsHomogeneous.pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
(hφ : φ.IsHomogeneous m)
(n : ℕ)
:
(φ ^ n).IsHomogeneous (m * n)
theorem
MvPolynomial.isHomogeneous_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(i : σ)
(n : ℕ)
:
(X i ^ n).IsHomogeneous n
theorem
MvPolynomial.isHomogeneous_C_mul_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
(n : ℕ)
:
(C r * X i ^ n).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.eval₂
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{m n : ℕ}
(hφ : φ.IsHomogeneous m)
(f : R →+* MvPolynomial τ S)
(g : σ → MvPolynomial τ S)
(hf : ∀ (r : R), (f r).IsHomogeneous 0)
(hg : ∀ (i : σ), (g i).IsHomogeneous n)
:
(MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
theorem
MvPolynomial.IsHomogeneous.map
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(f : R →+* S)
:
((MvPolynomial.map f) φ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.aeval
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{m n : ℕ}
[Algebra R S]
(hφ : φ.IsHomogeneous m)
(g : σ → MvPolynomial τ S)
(hg : ∀ (i : σ), (g i).IsHomogeneous n)
:
((MvPolynomial.aeval g) φ).IsHomogeneous (n * m)
theorem
MvPolynomial.IsHomogeneous.neg
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
:
(-φ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.sub
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
{φ ψ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(hψ : ψ.IsHomogeneous n)
:
(φ - ψ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.totalDegree_le
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous 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}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(h : φ ≠ 0)
:
theorem
MvPolynomial.IsHomogeneous.rename_isHomogeneous
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
{f : σ → τ}
(h : φ.IsHomogeneous n)
:
((rename f) φ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
{f : σ → τ}
(hf : Function.Injective f)
:
theorem
MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous
{R : Type u_3}
[CommSemiring R]
{N : ℕ}
{φ : MvPolynomial (Fin (N + 1)) R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(i j : ℕ)
(h : i + j = n)
:
(((finSuccEquiv R N) φ).coeff i).IsHomogeneous j
theorem
MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{n : ℕ}
[hσ : Finite σ]
{p : Polynomial (MvPolynomial σ R)}
(hp : ((optionEquivLeft R σ).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}
[CommRing R]
[IsDomain R]
{F : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = 0)
(hnR : ↑n ≤ Cardinal.mk R)
:
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}
[CommRing R]
[IsDomain R]
{F G : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(hG : G.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = (eval r) G)
(hnR : ↑n ≤ Cardinal.mk R)
:
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}
[CommRing R]
[IsDomain R]
[Infinite R]
{F : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) 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}
[CommRing R]
[IsDomain R]
[Infinite R]
{F G : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(hG : G.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = (eval r) G)
:
See MvPolynomial.IsHomogeneous.funext_of_le_card
for a version that assumes n ≤ #R.
instance
MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
The homogeneous submodules form a graded ring. This instance is used by DirectSum.commSemiring
and DirectSum.algebra.
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.
Instances For
theorem
MvPolynomial.homogeneousComponent_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.coeff_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(d : σ →₀ ℕ)
:
theorem
MvPolynomial.homogeneousComponent_apply
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousComponent_isHomogeneous
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
((homogeneousComponent n) φ).IsHomogeneous n
@[simp]
theorem
MvPolynomial.homogeneousComponent_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
@[simp]
theorem
MvPolynomial.homogeneousComponent_C_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
(r : R)
:
theorem
MvPolynomial.homogeneousComponent_eq_zero'
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : ∀ d ∈ φ.support, d.degree ≠ n)
:
theorem
MvPolynomial.homogeneousComponent_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : φ.totalDegree < n)
:
theorem
MvPolynomial.sum_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousComponent_of_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{m n : ℕ}
{p : MvPolynomial σ R}
(h : p ∈ homogeneousSubmodule σ R n)
:
theorem
MvPolynomial.HomogeneousSubmodule.gradedMonoid
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
The homogeneous submodules form a graded ring.
This instance is used by DirectSum.commSemiring and DirectSum.algebra.
@[reducible, inline]
The decomposition of MvPolynomial σ R into homogeneous submodules.
Instances For
@[reducible, inline]
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.
Instances For
theorem
MvPolynomial.decomposition.decompose'_apply
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(i : ℕ)
:
theorem
MvPolynomial.decomposition.decompose'_eq
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
DirectSum.Decomposition.decompose' = fun (φ : MvPolynomial σ R) =>
(DirectSum.mk (fun (i : ℕ) => ↥(homogeneousSubmodule σ R i)) (Finset.image Finsupp.degree φ.support))
fun (m : ↑↑(Finset.image Finsupp.degree φ.support)) => ⟨(homogeneousComponent ↑m) φ, ⋯⟩