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)
:
MvPolynomial.weightedTotalDegree 1 φ = φ.totalDegree
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)
:
p ∈ MvPolynomial.homogeneousSubmodule σ R n ↔ p.IsHomogeneous n
theorem
MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
MvPolynomial.homogeneousSubmodule σ R 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}
[CommSemiring R]
(m : ℕ)
(n : ℕ)
:
MvPolynomial.homogeneousSubmodule σ R m * MvPolynomial.homogeneousSubmodule σ R n ≤ MvPolynomial.homogeneousSubmodule σ R (m + n)
theorem
MvPolynomial.isHomogeneous_monomial
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{d : σ →₀ ℕ}
(r : R)
{n : ℕ}
(hn : d.degree = n)
:
((MvPolynomial.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)
:
(MvPolynomial.C r).IsHomogeneous 0
theorem
MvPolynomial.isHomogeneous_X
{σ : Type u_1}
(R : Type u_3)
[CommSemiring R]
(i : σ)
:
(MvPolynomial.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)
:
MvPolynomial.coeff d φ = 0
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)
:
m = n
theorem
MvPolynomial.IsHomogeneous.add
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ 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}
{ψ : MvPolynomial σ R}
{m : ℕ}
{n : ℕ}
(hφ : φ.IsHomogeneous m)
(hψ : ψ.IsHomogeneous 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)
:
(MvPolynomial.C r * φ).IsHomogeneous m
theorem
MvPolynomial.isHomogeneous_C_mul_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
:
(MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1
@[deprecated MvPolynomial.isHomogeneous_C_mul_X]
theorem
MvPolynomial.C_mul_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
:
(MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1
Alias of MvPolynomial.isHomogeneous_C_mul_X.
theorem
MvPolynomial.IsHomogeneous.pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
(hφ : φ.IsHomogeneous m)
(n : ℕ)
:
theorem
MvPolynomial.isHomogeneous_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(i : σ)
(n : ℕ)
:
(MvPolynomial.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 : ℕ)
:
(MvPolynomial.C r * MvPolynomial.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}
{ψ : 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)
:
φ.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}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(h : φ ≠ 0)
:
φ.totalDegree = n
theorem
MvPolynomial.IsHomogeneous.rename_isHomogeneous
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
{f : σ → τ}
(h : φ.IsHomogeneous n)
:
((MvPolynomial.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)
:
((MvPolynomial.rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n
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)
:
(((MvPolynomial.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 : ((MvPolynomial.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), (MvPolynomial.eval r) F = 0)
(hnR : ↑n ≤ Cardinal.mk R)
:
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}
[CommRing R]
[IsDomain R]
{F : MvPolynomial σ R}
{G : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(hG : G.IsHomogeneous n)
(h : ∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G)
(hnR : ↑n ≤ Cardinal.mk R)
:
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}
[CommRing R]
[IsDomain R]
[Infinite R]
{F : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(h : ∀ (r : σ → R), (MvPolynomial.eval 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}
[CommRing R]
[IsDomain R]
[Infinite R]
{F : MvPolynomial σ R}
{G : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(hG : G.IsHomogeneous n)
(h : ∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G)
:
F = 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.
Equations
- ⋯ = ⋯
def
MvPolynomial.homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
:
MvPolynomial σ R →ₗ[R] MvPolynomial σ R
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 : σ →₀ ℕ)
:
MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent n) φ) = if d.degree = n then MvPolynomial.coeff d φ else 0
theorem
MvPolynomial.homogeneousComponent_apply
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
(MvPolynomial.homogeneousComponent n) φ = ∑ d ∈ Finset.filter (fun (d : σ →₀ ℕ) => d.degree = n) φ.support, (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
theorem
MvPolynomial.homogeneousComponent_isHomogeneous
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
((MvPolynomial.homogeneousComponent n) φ).IsHomogeneous n
@[simp]
theorem
MvPolynomial.homogeneousComponent_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
(MvPolynomial.homogeneousComponent 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)
@[simp]
theorem
MvPolynomial.homogeneousComponent_C_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
(r : R)
:
(MvPolynomial.homogeneousComponent n) (MvPolynomial.C r * φ) = MvPolynomial.C r * (MvPolynomial.homogeneousComponent n) φ
theorem
MvPolynomial.homogeneousComponent_eq_zero'
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : ∀ d ∈ φ.support, d.degree ≠ n)
:
(MvPolynomial.homogeneousComponent n) φ = 0
theorem
MvPolynomial.homogeneousComponent_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : φ.totalDegree < n)
:
(MvPolynomial.homogeneousComponent n) φ = 0
theorem
MvPolynomial.sum_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
∑ i ∈ Finset.range (φ.totalDegree + 1), (MvPolynomial.homogeneousComponent i) φ = φ
theorem
MvPolynomial.homogeneousComponent_of_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{m : ℕ}
{n : ℕ}
{p : MvPolynomial σ R}
(h : p ∈ MvPolynomial.homogeneousSubmodule σ R n)
:
(MvPolynomial.homogeneousComponent m) p = if m = n then p else 0
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.
Equations
- MvPolynomial.decomposition = MvPolynomial.weightedDecomposition R 1
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.
Equations
- MvPolynomial.gradedAlgebra = MvPolynomial.weightedGradedAlgebra R 1
Instances For
theorem
MvPolynomial.decomposition.decompose'_apply
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(i : ℕ)
:
↑((DirectSum.Decomposition.decompose' φ) i) = (MvPolynomial.homogeneousComponent 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 : ℕ) => ↥(MvPolynomial.homogeneousSubmodule σ R i)) (Finset.image Finsupp.degree φ.support))
fun (m : ↑↑(Finset.image Finsupp.degree φ.support)) => ⟨(MvPolynomial.homogeneousComponent ↑m) φ, ⋯⟩