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
- MvPolynomial.IsHomogeneous φ n = ∀ ⦃d : σ →₀ ℕ⦄, MvPolynomial.coeff d φ ≠ 0 → (Finset.sum d.support fun (i : σ) => d i) = n
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
@[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 : ℕ)
:
MvPolynomial.homogeneousSubmodule σ R n = Finsupp.supported R R {d : σ →₀ ℕ | (Finset.sum d.support fun (i : σ) => d i) = 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 : (Finset.sum d.support fun (i : σ) => d i) = n)
:
theorem
MvPolynomial.isHomogeneous_of_totalDegree_zero
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
{p : MvPolynomial σ R}
(hp : MvPolynomial.totalDegree p = 0)
:
theorem
MvPolynomial.isHomogeneous_C
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
(r : R)
:
MvPolynomial.IsHomogeneous (MvPolynomial.C r) 0
theorem
MvPolynomial.IsHomogeneous.coeff_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : MvPolynomial.IsHomogeneous φ n)
(d : σ →₀ ℕ)
(hd : (Finset.sum d.support fun (i : σ) => d i) ≠ n)
:
MvPolynomial.coeff d φ = 0
theorem
MvPolynomial.IsHomogeneous.inj_right
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
{n : ℕ}
(hm : MvPolynomial.IsHomogeneous φ m)
(hn : MvPolynomial.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φ : MvPolynomial.IsHomogeneous φ n)
(hψ : MvPolynomial.IsHomogeneous ψ n)
:
MvPolynomial.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, MvPolynomial.IsHomogeneous (φ i) n)
:
MvPolynomial.IsHomogeneous (Finset.sum s fun (i : ι) => φ i) n
theorem
MvPolynomial.IsHomogeneous.mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{ψ : MvPolynomial σ R}
{m : ℕ}
{n : ℕ}
(hφ : MvPolynomial.IsHomogeneous φ m)
(hψ : MvPolynomial.IsHomogeneous ψ n)
:
MvPolynomial.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, MvPolynomial.IsHomogeneous (φ i) (n i))
:
MvPolynomial.IsHomogeneous (Finset.prod s fun (i : ι) => φ i) (Finset.sum s fun (i : ι) => n i)
theorem
MvPolynomial.IsHomogeneous.C_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
(hφ : MvPolynomial.IsHomogeneous φ m)
(r : R)
:
MvPolynomial.IsHomogeneous (MvPolynomial.C r * φ) m
theorem
MvPolynomial.isHomogeneous_C_mul_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
:
MvPolynomial.IsHomogeneous (MvPolynomial.C r * MvPolynomial.X i) 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.IsHomogeneous (MvPolynomial.C r * MvPolynomial.X i) 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φ : MvPolynomial.IsHomogeneous φ m)
(n : ℕ)
:
MvPolynomial.IsHomogeneous (φ ^ n) (m * n)
theorem
MvPolynomial.isHomogeneous_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(i : σ)
(n : ℕ)
:
theorem
MvPolynomial.isHomogeneous_C_mul_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
(n : ℕ)
:
MvPolynomial.IsHomogeneous (MvPolynomial.C r * MvPolynomial.X i ^ n) 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φ : MvPolynomial.IsHomogeneous φ m)
(f : R →+* MvPolynomial τ S)
(g : σ → MvPolynomial τ S)
(hf : ∀ (r : R), MvPolynomial.IsHomogeneous (f r) 0)
(hg : ∀ (i : σ), MvPolynomial.IsHomogeneous (g i) n)
:
MvPolynomial.IsHomogeneous (MvPolynomial.eval₂ f g φ) (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φ : MvPolynomial.IsHomogeneous φ n)
(f : R →+* S)
:
MvPolynomial.IsHomogeneous ((MvPolynomial.map f) φ) 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φ : MvPolynomial.IsHomogeneous φ m)
(g : σ → MvPolynomial τ S)
(hg : ∀ (i : σ), MvPolynomial.IsHomogeneous (g i) n)
:
MvPolynomial.IsHomogeneous ((MvPolynomial.aeval g) φ) (n * m)
theorem
MvPolynomial.IsHomogeneous.neg
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : MvPolynomial.IsHomogeneous φ n)
:
theorem
MvPolynomial.IsHomogeneous.sub
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
{φ : MvPolynomial σ R}
{ψ : MvPolynomial σ R}
{n : ℕ}
(hφ : MvPolynomial.IsHomogeneous φ n)
(hψ : MvPolynomial.IsHomogeneous ψ n)
:
MvPolynomial.IsHomogeneous (φ - ψ) n
theorem
MvPolynomial.IsHomogeneous.totalDegree_le
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : MvPolynomial.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φ : MvPolynomial.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 : MvPolynomial.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φ : MvPolynomial.IsHomogeneous φ n)
(i : ℕ)
(j : ℕ)
(h : i + j = n)
:
MvPolynomial.IsHomogeneous (Polynomial.coeff ((MvPolynomial.finSuccEquiv R N) φ) i) 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.IsHomogeneous ((AlgEquiv.symm (MvPolynomial.optionEquivLeft R σ)) p) n)
(i : ℕ)
(j : ℕ)
(h : i + j = n)
:
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 : MvPolynomial.IsHomogeneous F 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 : MvPolynomial.IsHomogeneous F n)
(hG : MvPolynomial.IsHomogeneous G 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 : MvPolynomial.IsHomogeneous F 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 : MvPolynomial.IsHomogeneous F n)
(hG : MvPolynomial.IsHomogeneous G 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MvPolynomial.coeff_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(d : σ →₀ ℕ)
:
MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent n) φ) = if (Finset.sum d.support fun (i : σ) => d i) = 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) φ = Finset.sum
(Finset.filter (fun (d : σ →₀ ℕ) => (Finset.sum d.support fun (i : σ) => d i) = n) (MvPolynomial.support φ))
fun (d : σ →₀ ℕ) => (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
theorem
MvPolynomial.homogeneousComponent_isHomogeneous
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
@[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 ∈ MvPolynomial.support φ, (Finset.sum d.support fun (i : σ) => d i) ≠ n)
:
(MvPolynomial.homogeneousComponent n) φ = 0
theorem
MvPolynomial.homogeneousComponent_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : MvPolynomial.totalDegree φ < n)
:
(MvPolynomial.homogeneousComponent n) φ = 0
theorem
MvPolynomial.sum_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
(Finset.sum (Finset.range (MvPolynomial.totalDegree φ + 1)) fun (i : ℕ) => (MvPolynomial.homogeneousComponent i) φ) = φ
theorem
MvPolynomial.homogeneousComponent_homogeneous_polynomial
{σ : 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