Homogeneous polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 degree n.
homogeneous_submodule σ R n: the submodule of homogeneous polynomials of degree n.
homogeneous_component n: the additive morphism that projects polynomials onto their summand that is homogeneous of degree n.
sum_homogeneous_component: every polynomial is the sum of its homogeneous components

source

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.

Equations

φ.is_homogeneous n = ∀ ⦃d : σ →₀ ℕ⦄, mv_polynomial.coeff d φ ≠ 0 → d.support.sum (λ (i : σ), ⇑d i) = n

source

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_polynomials 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

mv_polynomial.is_homogeneous.homogeneous_submodule.gcomm_semiring

source

@[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

source

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.

source

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)

source

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

source

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

source

theorem mv_polynomial.is_homogeneous_C (σ : Type u_1) {R : Type u_3} [comm_semiring R] (r : R) :

(⇑mv_polynomial.C r).is_homogeneous 0

source

theorem mv_polynomial.is_homogeneous_zero (σ : Type u_1) (R : Type u_3) [comm_semiring R] (n : ℕ) :

0.is_homogeneous n

source

theorem mv_polynomial.is_homogeneous_one (σ : Type u_1) (R : Type u_3) [comm_semiring R] :

1.is_homogeneous 0

source

theorem mv_polynomial.is_homogeneous_X {σ : Type u_1} (R : Type u_3) [comm_semiring R] (i : σ) :

(mv_polynomial.X i).is_homogeneous 1

source

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

source

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

source

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

source

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

source

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)

source

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))

source

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

source

@[protected, instance]

def mv_polynomial.is_homogeneous.homogeneous_submodule.gcomm_semiring {σ : Type u_1} {R : Type u_3} [comm_semiring R] :

set_like.graded_monoid (mv_polynomial.homogeneous_submodule σ R)

The homogeneous submodules form a graded ring. This instance is used by direct_sum.comm_semiring and direct_sum.algebra.

source

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.

Equations

mv_polynomial.homogeneous_component n = (finsupp.supported R R {d : σ →₀ ℕ | d.support.sum (λ (i : σ), ⇑d i) = n}).subtype.comp (finsupp.restrict_dom R R {d : σ →₀ ℕ | d.support.sum (λ (i : σ), ⇑d i) = n})

source

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

source

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 φ))

source

theorem mv_polynomial.homogeneous_component_is_homogeneous {σ : Type u_1} {R : Type u_3} [comm_semiring R] (n : ℕ) (φ : mv_polynomial σ R) :

(⇑(mv_polynomial.homogeneous_component n) φ).is_homogeneous n

source

@[simp]

theorem mv_polynomial.homogeneous_component_zero {σ : Type u_1} {R : Type u_3} [comm_semiring R] (φ : mv_polynomial σ R) :

⇑(mv_polynomial.homogeneous_component 0) φ = ⇑mv_polynomial.C (mv_polynomial.coeff 0 φ)

source

@[simp]

theorem mv_polynomial.homogeneous_component_C_mul {σ : Type u_1} {R : Type u_3} [comm_semiring R] (φ : mv_polynomial σ R) (n : ℕ) (r : R) :

⇑(mv_polynomial.homogeneous_component n) (⇑mv_polynomial.C r * φ) = ⇑mv_polynomial.C r * ⇑(mv_polynomial.homogeneous_component n) φ

source

theorem mv_polynomial.homogeneous_component_eq_zero' {σ : Type u_1} {R : Type u_3} [comm_semiring R] (n : ℕ) (φ : mv_polynomial σ R) (h : ∀ (d : σ →₀ ℕ), d ∈ φ.support → d.support.sum (λ (i : σ), ⇑d i) ≠ n) :

⇑(mv_polynomial.homogeneous_component n) φ = 0

source

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) :

⇑(mv_polynomial.homogeneous_component n) φ = 0

source

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) φ) = φ

source

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