Homogenization #
Main definitions #
mv_polynomial.homogenization
Main statements #
- foo_bar_unique
Notation #
Implementation details #
- We homogenize polynomials over a given ground set of variables, rather than adjoining an extra variable to give the user more choice in the type of the polynomials involved.
References #
- [F. Bar, Quuxes][]
Tags #
theorem
MvPolynomial.Finsupp.sum_update_add
{ι : Type u_3}
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[AddCommMonoid β]
(f : ι →₀ α)
(i : ι)
(a : α)
(g : ι → α → β)
(hg : ∀ (i : ι), g i 0 = 0)
(hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂)
:
Finsupp.sum (Finsupp.update f i a) g + g i (↑f i) = Finsupp.sum f g + g i a
def
MvPolynomial.homogenization
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(p : MvPolynomial ι R)
:
MvPolynomial ι R
The homogenization of a multivariate polynomial at a single variable.
Equations
- MvPolynomial.homogenization i p = Finsupp.mapDomain (fun j => j + fun₀ | i => MvPolynomial.totalDegree p - Finsupp.sum j fun x m => m) p
Instances For
@[simp]
theorem
MvPolynomial.Finsupp.support_mapDomain
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[AddCommMonoid M]
(f : α ↪ β)
(v : α →₀ M)
:
(Finsupp.mapDomain (↑f) v).support ⊆ Finset.map f v.support
theorem
MvPolynomial.Finsupp.mapDomain_apply'
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[AddCommMonoid M]
(S : Set α)
{f : α → β}
(x : α →₀ M)
(hS : ↑x.support ⊆ S)
(hf : Set.InjOn f S)
{a : α}
(ha : a ∈ S)
:
↑(Finsupp.mapDomain f x) (f a) = ↑x a
theorem
MvPolynomial.Finsupp.mapDomain_injOn
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[AddCommMonoid M]
(S : Set α)
{f : α → β}
(hf : Set.InjOn f S)
:
Set.InjOn (Finsupp.mapDomain f) {w | ↑w.support ⊆ S}
@[simp]
theorem
MvPolynomial.homogenization_zero
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
:
MvPolynomial.homogenization i 0 = 0
@[simp]
theorem
MvPolynomial.homogenization_one
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
:
MvPolynomial.homogenization i 1 = 1
@[simp]
theorem
MvPolynomial.homogenization_C
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(c : R)
:
MvPolynomial.homogenization i (↑MvPolynomial.C c) = ↑MvPolynomial.C c
@[simp]
theorem
MvPolynomial.homogenization_monomial
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
(i : ι)
(s : ι →₀ ℕ)
(r : R)
:
MvPolynomial.homogenization i (↑(MvPolynomial.monomial s) r) = ↑(MvPolynomial.monomial s) r
theorem
MvPolynomial.aux
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{i : ι}
{p : MvPolynomial ι R}
{x : ι →₀ ℕ}
(hp : x ∈ MvPolynomial.support p)
:
(Finsupp.sum (x + fun₀ | i => MvPolynomial.totalDegree p - Finsupp.sum x fun x m => m) fun x m => m) = MvPolynomial.totalDegree p
theorem
MvPolynomial.isHomogeneous_homogenization
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.homogenization_of_isHomogeneous
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(n : ℕ)
(i : ι)
(p : MvPolynomial ι R)
(hp : MvPolynomial.IsHomogeneous p n)
:
MvPolynomial.homogenization i p = p
theorem
MvPolynomial.homogenization_idempotent
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.homogenization_ne_zero_of_ne_zero
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
{p : MvPolynomial ι R}
(hp : p ≠ 0)
(hjp : ∀ (j : ι →₀ ℕ), j ∈ MvPolynomial.support p → ↑j i = 0)
:
MvPolynomial.homogenization i p ≠ 0
theorem
MvPolynomial.totalDegree_homogenization
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(p : MvPolynomial ι R)
(h : ∀ (j : ι →₀ ℕ), j ∈ MvPolynomial.support p → ↑j i = 0)
:
def
MvPolynomial.leadingTerms
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
MvPolynomial ι R
The sum of the monomials of highest degree of a multivariate polynomial.
Equations
Instances For
theorem
MvPolynomial.leadingTerms_apply
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
MvPolynomial.leadingTerms p = Finset.sum
(Finset.filter (fun d => (Finset.sum d.support fun i => ↑d i) = MvPolynomial.totalDegree p)
(MvPolynomial.support p))
fun d => ↑(MvPolynomial.monomial d) (MvPolynomial.coeff d p)
theorem
MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
@[simp]
theorem
MvPolynomial.leadingTerms_C
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(r : R)
:
MvPolynomial.leadingTerms (↑MvPolynomial.C r) = ↑MvPolynomial.C r
@[simp]
@[simp]
@[simp]
theorem
MvPolynomial.leadingTerms_monomial
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
(s : ι →₀ ℕ)
(r : R)
:
MvPolynomial.leadingTerms (↑(MvPolynomial.monomial s) r) = ↑(MvPolynomial.monomial s) r
@[simp]
theorem
MvPolynomial.isHomogeneous_leadingTerms
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.exists_coeff_ne_zero_totalDegree
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{p : MvPolynomial ι R}
(hp : p ≠ 0)
:
∃ v, (Finsupp.sum v fun x e => e) = MvPolynomial.totalDegree p ∧ MvPolynomial.coeff v p ≠ 0
theorem
MvPolynomial.support_add_eq
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
[DecidableEq ι]
{g₁ : MvPolynomial ι R}
{g₂ : MvPolynomial ι R}
(h : Disjoint (MvPolynomial.support g₁) (MvPolynomial.support g₂))
:
MvPolynomial.support (g₁ + g₂) = MvPolynomial.support g₁ ∪ MvPolynomial.support g₂
theorem
MvPolynomial.add_ne_zero_of_ne_zero_of_support_disjoint
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
(q : MvPolynomial ι R)
(hp : p ≠ 0)
(h : Disjoint (MvPolynomial.support p) (MvPolynomial.support q))
:
theorem
MvPolynomial.support_sum_monomial_eq
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
[DecidableEq R]
(S : Finset (ι →₀ ℕ))
(f : (ι →₀ ℕ) → R)
:
MvPolynomial.support (Finset.sum S fun v => ↑(MvPolynomial.monomial v) (f v)) = Finset.filter (fun v => f v ≠ 0) S
theorem
MvPolynomial.support_sum_monomial_subset
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
(S : Finset (ι →₀ ℕ))
(f : (ι →₀ ℕ) → R)
:
MvPolynomial.support (Finset.sum S fun v => ↑(MvPolynomial.monomial v) (f v)) ⊆ S
theorem
MvPolynomial.sum_monomial_ne_zero_of_exists_mem_ne_zero
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
(S : Finset (ι →₀ ℕ))
(f : (ι →₀ ℕ) → R)
(h : ∃ s x, f s ≠ 0)
:
(Finset.sum S fun s => ↑(MvPolynomial.monomial s) (f s)) ≠ 0
theorem
MvPolynomial.leadingTerms_ne_zero
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{p : MvPolynomial ι R}
(hp : p ≠ 0)
:
@[simp]
theorem
MvPolynomial.totalDegree_homogenous_component_of_ne_zero
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{n : ℕ}
{p : MvPolynomial ι R}
(hp : ↑(MvPolynomial.homogeneousComponent n) p ≠ 0)
:
@[simp]
theorem
MvPolynomial.totalDegree_leadingTerms
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.leadingTerms_idempotent
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.coeff_leadingTerms
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
(d : ι →₀ ℕ)
:
MvPolynomial.coeff d (MvPolynomial.leadingTerms p) = if (Finset.sum d.support fun i => ↑d i) = MvPolynomial.totalDegree p then MvPolynomial.coeff d p else 0
theorem
MvPolynomial.support_homogeneousComponent
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(n : ℕ)
(p : MvPolynomial ι R)
:
MvPolynomial.support (↑(MvPolynomial.homogeneousComponent n) p) = Finset.filter (fun d => (Finsupp.sum d fun x m => m) = n) (MvPolynomial.support p)
theorem
MvPolynomial.support_homogeneousComponent_subset
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(n : ℕ)
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.support_leadingTerms
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
MvPolynomial.support (MvPolynomial.leadingTerms p) = Finset.filter (fun d => (Finsupp.sum d fun x m => m) = MvPolynomial.totalDegree p) (MvPolynomial.support p)
theorem
MvPolynomial.support_leadingTerms_subset
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
:
theorem
MvPolynomial.eq_leadingTerms_add
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
(hp : MvPolynomial.totalDegree p ≠ 0)
:
∃ p_rest, p = MvPolynomial.leadingTerms p + p_rest ∧ MvPolynomial.totalDegree p_rest < MvPolynomial.totalDegree p
theorem
MvPolynomial.leadingTerms_add_of_totalDegree_lt
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(p : MvPolynomial ι R)
(q : MvPolynomial ι R)
(h : MvPolynomial.totalDegree q < MvPolynomial.totalDegree p)
:
theorem
MvPolynomial.NoZeroSmulDivisors.smul_eq_zero_iff_eq_zero_or_eq_zero
(R : Type u_1)
(M : Type u_2)
[Zero R]
[Zero M]
[SMulWithZero R M]
[NoZeroSMulDivisors R M]
{c : R}
{x : M}
:
@[simp]
theorem
MvPolynomial.leadingTerms_C_mul
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
[NoZeroSMulDivisors R R]
(p : MvPolynomial ι R)
(r : R)
:
MvPolynomial.leadingTerms (↑MvPolynomial.C r * p) = ↑MvPolynomial.C r * MvPolynomial.leadingTerms p
theorem
MvPolynomial.eq_C_of_totalDegree_zero
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{p : MvPolynomial ι R}
(hp : MvPolynomial.totalDegree p = 0)
:
p = ↑MvPolynomial.C (MvPolynomial.coeff 0 p)
@[simp]
theorem
MvPolynomial.leadingTerms_mul
{ι : Type u_2}
{S : Type u_1}
[CommRing S]
[IsDomain S]
(p : MvPolynomial ι S)
(q : MvPolynomial ι S)
:
theorem
MvPolynomial.totalDegree_mul_eq
{ι : Type u_2}
{S : Type u_1}
[CommRing S]
[IsDomain S]
{p : MvPolynomial ι S}
{q : MvPolynomial ι S}
(hp : p ≠ 0)
(hq : q ≠ 0)
:
theorem
MvPolynomial.homogenization_add_of_totalDegree_eq
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(p : MvPolynomial ι R)
(q : MvPolynomial ι R)
(h : MvPolynomial.totalDegree p = MvPolynomial.totalDegree q)
(hpq : MvPolynomial.totalDegree p = MvPolynomial.totalDegree (p + q))
:
MvPolynomial.homogenization i (p + q) = MvPolynomial.homogenization i p + MvPolynomial.homogenization i q
theorem
MvPolynomial.homogenization_mul
{ι : Type u_2}
{S : Type u_1}
[CommRing S]
[IsDomain S]
(i : ι)
(p : MvPolynomial ι S)
(q : MvPolynomial ι S)
:
MvPolynomial.homogenization i (p * q) = MvPolynomial.homogenization i p * MvPolynomial.homogenization i q
@[simp]
theorem
MvPolynomial.homogenization_X_add_C
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{i : ι}
{j : ι}
(r : R)
:
MvPolynomial.homogenization i (MvPolynomial.X j + ↑MvPolynomial.C r) = MvPolynomial.X j + ↑MvPolynomial.C r * MvPolynomial.X i
@[simp]
theorem
MvPolynomial.homogenization_X_sub_C
{ι : Type u_2}
{R : Type u_1}
[CommRing R]
{i : ι}
{j : ι}
(r : R)
:
MvPolynomial.homogenization i (MvPolynomial.X j - ↑MvPolynomial.C r) = MvPolynomial.X j - ↑MvPolynomial.C r * MvPolynomial.X i
@[simp]
theorem
MvPolynomial.homogenization_X_pow_add_C
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{i : ι}
{j : ι}
{n : ℕ}
(hn : 0 < n)
(r : R)
:
MvPolynomial.homogenization i (MvPolynomial.X j ^ n + ↑MvPolynomial.C r) = MvPolynomial.X j ^ n + ↑MvPolynomial.C r * MvPolynomial.X i ^ n
@[simp]
theorem
MvPolynomial.homogenization_X_pow_sub_C
{ι : Type u_2}
{R : Type u_1}
[CommRing R]
{i : ι}
{j : ι}
{n : ℕ}
(hn : 0 < n)
(r : R)
:
MvPolynomial.homogenization i (MvPolynomial.X j ^ n - ↑MvPolynomial.C r) = MvPolynomial.X j ^ n - ↑MvPolynomial.C r * MvPolynomial.X i ^ n
@[simp]
theorem
MvPolynomial.homogenization_X_pow_sub_one
{ι : Type u_2}
{R : Type u_1}
[CommRing R]
{i : ι}
{j : ι}
{n : ℕ}
(hn : 0 < n)
:
MvPolynomial.homogenization i (MvPolynomial.X j ^ n - 1) = MvPolynomial.X j ^ n - MvPolynomial.X i ^ n
@[simp]
theorem
MvPolynomial.homogenization_X_pow_add_one
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
{i : ι}
{j : ι}
{n : ℕ}
(hn : 0 < n)
:
MvPolynomial.homogenization i (MvPolynomial.X j ^ n + 1) = MvPolynomial.X j ^ n + MvPolynomial.X i ^ n
theorem
MvPolynomial.support_sum_monomial_subset'
{R : Type u_3}
{ι : Type u_1}
[CommSemiring R]
[DecidableEq ι]
{α : Type u_2}
(S : Finset α)
(g : α → ι →₀ ℕ)
(f : α → R)
:
MvPolynomial.support (Finset.sum S fun v => ↑(MvPolynomial.monomial (g v)) (f v)) ⊆ Finset.image g S
theorem
MvPolynomial.support_mul'
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
[DecidableEq ι]
(p : MvPolynomial ι R)
(q : MvPolynomial ι R)
:
@[simp]
theorem
MvPolynomial.support_one_of_nontrivial
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
[Nontrivial R]
:
theorem
MvPolynomial.support_prod
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
[DecidableEq ι]
(P : Finset (MvPolynomial ι R))
:
MvPolynomial.support (Finset.prod P id) ⊆ Finset.sum P MvPolynomial.support
theorem
MvPolynomial.degreeOf_eq_zero_iff
{R : Type u_1}
{ι : Type u_2}
[CommSemiring R]
(i : ι)
(p : MvPolynomial ι R)
:
MvPolynomial.degreeOf i p = 0 ↔ ∀ (j : ι →₀ ℕ), j ∈ MvPolynomial.support p → ↑j i = 0
theorem
MvPolynomial.prod_contains_no
{R : Type u_2}
{ι : Type u_1}
[CommSemiring R]
(i : ι)
(P : Finset (MvPolynomial ι R))
(hp : ∀ (p : MvPolynomial ι R), p ∈ P → ∀ (j : ι →₀ ℕ), j ∈ MvPolynomial.support p → ↑j i = 0)
(j : ι →₀ ℕ)
(hjp : j ∈ MvPolynomial.support (Finset.prod P id))
:
↑j i = 0
theorem
MvPolynomial.homogenization_prod
{ι : Type u_3}
{σ : Type u_1}
{S : Type u_2}
[CommRing S]
[IsDomain S]
(i : ι)
(P : σ → MvPolynomial ι S)
(L : Finset σ)
:
MvPolynomial.homogenization i (Finset.prod L fun l => P l) = Finset.prod L fun l => MvPolynomial.homogenization i (P l)
theorem
MvPolynomial.homogenization_prod_id
{ι : Type u_2}
{S : Type u_1}
[CommRing S]
[IsDomain S]
(i : ι)
(P : Finset (MvPolynomial ι S))
:
MvPolynomial.homogenization i (Finset.prod P id) = Finset.prod P fun p => MvPolynomial.homogenization i p