Mathlib.Algebra.MvPolynomial.Expand

Expand multivariate polynomials #

Given a multivariate polynomial φ, one may replace every occurrence of X i by X i ^ n, for some natural number n. This operation is called MvPolynomial.expand and it is an algebra homomorphism.

Main declaration #

MvPolynomial.expand: expand a polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

source

noncomputable def MvPolynomial.expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) :

MvPolynomial σ R →ₐ[R] MvPolynomial σ R

Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

See also Polynomial.expand.

Equations

MvPolynomial.expand p = MvPolynomial.bind₁ fun (i : σ) => MvPolynomial.X i ^ p

Instances For

source

theorem MvPolynomial.coe_expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) :

⇑(expand p) = eval₂ C ((fun (s : σ) => X s) ^ p)

source

theorem MvPolynomial.expand_C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (r : R) :

(expand p) (C r) = C r

source

@[simp]

theorem MvPolynomial.expand_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (i : σ) :

(expand p) (X i) = X i ^ p

source

@[simp]

theorem MvPolynomial.expand_monomial {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (d : σ →₀ ℕ) (r : R) :

(expand p) ((monomial d) r) = (monomial (p • d)) r

source

@[simp]

theorem MvPolynomial.expand_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] :

expand 0 = (Algebra.ofId R (MvPolynomial σ R)).comp (aeval 1)

source

theorem MvPolynomial.expand_zero_apply {σ : Type u_1} {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) :

(expand 0) f = C ((eval 1) f)

source

@[simp]

theorem MvPolynomial.expand_one {σ : Type u_1} {R : Type u_3} [CommSemiring R] :

expand 1 = AlgHom.id R (MvPolynomial σ R)

source

theorem MvPolynomial.expand_one_apply {σ : Type u_1} {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) :

(expand 1) f = f

source

theorem MvPolynomial.expand_mul_eq_comp {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p q : ℕ) :

expand (p * q) = (expand p).comp (expand q)

source

theorem MvPolynomial.expand_mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p q : ℕ) (φ : MvPolynomial σ R) :

(expand (p * q)) φ = (expand p) ((expand q) φ)

source

@[simp]

theorem MvPolynomial.coeff_expand_smul {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (hp : p ≠ 0) (φ : MvPolynomial σ R) (m : σ →₀ ℕ) :

coeff (p • m) ((expand p) φ) = coeff m φ

source

@[simp]

theorem MvPolynomial.coeff_expand_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (hp : p ≠ 0) (φ : MvPolynomial σ R) :

coeff 0 ((expand p) φ) = coeff 0 φ

source

theorem MvPolynomial.expand_injective {σ : Type u_1} {R : Type u_3} [CommSemiring R] {n : ℕ} (hn : 0 < n) :

Function.Injective ⇑(expand n)

Expansion is injective.

source

theorem MvPolynomial.expand_inj {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (hp : 0 < p) {f g : MvPolynomial σ R} :

(expand p) f = (expand p) g ↔ f = g

source

theorem MvPolynomial.expand_eq_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (hp : 0 < p) {f : MvPolynomial σ R} :

(expand p) f = 0 ↔ f = 0

source

theorem MvPolynomial.expand_ne_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (hp : 0 < p) {f : MvPolynomial σ R} :

(expand p) f ≠ 0 ↔ f ≠ 0

source

theorem MvPolynomial.expand_eq_C {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (hp : 0 < p) {f : MvPolynomial σ R} {r : R} :

(expand p) f = C r ↔ f = C r

source

theorem MvPolynomial.expand_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → MvPolynomial τ R) :

(expand p).comp (bind₁ f) = bind₁ fun (i : σ) => (expand p) (f i)

source

theorem MvPolynomial.expand_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :

(expand p) ((bind₁ f) φ) = (bind₁ fun (i : σ) => (expand p) (f i)) φ

source

@[simp]

theorem MvPolynomial.map_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (p : ℕ) (f : R →+* S) (φ : MvPolynomial σ R) :

(map f) ((expand p) φ) = (expand p) ((map f) φ)

source

@[simp]

theorem MvPolynomial.rename_comp_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → τ) :

(rename f).comp (expand p) = (expand p).comp (rename f)

source

@[simp]

theorem MvPolynomial.rename_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → τ) (φ : MvPolynomial σ R) :

(rename f) ((expand p) φ) = (expand p) ((rename f) φ)

source

theorem MvPolynomial.eval₂Hom_comp_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (p : ℕ) (f : R →+* S) (g : σ → S) :

(eval₂Hom f g).comp ↑(expand p) = eval₂Hom f (g ^ p)

source

@[simp]

theorem MvPolynomial.eval₂_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (p : ℕ) (f : R →+* S) (g : σ → S) (φ : MvPolynomial σ R) :

eval₂ f g ((expand p) φ) = eval₂ f (g ^ p) φ

source

@[simp]

theorem MvPolynomial.aeval_comp_expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) {A : Type u_5} [CommSemiring A] [Algebra R A] (f : σ → A) :

(aeval f).comp (expand p) = aeval (f ^ p)

source

@[simp]

theorem MvPolynomial.aeval_expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) {A : Type u_5} [CommSemiring A] [Algebra R A] (f : σ → A) (φ : MvPolynomial σ R) :

(aeval f) ((expand p) φ) = (aeval (f ^ p)) φ

source

@[simp]

theorem MvPolynomial.eval_expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → R) (φ : MvPolynomial σ R) :

(eval f) ((expand p) φ) = (eval (f ^ p)) φ

source

theorem MvPolynomial.support_expand_subset {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (φ : MvPolynomial σ R) [DecidableEq σ] :

((expand p) φ).support ⊆ Finset.image (fun (x : σ →₀ ℕ) => p • x) φ.support

source

theorem MvPolynomial.coeff_expand_of_not_dvd {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (φ : MvPolynomial σ R) {m : σ →₀ ℕ} {i : σ} (h : ¬p ∣ m i) :

coeff m ((expand p) φ) = 0

source

theorem MvPolynomial.support_expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (φ : MvPolynomial σ R) [DecidableEq σ] (hp : p ≠ 0) :

((expand p) φ).support = Finset.image (fun (x : σ →₀ ℕ) => p • x) φ.support

source

theorem MvPolynomial.totalDegree_expand {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : ℕ} (f : MvPolynomial σ R) :

((expand p) f).totalDegree = f.totalDegree * p

source

theorem MvPolynomial.isLocalHom_expand (R : Type u_1) (σ : Type u_2) [CommRing R] {p : ℕ} (hp : p ≠ 0) :

IsLocalHom (expand p)

source

theorem MvPolynomial.of_irreducible_expand {R : Type u_1} (σ : Type u_2) [CommRing R] {p : ℕ} (hp : p ≠ 0) {f : MvPolynomial σ R} (hf : Irreducible ((expand p) f)) :

Irreducible f