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 degree n.
• homogeneousSubmodule σ R n: the submodule of homogeneous polynomials of degree n.
• homogeneousComponent n: the additive morphism that projects polynomials onto their summand that is homogeneous of degree n.
• 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 : ℕ) : Prop

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

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.

@[simp]

theorem MvPolynomial.mem_homogeneousSubmodule {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ℕ) (p : MvPolynomial σ R) : p ∈ MvPolynomial.homogeneousSubmodule σ R n ↔ MvPolynomial.IsHomogeneous p 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 | (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) : MvPolynomial.IsHomogeneous (↑(MvPolynomial.monomial d) r) n

theorem MvPolynomial.isHomogeneous_of_totalDegree_zero (σ : Type u_1) {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} (hp : MvPolynomial.totalDegree p = 0) : MvPolynomial.IsHomogeneous 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_zero (σ : Type u_1) (R : Type u_3) [CommSemiring R] (n : ℕ) : MvPolynomial.IsHomogeneous 0 n

theorem MvPolynomial.isHomogeneous_one (σ : Type u_1) (R : Type u_3) [CommSemiring R] : MvPolynomial.IsHomogeneous 1 0

theorem MvPolynomial.isHomogeneous_X {σ : Type u_1} (R : Type u_3) [CommSemiring R] (i : σ) : MvPolynomial.IsHomogeneous (MvPolynomial.X i) 1

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 : ι), 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 : ι), 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.totalDegree {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} (hφ : MvPolynomial.IsHomogeneous φ n) (h : φ ≠ 0) : MvPolynomial.totalDegree φ = n

instance MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring {σ : Type u_1} {R : Type u_3} [CommSemiring R] : SetLike.GradedMonoid (MvPolynomial.homogeneousSubmodule σ R)

The homogeneous submodules form a graded ring. This instance is used by DirectSum.commSemiring and DirectSum.algebra.

Equations

• @MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring = @MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring.proof_1

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.

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) : MvPolynomial.IsHomogeneous (↑(MvPolynomial.homogeneousComponent n) φ) 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 : σ →₀ ℕ), 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