Homogeneous polynomials #
A multivariate polynomial φ
is homogeneous of degree n
if all monomials occuring in φ
have degree n
.
Main definitions/lemmas #
is_homogeneous φ n
: a predicate that asserts thatφ
is homogeneous of degreen
.homogeneous_submodule σ R n
: the submodule of homogeneous polynomials of degreen
.homogeneous_component n
: the additive morphism that projects polynomials onto their summand that is homogeneous of degreen
.sum_homogeneous_component
: every polynomial is the sum of its homogeneous components
def
mv_polynomial.is_homogeneous
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R)
(n : ℕ) :
Prop
A multivariate polynomial φ
is homogeneous of degree n
if all monomials occuring in φ
have degree n
.
def
mv_polynomial.homogeneous_submodule
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R]
(n : ℕ) :
submodule R (mv_polynomial σ R)
The submodule of homogeneous mv_polynomial
s of degree n
.
Equations
- mv_polynomial.homogeneous_submodule σ R n = {carrier := {x : mv_polynomial σ R | x.is_homogeneous n}, add_mem' := _, zero_mem' := _, smul_mem' := _}
Instances for mv_polynomial.homogeneous_submodule
@[simp]
theorem
mv_polynomial.mem_homogeneous_submodule
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(p : mv_polynomial σ R) :
p ∈ mv_polynomial.homogeneous_submodule σ R n ↔ p.is_homogeneous n
theorem
mv_polynomial.homogeneous_submodule_eq_finsupp_supported
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R]
(n : ℕ) :
mv_polynomial.homogeneous_submodule σ R n = finsupp.supported R R {d : σ →₀ ℕ | d.support.sum (λ (i : σ), ⇑d i) = n}
While equal, the former has a convenient definitional reduction.
theorem
mv_polynomial.homogeneous_submodule_mul
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(m n : ℕ) :
mv_polynomial.homogeneous_submodule σ R m * mv_polynomial.homogeneous_submodule σ R n ≤ mv_polynomial.homogeneous_submodule σ R (m + n)
theorem
mv_polynomial.is_homogeneous_monomial
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(d : σ →₀ ℕ)
(r : R)
(n : ℕ)
(hn : d.support.sum (λ (i : σ), ⇑d i) = n) :
(⇑(mv_polynomial.monomial d) r).is_homogeneous n
theorem
mv_polynomial.is_homogeneous_of_total_degree_zero
(σ : Type u_1)
{R : Type u_3}
[comm_semiring R]
{p : mv_polynomial σ R}
(hp : p.total_degree = 0) :
p.is_homogeneous 0
theorem
mv_polynomial.is_homogeneous_zero
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R]
(n : ℕ) :
0.is_homogeneous n
theorem
mv_polynomial.is_homogeneous_one
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R] :
1.is_homogeneous 0
theorem
mv_polynomial.is_homogeneous.coeff_eq_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{n : ℕ}
(hφ : φ.is_homogeneous n)
(d : σ →₀ ℕ)
(hd : d.support.sum (λ (i : σ), ⇑d i) ≠ n) :
mv_polynomial.coeff d φ = 0
theorem
mv_polynomial.is_homogeneous.inj_right
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{m n : ℕ}
(hm : φ.is_homogeneous m)
(hn : φ.is_homogeneous n)
(hφ : φ ≠ 0) :
m = n
theorem
mv_polynomial.is_homogeneous.add
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ ψ : mv_polynomial σ R}
{n : ℕ}
(hφ : φ.is_homogeneous n)
(hψ : ψ.is_homogeneous n) :
(φ + ψ).is_homogeneous n
theorem
mv_polynomial.is_homogeneous.sum
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{ι : Type u_2}
(s : finset ι)
(φ : ι → mv_polynomial σ R)
(n : ℕ)
(h : ∀ (i : ι), i ∈ s → (φ i).is_homogeneous n) :
(s.sum (λ (i : ι), φ i)).is_homogeneous n
theorem
mv_polynomial.is_homogeneous.mul
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ ψ : mv_polynomial σ R}
{m n : ℕ}
(hφ : φ.is_homogeneous m)
(hψ : ψ.is_homogeneous n) :
(φ * ψ).is_homogeneous (m + n)
theorem
mv_polynomial.is_homogeneous.prod
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{ι : Type u_2}
(s : finset ι)
(φ : ι → mv_polynomial σ R)
(n : ι → ℕ)
(h : ∀ (i : ι), i ∈ s → (φ i).is_homogeneous (n i)) :
(s.prod (λ (i : ι), φ i)).is_homogeneous (s.sum (λ (i : ι), n i))
theorem
mv_polynomial.is_homogeneous.total_degree
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{n : ℕ}
(hφ : φ.is_homogeneous n)
(h : φ ≠ 0) :
φ.total_degree = n
@[protected, instance]
def
mv_polynomial.is_homogeneous.homogeneous_submodule.gcomm_semiring
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R] :
The homogeneous submodules form a graded ring. This instance is used by direct_sum.comm_semiring
and direct_sum.algebra
.
noncomputable
def
mv_polynomial.homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ) :
mv_polynomial σ R →ₗ[R] mv_polynomial σ R
homogeneous_component n φ
is the part of φ
that is homogeneous of degree n
.
See sum_homogeneous_component
for the statement that φ
is equal to the sum
of all its homogeneous components.
theorem
mv_polynomial.coeff_homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R)
(d : σ →₀ ℕ) :
mv_polynomial.coeff d (⇑(mv_polynomial.homogeneous_component n) φ) = ite (d.support.sum (λ (i : σ), ⇑d i) = n) (mv_polynomial.coeff d φ) 0
theorem
mv_polynomial.homogeneous_component_apply
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.homogeneous_component n) φ = (finset.filter (λ (d : σ →₀ ℕ), d.support.sum (λ (i : σ), ⇑d i) = n) φ.support).sum (λ (d : σ →₀ ℕ), ⇑(mv_polynomial.monomial d) (mv_polynomial.coeff d φ))
theorem
mv_polynomial.homogeneous_component_is_homogeneous
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R) :
@[simp]
theorem
mv_polynomial.homogeneous_component_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R) :
@[simp]
theorem
mv_polynomial.homogeneous_component_C_mul
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R)
(n : ℕ)
(r : R) :
theorem
mv_polynomial.homogeneous_component_eq_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R)
(h : φ.total_degree < n) :
theorem
mv_polynomial.sum_homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R) :
(finset.range (φ.total_degree + 1)).sum (λ (i : ℕ), ⇑(mv_polynomial.homogeneous_component i) φ) = φ
theorem
mv_polynomial.homogeneous_component_homogeneous_polynomial
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(m n : ℕ)
(p : mv_polynomial σ R)
(h : p ∈ mv_polynomial.homogeneous_submodule σ R n) :
⇑(mv_polynomial.homogeneous_component m) p = ite (m = n) p 0