# Multivariate polynomials #

This file defines functions for evaluating multivariate polynomials. These include generically evaluating a polynomial given a valuation of all its variables, and more advanced evaluations that allow one to map the coefficients to different rings.

### Notation #

In the definitions below, we use the following notation:

- `σ : Type*` (indexing the variables)
- `R : Type*` `[CommSemiring R]` (the coefficients)
- `s : σ →₀ ℕ`, a function from `σ` to `ℕ` which is zero away from a finite set. This will give rise to a monomial in `MvPolynomial σ R` which mathematicians might call `X^s`
- `a : R`
- `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians
- `p : MvPolynomial σ R`

### Definitions #

- `eval₂ (f : R → S₁) (g : σ → S₁) p` : given a semiring homomorphism from `R` to another semiring `S₁`, and a map `σ → S₁`, evaluates `p` at this valuation, returning a term of type `S₁`. Note that `eval₂` can be made using `eval` and `map` (see below), and it has been suggested that sticking to `eval` and `map` might make the code less brittle.
- `eval (g : σ → R) p` : given a map `σ → R`, evaluates `p` at this valuation, returning a term of type `R`
- `map (f : R → S₁) p` : returns the multivariate polynomial obtained from `p` by the change of coefficient semiring corresponding to `f`
- `aeval (g : σ → S₁) p` : evaluates the multivariate polynomial obtained from `p` by the change of coefficient semiring corresponding to `g` (`a` stands for `Algebra`)

source
def MvPolynomial.eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
S₁

Evaluate a polynomial `p` given a valuation `g` of all the variables and a ring hom `f` from the scalar ring to the target

Equations

- MvPolynomial.eval₂ f g p = Finsupp.sum p fun (s : σ →₀ ℕ) (a : R) => f a * s.prod fun (n : σ) (e : ℕ) => g n ^ e

Instances For

source
theorem MvPolynomial.eval₂_eq {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
eval₂ g X f = ∑ d ∈ f.support, g (coeff d f) * ∏ i ∈ d.support, X i ^ d i
source
theorem MvPolynomial.eval₂_eq' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
eval₂ g X f = ∑ d ∈ f.support, g (coeff d f) * ∏ i : σ, X i ^ d i
source
@[simp]
theorem MvPolynomial.eval₂_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) :
eval₂ f g 0 = 0
source
@[simp]
theorem MvPolynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) :
eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q
source
@[simp]
theorem MvPolynomial.eval₂_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) :
eval₂ f g ((monomial s) a) = f a * s.prod fun (n : σ) (e : ℕ) => g n ^ e
source
@[simp]
theorem MvPolynomial.eval₂_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (a : R) :
eval₂ f g (C a) = f a
source
@[simp]
theorem MvPolynomial.eval₂_one {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) :
eval₂ f g 1 = 1
source
@[simp]
theorem MvPolynomial.eval₂_natCast {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : ℕ) :
eval₂ f g ↑n = ↑n
source
@[simp]
theorem MvPolynomial.eval₂_ofNat {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : ℕ) [n.AtLeastTwo] :
eval₂ f g (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem MvPolynomial.eval₂_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : σ) :
eval₂ f g (X n) = g n
source
theorem MvPolynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {s : σ →₀ ℕ} {a : R} :
eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun (n : σ) (e : ℕ) => g n ^ e
source
theorem MvPolynomial.eval₂_mul_C {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) :
eval₂ f g (p * C a) = eval₂ f g p * f a
source
@[simp]
theorem MvPolynomial.eval₂_mul {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R} :
eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q
source
@[simp]
theorem MvPolynomial.eval₂_pow {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R} {n : ℕ} :
eval₂ f g (p ^ n) = eval₂ f g p ^ n
source
def MvPolynomial.eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) :
MvPolynomial σ R →+* S₁

`MvPolynomial.eval₂` as a `RingHom`.

Equations

- MvPolynomial.eval₂Hom f g = { toFun := MvPolynomial.eval₂ f g, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
theorem MvPolynomial.eval₂_dvd {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) {p q : MvPolynomial σ R} (h : p ∣ q) :
eval₂ f g p ∣ eval₂ f g q
source
@[simp]
theorem MvPolynomial.coe_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) :
⇑(eval₂Hom f g) = eval₂ f g
source
theorem MvPolynomial.eval₂Hom_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f₁ f₂ : R →+* S₁} {g₁ g₂ : σ → S₁} {p₁ p₂ : MvPolynomial σ R} :
f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₂ g₂) p₂
source
@[simp]
theorem MvPolynomial.eval₂Hom_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (r : R) :
(eval₂Hom f g) (C r) = f r
source
@[simp]
theorem MvPolynomial.eval₂Hom_X' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (i : σ) :
(eval₂Hom f g) (X i) = g i
source
@[simp]
theorem MvPolynomial.comp_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) :
φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun (i : σ) => φ (g i)
source
theorem MvPolynomial.map_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
φ ((eval₂Hom f g) p) = (eval₂Hom (φ.comp f) fun (i : σ) => φ (g i)) p
source
theorem MvPolynomial.eval₂Hom_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
(eval₂Hom f g) ((monomial d) r) = f r * d.prod fun (i : σ) (k : ℕ) => g i ^ k
source
theorem MvPolynomial.eval₂_comp_left {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p
source
@[simp]
theorem MvPolynomial.eval₂_eta {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
eval₂ C X p = p
source
theorem MvPolynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g₁ g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i) :
eval₂ f g₁ p = eval₂ f g₂ p
source
@[simp]
theorem MvPolynomial.eval₂_sum {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R) :
eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, eval₂ f g (p x)
source
@[simp]
theorem MvPolynomial.eval₂_prod {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R) :
eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, eval₂ f g (p x)
source
theorem MvPolynomial.eval₂_assoc {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R) :
eval₂ f (fun (t : S₂) => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)
source
def MvPolynomial.eval {R : Type u} {σ : Type u_1} [CommSemiring R] (f : σ → R) :
MvPolynomial σ R →+* R

Evaluate a polynomial `p` given a valuation `f` of all the variables

Equations

- MvPolynomial.eval f = MvPolynomial.eval₂Hom (RingHom.id R) f

Instances For

source
theorem MvPolynomial.eval_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (X : σ → R) (f : MvPolynomial σ R) :
(eval X) f = ∑ d ∈ f.support, coeff d f * ∏ i ∈ d.support, X i ^ d i
source
theorem MvPolynomial.eval_eq' {R : Type u} {σ : Type u_1} [CommSemiring R] [Fintype σ] (X : σ → R) (f : MvPolynomial σ R) :
(eval X) f = ∑ d ∈ f.support, coeff d f * ∏ i : σ, X i ^ d i
source
theorem MvPolynomial.eval_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] {f : σ → R} :
(eval f) ((monomial s) a) = a * s.prod fun (n : σ) (e : ℕ) => f n ^ e
source
@[simp]
theorem MvPolynomial.eval_C {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σ → R} (a : R) :
(eval f) (C a) = a
source
@[simp]
theorem MvPolynomial.eval_X {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σ → R} (n : σ) :
(eval f) (X n) = f n
source
@[simp]
theorem MvPolynomial.eval_ofNat {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σ → R} (n : ℕ) [n.AtLeastTwo] :
(eval f) (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem MvPolynomial.smul_eval {R : Type u} {σ : Type u_1} [CommSemiring R] (x : σ → R) (p : MvPolynomial σ R) (s : R) :
(eval x) (s • p) = s * (eval x) p
source
theorem MvPolynomial.eval_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} {f : σ → R} :
(eval f) (p + q) = (eval f) p + (eval f) q
source
theorem MvPolynomial.eval_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} {f : σ → R} :
(eval f) (p * q) = (eval f) p * (eval f) q
source
theorem MvPolynomial.eval_pow {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {f : σ → R} (n : ℕ) :
(eval f) (p ^ n) = (eval f) p ^ n
source
theorem MvPolynomial.eval_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
(eval g) (∑ i ∈ s, f i) = ∑ i ∈ s, (eval g) (f i)
source
theorem MvPolynomial.eval_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
(eval g) (∏ i ∈ s, f i) = ∏ i ∈ s, (eval g) (f i)
source
theorem MvPolynomial.eval_assoc {R : Type u} {σ : Type u_1} [CommSemiring R] {τ : Type u_2} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPolynomial σ R) :
(eval (⇑(eval g) ∘ f)) p = (eval g) (eval₂ C f p)
source
@[simp]
theorem MvPolynomial.eval₂_id {R : Type u} {σ : Type u_1} [CommSemiring R] {g : σ → R} (p : MvPolynomial σ R) :
eval₂ (RingHom.id R) g p = (eval g) p
source
theorem MvPolynomial.eval_eval₂ {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {τ : Type u_3} {x : τ → S} [CommSemiring S] (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (p : MvPolynomial σ R) :
(eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun (s : σ) => (eval x) (g s)) p
source
def MvPolynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) :
MvPolynomial σ R →+* MvPolynomial σ S₁

`map f p` maps a polynomial `p` across a ring hom `f`

Equations

- MvPolynomial.map f = MvPolynomial.eval₂Hom (MvPolynomial.C.comp f) MvPolynomial.X

Instances For

source
@[simp]
theorem MvPolynomial.map_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (s : σ →₀ ℕ) (a : R) :
(map f) ((monomial s) a) = (monomial s) (f a)
source
@[simp]
theorem MvPolynomial.map_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (a : R) :
(map f) (C a) = C (f a)
source
@[simp]
theorem MvPolynomial.map_ofNat {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (n : ℕ) [n.AtLeastTwo] :
(map f) (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem MvPolynomial.map_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (n : σ) :
(map f) (X n) = X n
source
theorem MvPolynomial.map_id {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
(map (RingHom.id R)) p = p
source
theorem MvPolynomial.map_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) [CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) :
(map g) ((map f) p) = (map (g.comp f)) p
source
theorem MvPolynomial.eval₂_eq_eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
eval₂ f g p = (eval g) ((map f) p)
source
theorem MvPolynomial.eval₂_comp_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
source
theorem MvPolynomial.map_eval₂ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R) :
(map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
source
theorem MvPolynomial.coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) (m : σ →₀ ℕ) :
coeff m ((map f) p) = f (coeff m p)
source
theorem MvPolynomial.map_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (hf : Function.Injective ⇑f) :
Function.Injective ⇑(map f)
source
theorem MvPolynomial.map_injective_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) :
Function.Injective ⇑(map f) ↔ Function.Injective ⇑f
source
theorem MvPolynomial.map_surjective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (hf : Function.Surjective ⇑f) :
Function.Surjective ⇑(map f)
source
theorem MvPolynomial.map_surjective_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) :
Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f
source
theorem MvPolynomial.map_leftInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse ⇑f ⇑g) :
Function.LeftInverse ⇑(map f) ⇑(map g)

If `f` is a left-inverse of `g` then `map f` is a left-inverse of `map g`.

source
theorem MvPolynomial.map_rightInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.RightInverse ⇑f ⇑g) :
Function.RightInverse ⇑(map f) ⇑(map g)

If `f` is a right-inverse of `g` then `map f` is a right-inverse of `map g`.

source
@[simp]
theorem MvPolynomial.eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
(eval g) ((map f) p) = eval₂ f g p
source
theorem MvPolynomial.eval₂_comp {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → R) (p : MvPolynomial σ R) :
f ((eval g) p) = eval₂ f (⇑f ∘ g) p
source
@[simp]
theorem MvPolynomial.eval₂_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
eval₂ φ g ((map f) p) = eval₂ (φ.comp f) g p
source
@[simp]
theorem MvPolynomial.eval₂Hom_map_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
(eval₂Hom φ g) ((map f) p) = (eval₂Hom (φ.comp f) g) p
source
@[simp]
theorem MvPolynomial.constantCoeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (φ : MvPolynomial σ R) :
constantCoeff ((map f) φ) = f (constantCoeff φ)
source
theorem MvPolynomial.constantCoeff_comp_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) :
constantCoeff.comp (map f) = f.comp constantCoeff
source
theorem MvPolynomial.support_map_subset {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) :
((map f) p).support ⊆ p.support
source
theorem MvPolynomial.support_map_of_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (p : MvPolynomial σ R) {f : R →+* S₁} (hf : Function.Injective ⇑f) :
((map f) p).support = p.support
source
theorem MvPolynomial.C_dvd_iff_map_hom_eq_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (q : R →+* S₁) (r : R) (hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r') (φ : MvPolynomial σ R) :
C r ∣ φ ↔ (map q) φ = 0
source
theorem MvPolynomial.map_mapRange_eq_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) :
(map f) (Finsupp.mapRange g hg φ) = φ ↔ ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ
source
theorem MvPolynomial.coeffs_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) [DecidableEq S₁] :
((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
source
@[simp]
theorem MvPolynomial.coe_coeffs_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) :
↑((map f) p).coeffs ⊆ ⇑f '' ↑p.coeffs
source
theorem MvPolynomial.mem_range_map_iff_coeffs_subset {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {x : MvPolynomial σ S₁} :
x ∈ Set.range ⇑(map f) ↔ ↑x.coeffs ⊆ Set.range ⇑f
source
def MvPolynomial.mapAlgHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂

If `f : S₁ →ₐ[R] S₂` is a morphism of `R`-algebras, then so is `MvPolynomial.map f`.

Equations

- MvPolynomial.mapAlgHom f = { toRingHom := MvPolynomial.map ↑f, commutes' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.mapAlgHom_apply {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) (p : MvPolynomial σ S₁) :
(mapAlgHom f) p = eval₂ (C.comp ↑f) X p
source
@[simp]
theorem MvPolynomial.mapAlgHom_id {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] :
mapAlgHom (AlgHom.id R S₁) = AlgHom.id R (MvPolynomial σ S₁)
source
@[simp]
theorem MvPolynomial.mapAlgHom_coe_ringHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
↑(mapAlgHom f) = map ↑f
source
theorem MvPolynomial.range_mapAlgHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
Subalgebra.toSubmodule (mapAlgHom f).range = coeffsIn σ (Subalgebra.toSubmodule f.range)

### The algebra of multivariate polynomials #

source
def MvPolynomial.aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) :
MvPolynomial σ R →ₐ[R] S₁

A map `σ → S₁` where `S₁` is an algebra over `R` generates an `R`-algebra homomorphism from multivariate polynomials over `σ` to `S₁`.

Equations

- MvPolynomial.aeval f = { toRingHom := MvPolynomial.eval₂Hom (algebraMap R S₁) f, commutes' := ⋯ }

Instances For

source
theorem MvPolynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (p : MvPolynomial σ R) :
(aeval f) p = eval₂ (algebraMap R S₁) f p
source
theorem MvPolynomial.aeval_eq_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (p : MvPolynomial σ R) :
(aeval f) p = (eval₂Hom (algebraMap R S₁) f) p
source
@[simp]
theorem MvPolynomial.coe_aeval_eq_eval {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] (f : σ → S₁) :
↑(aeval f) = eval f
source
@[simp]
theorem MvPolynomial.aeval_eq_eval {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] (f : σ → S₁) :
⇑(aeval f) = ⇑(eval f)
source
@[simp]
theorem MvPolynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (s : σ) :
(aeval f) (X s) = f s
source
theorem MvPolynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (r : R) :
(aeval f) (C r) = (algebraMap R S₁) r
source
@[simp]
theorem MvPolynomial.aeval_ofNat {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (n : ℕ) [n.AtLeastTwo] :
(aeval f) (OfNat.ofNat n) = OfNat.ofNat n
source
theorem MvPolynomial.aeval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (φ : MvPolynomial σ R →ₐ[R] S₁) :
φ = aeval (⇑φ ∘ X)
source
theorem MvPolynomial.aeval_X_left {R : Type u} {σ : Type u_1} [CommSemiring R] :
aeval X = AlgHom.id R (MvPolynomial σ R)
source
theorem MvPolynomial.aeval_X_left_apply {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
(aeval X) p = p
source
theorem MvPolynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {B : Type u_2} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) :
φ.comp (aeval f) = aeval fun (i : σ) => φ (f i)
source
theorem MvPolynomial.comp_aeval_apply {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {B : Type u_2} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) (p : MvPolynomial σ R) :
φ ((aeval f) p) = (aeval fun (i : σ) => φ (f i)) p
source
@[simp]
theorem MvPolynomial.map_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] {B : Type u_2} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
φ ((aeval g) p) = (eval₂Hom (φ.comp (algebraMap R S₁)) fun (i : σ) => φ (g i)) p
source
@[simp]
theorem MvPolynomial.eval₂Hom_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) :
eval₂Hom f 0 = f.comp constantCoeff
source
@[simp]
theorem MvPolynomial.eval₂Hom_zero' {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) :
(eval₂Hom f fun (x : σ) => 0) = f.comp constantCoeff
source
theorem MvPolynomial.eval₂Hom_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
(eval₂Hom f 0) p = f (constantCoeff p)
source
theorem MvPolynomial.eval₂Hom_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
(eval₂Hom f fun (x : σ) => 0) p = f (constantCoeff p)
source
@[simp]
theorem MvPolynomial.eval₂_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
eval₂ f 0 p = f (constantCoeff p)
source
@[simp]
theorem MvPolynomial.eval₂_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
eval₂ f (fun (x : σ) => 0) p = f (constantCoeff p)
source
@[simp]
theorem MvPolynomial.aeval_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (p : MvPolynomial σ R) :
(aeval 0) p = (algebraMap R S₁) (constantCoeff p)
source
@[simp]
theorem MvPolynomial.aeval_zero' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (p : MvPolynomial σ R) :
(aeval fun (x : σ) => 0) p = (algebraMap R S₁) (constantCoeff p)
source
@[simp]
theorem MvPolynomial.eval_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :
eval 0 = constantCoeff
source
@[simp]
theorem MvPolynomial.eval_zero' {R : Type u} {σ : Type u_1} [CommSemiring R] :
(eval fun (x : σ) => 0) = constantCoeff
source
theorem MvPolynomial.aeval_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
(aeval g) ((monomial d) r) = (algebraMap R S₁) r * d.prod fun (i : σ) (k : ℕ) => g i ^ k
source
theorem MvPolynomial.eval₂Hom_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (g : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0) :
(eval₂Hom f g) φ = 0
source
theorem MvPolynomial.aeval_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] [Algebra R S₂] (f : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, f i = 0) :
(aeval f) φ = 0
source
theorem MvPolynomial.aeval_sum {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {ι : Type u_2} (s : Finset ι) (φ : ι → MvPolynomial σ R) :
(aeval f) (∑ i ∈ s, φ i) = ∑ i ∈ s, (aeval f) (φ i)
source
theorem MvPolynomial.aeval_prod {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {ι : Type u_2} (s : Finset ι) (φ : ι → MvPolynomial σ R) :
(aeval f) (∏ i ∈ s, φ i) = ∏ i ∈ s, (aeval f) (φ i)
source
theorem Algebra.adjoin_range_eq_range_aeval (R : Type u) {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) :
adjoin R (Set.range f) = (MvPolynomial.aeval f).range
source
theorem Algebra.adjoin_eq_range (R : Type u) {S₁ : Type v} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (s : Set S₁) :
adjoin R s = (MvPolynomial.aeval Subtype.val).range
source
def MvPolynomial.aevalTower {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (f : R →ₐ[S] A) (X : σ → A) :
MvPolynomial σ R →ₐ[S] A

Version of `aeval` for defining algebra homs out of `MvPolynomial σ R` over a smaller base ring than `R`.

Equations

- MvPolynomial.aevalTower f X = { toRingHom := MvPolynomial.eval₂Hom (↑f) X, commutes' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.aevalTower_X {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (i : σ) :
(aevalTower g y) (X i) = y i
source
@[simp]
theorem MvPolynomial.aevalTower_C {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) :
(aevalTower g y) (C x) = g x
source
@[simp]
theorem MvPolynomial.aevalTower_ofNat {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (n : ℕ) [n.AtLeastTwo] :
(aevalTower g y) (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem MvPolynomial.aevalTower_comp_C {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) :
(↑(aevalTower g y)).comp C = ↑g
source
theorem MvPolynomial.aevalTower_algebraMap {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) :
(aevalTower g y) ((algebraMap R (MvPolynomial σ R)) x) = g x
source
theorem MvPolynomial.aevalTower_comp_algebraMap {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) :
(↑(aevalTower g y)).comp (algebraMap R (MvPolynomial σ R)) = ↑g
source
theorem MvPolynomial.aevalTower_toAlgHom {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) :
(aevalTower g y) ((IsScalarTower.toAlgHom S R (MvPolynomial σ R)) x) = g x
source
@[simp]
theorem MvPolynomial.aevalTower_comp_toAlgHom {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) :
(aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g
source
@[simp]
theorem MvPolynomial.aevalTower_id {σ : Type u_1} {S : Type u_2} [CommSemiring S] :
aevalTower (AlgHom.id S S) = aeval
source
@[simp]
theorem MvPolynomial.aevalTower_ofId {σ : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S A] :
aevalTower (Algebra.ofId S A) = aeval
source
theorem MvPolynomial.eval₂_mem {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {f : R →+* S} {p : MvPolynomial σ R} {s : subS} (hs : ∀ i ∈ p.support, f (coeff i p) ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) :
eval₂ f v p ∈ s
source
theorem MvPolynomial.eval_mem {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ p.support, coeff i p ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) :
(eval v) p ∈ s
source
theorem MvPolynomial.aeval_sumElim {R : Type u} [CommSemiring R] {S : Type u_2} {T : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {σ : Type u_4} {τ : Type u_5} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
(aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
source
noncomputable def MvPolynomial.algebraMvPolynomial {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] :
Algebra (MvPolynomial σ R) (MvPolynomial σ S)

If `S` is an `R`-algebra, then `MvPolynomial σ S` is a `MvPolynomial σ R` algebra.

Warning: This produces a diamond for `Algebra (MvPolynomial σ R) (MvPolynomial σ (MvPolynomial σ S))`. That's why it is not a global instance.

Equations

- MvPolynomial.algebraMvPolynomial = (MvPolynomial.map (algebraMap R S)).toAlgebra

Instances For

source
@[simp]
theorem MvPolynomial.algebraMap_def {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] :
algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = map (algebraMap R S)
source
instance MvPolynomial.instIsScalarTower {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] :
IsScalarTower R (MvPolynomial σ R) (MvPolynomial σ S)
source
instance MvPolynomial.instFaithfulSMul {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [FaithfulSMul R S] :
FaithfulSMul (MvPolynomial σ R) (MvPolynomial σ S)