Mathlib.Algebra.MvPolynomial.Eval

MvPolynomial.eval₂ definition

(p : MvPolynomial σ R) : S₁

Full source

/-- Evaluate a polynomial `p` given a valuation `g` of all the variables
  and a ring hom `f` from the scalar ring to the target -/
def eval₂ (p : MvPolynomial σ R) : S₁ :=
  p.sum fun s a => f a * s.prod fun n e => g n ^ e

Evaluation of multivariate polynomials via semiring homomorphism and valuation

Informal description

Given a multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, a semiring homomorphism $f: R \to S_1$, and a valuation $g: \sigma \to S_1$, the evaluation $\text{eval}_2(f, g, p)$ is defined as the sum over all monomials in $p$ of the product of $f$ applied to the coefficient of the monomial and the monomial evaluated at $g$, i.e., \[ \text{eval}_2(f, g, p) = \sum_{s \in \text{support}(p)} f(p_s) \cdot \prod_{n \in \sigma} (g(n))^{s(n)} \] where $p_s$ denotes the coefficient of the monomial $s$ in $p$.

MvPolynomial.eval₂_eq theorem

 (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
  f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i ∈ d.support, X i ^ d i

Full source

theorem eval₂_eq (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
    f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i ∈ d.support, X i ^ d i :=
  rfl

Evaluation Formula for Multivariate Polynomials via Semiring Homomorphism

Informal description

Let $R$ and $S_1$ be commutative semirings, $g : R \to S_1$ be a semiring homomorphism, $X : \sigma \to S_1$ be a valuation of the variables, and $f \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. Then the evaluation of $f$ via $g$ and $X$ is given by: \[ f.\text{eval}_2(g, X) = \sum_{d \in \text{support}(f)} g(f_d) \cdot \prod_{i \in \text{support}(d)} X_i^{d_i} \] where $f_d$ denotes the coefficient of the monomial $d$ in $f$, and $d_i$ is the exponent of variable $i$ in $d$.

MvPolynomial.eval₂_eq' theorem

 [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
  f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i, X i ^ d i

Full source

theorem eval₂_eq' [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
    f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i, X i ^ d i := by
  simp only [eval₂_eq, ← Finsupp.prod_pow]
  rfl

Evaluation Formula for Multivariate Polynomials over Finite Variable Set

Informal description

Let $\sigma$ be a finite type, $R$ and $S_1$ be commutative semirings, $g : R \to S_1$ be a semiring homomorphism, $X : \sigma \to S_1$ be a valuation of the variables, and $f \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. Then the evaluation of $f$ via $g$ and $X$ is given by: \[ f.\text{eval}_2(g, X) = \sum_{d \in \text{support}(f)} g(f_d) \cdot \prod_{i \in \sigma} X_i^{d_i} \] where $f_d$ denotes the coefficient of the monomial $d$ in $f$, and $d_i$ is the exponent of variable $i$ in $d$.

MvPolynomial.eval₂_zero theorem

: (0 : MvPolynomial σ R).eval₂ f g = 0

Full source

@[simp]
theorem eval₂_zero : (0 : MvPolynomial σ R).eval₂ f g = 0 :=
  Finsupp.sum_zero_index

Evaluation of Zero Polynomial Yields Zero

Informal description

For any commutative semiring $R$, type $\sigma$ indexing variables, commutative semiring $S_1$, semiring homomorphism $f: R \to S_1$, and valuation $g: \sigma \to S_1$, the evaluation of the zero polynomial satisfies: \[ \text{eval}_2(f, g, 0) = 0 \]

MvPolynomial.eval₂_add theorem

: (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g

Full source

@[simp]
theorem eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g := by
  classical exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

Additivity of Multivariate Polynomial Evaluation via Semiring Homomorphism

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $p, q \in \text{MvPolynomial}(\sigma, R)$ be multivariate polynomials. Given a semiring homomorphism $f: R \to S_1$ and a valuation $g: \sigma \to S_1$, the evaluation of the sum $p + q$ satisfies: \[ \text{eval}_2(f, g, p + q) = \text{eval}_2(f, g, p) + \text{eval}_2(f, g, q) \]

MvPolynomial.eval₂_monomial theorem

: (monomial s a).eval₂ f g = f a * s.prod fun n e => g n ^ e

Full source

@[simp]
theorem eval₂_monomial : (monomial s a).eval₂ f g = f a * s.prod fun n e => g n ^ e :=
  Finsupp.sum_single_index (by simp [f.map_zero])

Evaluation of Monomial via Semiring Homomorphism and Valuation

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $MvPolynomial(\sigma, R)$ be the ring of multivariate polynomials over $\sigma$ with coefficients in $R$. Given: - A semiring homomorphism $f: R \to S_1$ - A valuation $g: \sigma \to S_1$ - A finitely supported function $s: \sigma \to \mathbb{N}$ representing a monomial - A coefficient $a \in R$ The evaluation of the monomial $X^s$ with coefficient $a$ is given by: \[ \text{eval}_2(f, g, aX^s) = f(a) \cdot \prod_{n \in \sigma} (g(n))^{s(n)} \] where the product is taken over all variables $n \in \sigma$ in the support of $s$.

MvPolynomial.eval₂_C theorem

(a) : (C a).eval₂ f g = f a

Full source

@[simp]
theorem eval₂_C (a) : (C a).eval₂ f g = f a := by
  rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]

Evaluation of Constant Polynomial via Semiring Homomorphism

Informal description

Let $R$ and $S_1$ be commutative semirings, and let $f: R \to S_1$ be a semiring homomorphism. For any constant polynomial $C(a) \in \text{MvPolynomial}(\sigma, R)$ (where $a \in R$) and any valuation $g: \sigma \to S_1$, the evaluation of $C(a)$ satisfies: \[ \text{eval}_2(f, g, C(a)) = f(a) \]

MvPolynomial.eval₂_one theorem

: (1 : MvPolynomial σ R).eval₂ f g = 1

Full source

@[simp]
theorem eval₂_one : (1 : MvPolynomial σ R).eval₂ f g = 1 :=
  (eval₂_C _ _ _).trans f.map_one

Evaluation of the Constant One Polynomial via Semiring Homomorphism

Informal description

Given a commutative semiring $R$, a type $\sigma$ indexing variables, a commutative semiring $S_1$, a semiring homomorphism $f: R \to S_1$, and a valuation $g: \sigma \to S_1$, the evaluation of the constant polynomial $1 \in \text{MvPolynomial}(\sigma, R)$ satisfies: \[ \text{eval}_2(f, g, 1) = 1 \]

MvPolynomial.eval₂_natCast theorem

(n : Nat) : (n : MvPolynomial σ R).eval₂ f g = n

Full source

@[simp] theorem eval₂_natCast (n : Nat) : (n : MvPolynomial σ R).eval₂ f g = n :=
  (eval₂_C _ _ _).trans (map_natCast f n)

Evaluation of Natural Number Constants in Multivariate Polynomials: $\text{eval}_2(f, g, n) = n$

Informal description

For any natural number $n$, the evaluation of the constant polynomial $n$ in $\text{MvPolynomial}(\sigma, R)$ via the semiring homomorphism $f \colon R \to S_1$ and valuation $g \colon \sigma \to S_1$ equals $n$, i.e., \[ \text{eval}_2(f, g, n) = n. \]

MvPolynomial.eval₂_ofNat theorem

(n : Nat) [n.AtLeastTwo] : (ofNat(n) : MvPolynomial σ R).eval₂ f g = ofNat(n)

Full source

@[simp] theorem eval₂_ofNat (n : Nat) [n.AtLeastTwo] :
    (ofNat(n) : MvPolynomial σ R).eval₂ f g = ofNat(n) :=
  eval₂_natCast f g n

Evaluation of Numerals ≥ 2 in Multivariate Polynomials: $\text{eval}_2(f, g, n) = n$

Informal description

For any natural number $n \geq 2$, the evaluation of the constant polynomial $n$ in $\text{MvPolynomial}(\sigma, R)$ via the semiring homomorphism $f \colon R \to S_1$ and valuation $g \colon \sigma \to S_1$ equals $n$, i.e., \[ \text{eval}_2(f, g, n) = n. \]

MvPolynomial.eval₂_X theorem

(n) : (X n).eval₂ f g = g n

Full source

@[simp]
theorem eval₂_X (n) : (X n).eval₂ f g = g n := by
  simp [eval₂_monomial, f.map_one, X, prod_single_index, pow_one]

Evaluation of variable polynomial: $\text{eval}_2(f, g, X_n) = g(n)$

Informal description

Given a semiring homomorphism $f: R \to S_1$ and a valuation $g: \sigma \to S_1$, the evaluation of the monomial $X_n$ (the polynomial variable corresponding to index $n \in \sigma$) via $\text{eval}_2$ satisfies $\text{eval}_2(f, g, X_n) = g(n)$.

MvPolynomial.eval₂_mul_monomial theorem

: ∀ {s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod fun n e => g n ^ e

Full source

theorem eval₂_mul_monomial :
    ∀ {s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod fun n e => g n ^ e := by
  classical
  apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    exact
      calc (p * X n * monomial s a).eval₂ f g
        _ = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g := by
          rw [monomial_single_add, pow_one, mul_assoc]
        _ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
          simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
            f.map_one]

Evaluation of Polynomial-Monomial Product via Semiring Homomorphism and Valuation: $\text{eval}_2(f, g, p \cdot (aX^s)) = \text{eval}_2(f, g, p) \cdot f(a) \cdot \prod_n g(n)^{s(n)}$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $p \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. Given a semiring homomorphism $f: R \to S_1$, a valuation $g: \sigma \to S_1$, a finitely supported function $s: \sigma \to \mathbb{N}$ representing a monomial, and a coefficient $a \in R$, the evaluation of the product $p \cdot (aX^s)$ satisfies: \[ \text{eval}_2(f, g, p \cdot (aX^s)) = \text{eval}_2(f, g, p) \cdot f(a) \cdot \prod_{n \in \sigma} (g(n))^{s(n)} \] where the product is taken over all variables $n \in \sigma$ in the support of $s$.

MvPolynomial.eval₂_mul_C theorem

: (p * C a).eval₂ f g = p.eval₂ f g * f a

Full source

theorem eval₂_mul_C : (p * C a).eval₂ f g = p.eval₂ f g * f a :=
  (eval₂_mul_monomial _ _).trans <| by simp

Evaluation of Polynomial-Constant Product via Semiring Homomorphism: $\text{eval}_2(f, g, p \cdot C(a)) = \text{eval}_2(f, g, p) \cdot f(a)$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $p \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. Given a semiring homomorphism $f: R \to S_1$, a valuation $g: \sigma \to S_1$, and a coefficient $a \in R$, the evaluation of the product $p \cdot C(a)$ (where $C(a)$ is the constant polynomial with coefficient $a$) satisfies: \[ \text{eval}_2(f, g, p \cdot C(a)) = \text{eval}_2(f, g, p) \cdot f(a) \]

MvPolynomial.eval₂_mul theorem

: ∀ {p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g

Full source

@[simp]
theorem eval₂_mul : ∀ {p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g := by
  apply MvPolynomial.induction_on q
  · simp [eval₂_C, eval₂_mul_C]
  · simp +contextual [mul_add, eval₂_add]
  · simp +contextual [X, eval₂_monomial, eval₂_mul_monomial, ← mul_assoc]

Multiplicativity of Multivariate Polynomial Evaluation via Semiring Homomorphism: $\text{eval}_2(f, g, p \cdot q) = \text{eval}_2(f, g, p) \cdot \text{eval}_2(f, g, q)$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $p, q \in \text{MvPolynomial}(\sigma, R)$ be multivariate polynomials. Given a semiring homomorphism $f: R \to S_1$ and a valuation $g: \sigma \to S_1$, the evaluation of the product $p \cdot q$ satisfies: \[ \text{eval}_2(f, g, p \cdot q) = \text{eval}_2(f, g, p) \cdot \text{eval}_2(f, g, q) \]

MvPolynomial.eval₂_pow theorem

{p : MvPolynomial σ R} : ∀ {n : ℕ}, (p ^ n).eval₂ f g = p.eval₂ f g ^ n

Full source

@[simp]
theorem eval₂_pow {p : MvPolynomial σ R} : ∀ {n : ℕ}, (p ^ n).eval₂ f g = p.eval₂ f g ^ n
  | 0 => by
    rw [pow_zero, pow_zero]
    exact eval₂_one _ _
  | n + 1 => by rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]

Power Evaluation of Multivariate Polynomials via Semiring Homomorphism: $\text{eval}_2(f, g, p^n) = \text{eval}_2(f, g, p)^n$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $p \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. Given a semiring homomorphism $f: R \to S_1$, a valuation $g: \sigma \to S_1$, and a natural number $n$, the evaluation of the power $p^n$ satisfies: \[ \text{eval}_2(f, g, p^n) = (\text{eval}_2(f, g, p))^n \]

MvPolynomial.eval₂Hom definition

(f : R →+* S₁) (g : σ → S₁) : MvPolynomial σ R →+* S₁

Full source

/-- `MvPolynomial.eval₂` as a `RingHom`. -/
def eval₂Hom (f : R →+* S₁) (g : σ → S₁) : MvPolynomialMvPolynomial σ R →+* S₁ where
  toFun := eval₂ f g
  map_one' := eval₂_one _ _
  map_mul' _ _ := eval₂_mul _ _
  map_zero' := eval₂_zero f g
  map_add' _ _ := eval₂_add _ _

Ring homomorphism induced by evaluation of multivariate polynomials

Informal description

Given a semiring homomorphism $ f: R \to S_1 $ and a valuation $ g: \sigma \to S_1 $, the function $ \text{eval₂Hom}(f, g) $ is the ring homomorphism from the multivariate polynomial ring $ \text{MvPolynomial}(\sigma, R) $ to $ S_1 $ defined by evaluating each polynomial at $ g $ after applying $ f $ to its coefficients. Specifically, it satisfies: \[ \text{eval₂Hom}(f, g)(1) = 1, \quad \text{eval₂Hom}(f, g)(p + q) = \text{eval₂Hom}(f, g)(p) + \text{eval₂Hom}(f, g)(q), \quad \text{eval₂Hom}(f, g)(p \cdot q) = \text{eval₂Hom}(f, g)(p) \cdot \text{eval₂Hom}(f, g)(q). \]

MvPolynomial.coe_eval₂Hom theorem

(f : R →+* S₁) (g : σ → S₁) : ⇑(eval₂Hom f g) = eval₂ f g

Full source

@[simp]
theorem coe_eval₂Hom (f : R →+* S₁) (g : σ → S₁) : ⇑(eval₂Hom f g) = eval₂ f g :=
  rfl

Equality of Evaluation Homomorphism and Evaluation Function on Multivariate Polynomials

Informal description

For any semiring homomorphism $f: R \to S_1$ and valuation $g: \sigma \to S_1$, the underlying function of the ring homomorphism $\text{eval₂Hom}(f, g)$ is equal to the evaluation function $\text{eval}_2(f, g)$ on multivariate polynomials. That is, for any $p \in \text{MvPolynomial}(\sigma, R)$, we have: \[ \text{eval₂Hom}(f, g)(p) = \text{eval}_2(f, g, p) \]

MvPolynomial.eval₂Hom_congr theorem

 {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₂

Full source

theorem eval₂Hom_congr {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₂ := by
  rintro rfl rfl rfl; rfl

Congruence of Evaluation Homomorphism for Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ a type indexing variables, and $f_1, f_2: R \to S_1$ semiring homomorphisms. Given two valuations $g_1, g_2: \sigma \to S_1$ and two multivariate polynomials $p_1, p_2 \in \text{MvPolynomial}(\sigma, R)$, if $f_1 = f_2$, $g_1 = g_2$, and $p_1 = p_2$, then the evaluation homomorphisms satisfy $\text{eval₂Hom}(f_1, g_1)(p_1) = \text{eval₂Hom}(f_2, g_2)(p_2)$.

MvPolynomial.eval₂Hom_C theorem

(f : R →+* S₁) (g : σ → S₁) (r : R) : eval₂Hom f g (C r) = f r

Full source

@[simp]
theorem eval₂Hom_C (f : R →+* S₁) (g : σ → S₁) (r : R) : eval₂Hom f g (C r) = f r :=
  eval₂_C f g r

Evaluation Homomorphism of Constant Polynomial Equals Coefficient Homomorphism

Informal description

Let $R$ and $S_1$ be commutative semirings, $f: R \to S_1$ be a semiring homomorphism, and $g: \sigma \to S_1$ be a valuation. For any constant polynomial $C(r) \in \text{MvPolynomial}(\sigma, R)$ where $r \in R$, the evaluation homomorphism satisfies: \[ \text{eval₂Hom}(f, g)(C(r)) = f(r) \]

MvPolynomial.eval₂Hom_X' theorem

(f : R →+* S₁) (g : σ → S₁) (i : σ) : eval₂Hom f g (X i) = g i

Full source

@[simp]
theorem eval₂Hom_X' (f : R →+* S₁) (g : σ → S₁) (i : σ) : eval₂Hom f g (X i) = g i :=
  eval₂_X f g i

Evaluation of Variable Polynomial via Homomorphism: $\text{eval₂Hom}(f, g)(X_i) = g(i)$

Informal description

Given a semiring homomorphism $f \colon R \to S_1$ and a valuation $g \colon \sigma \to S_1$, the evaluation homomorphism $\text{eval₂Hom}(f, g)$ applied to the monomial $X_i$ (the polynomial variable corresponding to index $i \in \sigma$) satisfies $\text{eval₂Hom}(f, g)(X_i) = g(i)$.

MvPolynomial.comp_eval₂Hom theorem

 [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) :
  φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i => φ (g i)

Full source

@[simp]
theorem comp_eval₂Hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) :
    φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i => φ (g i) := by
  apply MvPolynomial.ringHom_ext
  · intro r
    rw [RingHom.comp_apply, eval₂Hom_C, eval₂Hom_C, RingHom.comp_apply]
  · intro i
    rw [RingHom.comp_apply, eval₂Hom_X', eval₂Hom_X']

Composition of Ring Homomorphisms with Evaluation Homomorphism for Multivariate Polynomials

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings. Given a semiring homomorphism $f \colon R \to S_1$, a valuation $g \colon \sigma \to S_1$, and another semiring homomorphism $\varphi \colon S_1 \to S_2$, the composition of $\varphi$ with the evaluation homomorphism $\text{eval₂Hom}(f, g)$ is equal to the evaluation homomorphism obtained by composing $\varphi$ with $f$ and applying $\varphi$ to the valuation $g$. That is: \[ \varphi \circ \text{eval₂Hom}(f, g) = \text{eval₂Hom}(\varphi \circ f, \lambda i, \varphi(g(i))). \]

MvPolynomial.map_eval₂Hom theorem

 [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

Full source

theorem map_eval₂Hom [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 := by
  rw [← comp_eval₂Hom]
  rfl

Compatibility of Evaluation Homomorphism with Coefficient Ring Change: $\varphi \circ \text{eval₂Hom}(f, g) = \text{eval₂Hom}(\varphi \circ f, \varphi \circ g)$

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings. Given semiring homomorphisms $f \colon R \to S_1$ and $\varphi \colon S_1 \to S_2$, a valuation $g \colon \sigma \to S_1$, and a multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, we have: \[ \varphi\big(\text{eval₂Hom}(f, g)(p)\big) = \text{eval₂Hom}(\varphi \circ f, \lambda i, \varphi(g(i)))(p). \]

MvPolynomial.eval₂Hom_monomial theorem

 (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

Full source

theorem eval₂Hom_monomial (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 := by
  simp only [monomial_eq, RingHom.map_mul, eval₂Hom_C, Finsupp.prod, map_prod,
    RingHom.map_pow, eval₂Hom_X']

Evaluation Homomorphism of Monomial: $\text{eval₂Hom}(f, g)(X^d \cdot r) = f(r) \cdot \prod_i g(i)^{d(i)}$

Informal description

Let $R$ and $S_1$ be commutative semirings, $f \colon R \to S_1$ be a semiring homomorphism, and $g \colon \sigma \to S_1$ be a valuation. For any monomial $\text{monomial}(d, r) \in \text{MvPolynomial}(\sigma, R)$ with exponent vector $d \colon \sigma \to₀ \mathbb{N}$ and coefficient $r \in R$, the evaluation homomorphism satisfies: \[ \text{eval₂Hom}(f, g)(\text{monomial}(d, r)) = f(r) \cdot \prod_{i \in \sigma} (g(i))^{d(i)} \] where the product is taken over the finite support of $d$.

MvPolynomial.eval₂_comp_left theorem

 {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) : k (eval₂ f g p) = eval₂ (k.comp f) (k ∘ g) p

Full source

theorem eval₂_comp_left {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) :
    k (eval₂ f g p) = eval₂ (k.comp f) (k ∘ g) p := by
  apply MvPolynomial.induction_on p <;>
    simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

Composition of Semiring Homomorphisms Preserves Evaluation of Multivariate Polynomials

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings, and let $f \colon R \to S_1$ and $k \colon S_1 \to S_2$ be semiring homomorphisms. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$ and any valuation $g \colon \sigma \to S_1$, the following equality holds: \[ k\big(\text{eval}_2(f, g, p)\big) = \text{eval}_2(k \circ f, k \circ g, p). \]

MvPolynomial.eval₂_eta theorem

(p : MvPolynomial σ R) : eval₂ C X p = p

Full source

@[simp]
theorem eval₂_eta (p : MvPolynomial σ R) : eval₂ C X p = p := by
  apply MvPolynomial.induction_on p <;>
    simp +contextual [eval₂_add, eval₂_mul]

Identity Evaluation of Multivariate Polynomials via Coefficient and Variable Embeddings

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, evaluating $p$ using the coefficient embedding $C \colon R \to \text{MvPolynomial}(\sigma, R)$ and the variable embedding $X \colon \sigma \to \text{MvPolynomial}(\sigma, R)$ returns $p$ itself, i.e., \[ \text{eval}_2(C, X, p) = p. \]

MvPolynomial.eval₂_congr theorem

 (g₁ g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i) :
  p.eval₂ f g₁ = p.eval₂ f g₂

Full source

theorem eval₂_congr (g₁ g₂ : σ → S₁)
    (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeffcoeff c p ≠ 0 → g₁ i = g₂ i) :
    p.eval₂ f g₁ = p.eval₂ f g₂ := by
  apply Finset.sum_congr rfl
  intro C hc; dsimp; congr 1
  apply Finset.prod_congr rfl
  intro i hi; dsimp; congr 1
  apply h hi
  rwa [Finsupp.mem_support_iff] at hc

Equality of Multivariate Polynomial Evaluations under Congruent Valuations

Informal description

Let $p$ be a multivariate polynomial in $\text{MvPolynomial}(\sigma, R)$, and let $f \colon R \to S_1$ be a semiring homomorphism. Given two valuations $g_1, g_2 \colon \sigma \to S_1$, if for every monomial $c$ in the support of $p$ and every variable $i \in \sigma$ appearing in $c$ (i.e., $i \in \text{support}(c)$ and the coefficient of $c$ in $p$ is nonzero), we have $g_1(i) = g_2(i)$, then the evaluations of $p$ under $g_1$ and $g_2$ coincide, i.e., \[ \text{eval}_2(f, g_1, p) = \text{eval}_2(f, g_2, p). \]

MvPolynomial.eval₂_sum theorem

(s : Finset S₂) (p : S₂ → MvPolynomial σ R) : eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, eval₂ f g (p x)

Full source

theorem eval₂_sum (s : Finset S₂) (p : S₂ → MvPolynomial σ R) :
    eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, eval₂ f g (p x) :=
  map_sum (eval₂Hom f g) _ s

Linearity of Multivariate Polynomial Evaluation over Finite Sums

Informal description

Let $f \colon R \to S_1$ be a semiring homomorphism, $g \colon \sigma \to S_1$ a valuation, and $s$ a finite set. For any family of multivariate polynomials $(p_x)_{x \in s}$ in $\text{MvPolynomial}(\sigma, R)$, the evaluation of the sum of the polynomials equals the sum of their evaluations: \[ \text{eval}_2(f, g, \sum_{x \in s} p_x) = \sum_{x \in s} \text{eval}_2(f, g, p_x). \]

MvPolynomial.eval₂_prod theorem

(s : Finset S₂) (p : S₂ → MvPolynomial σ R) : eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, eval₂ f g (p x)

Full source

@[to_additive existing (attr := simp)]
theorem eval₂_prod (s : Finset S₂) (p : S₂ → MvPolynomial σ R) :
    eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, eval₂ f g (p x) :=
  map_prod (eval₂Hom f g) _ s

Evaluation Preserves Products of Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ a type indexing variables, $f : R \to S_1$ a semiring homomorphism, and $g : \sigma \to S_1$ a valuation. For any finite set $s \subseteq S_2$ and any family of multivariate polynomials $p : S_2 \to \text{MvPolynomial}(\sigma, R)$, the evaluation of the product polynomial equals the product of evaluations: \[ \text{eval}_2(f, g)\left(\prod_{x \in s} p(x)\right) = \prod_{x \in s} \text{eval}_2(f, g)(p(x)). \]

MvPolynomial.eval₂_assoc theorem

 (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R) : eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)

Full source

theorem eval₂_assoc (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R) :
    eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p) := by
  show _ = eval₂Hom f g (eval₂ C q p)
  rw [eval₂_comp_left (eval₂Hom f g)]; congr with a; simp

Associativity of Multivariate Polynomial Evaluation via Semiring Homomorphism

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings, $f \colon R \to S_1$ be a semiring homomorphism, and $g \colon \sigma \to S_1$ be a valuation. For any polynomial $p \in \text{MvPolynomial}(S_2, R)$ and any family of polynomials $q \colon S_2 \to \text{MvPolynomial}(\sigma, R)$, the following associativity property holds: \[ \text{eval}_2\left(f, \left(t \mapsto \text{eval}_2(f, g, q(t))\right), p\right) = \text{eval}_2(f, g, \text{eval}_2(C, q, p)) \] where $C \colon R \to \text{MvPolynomial}(\sigma, R)$ is the constant polynomial embedding.

MvPolynomial.eval definition

(f : σ → R) : MvPolynomial σ R →+* R

Full source

/-- Evaluate a polynomial `p` given a valuation `f` of all the variables -/
def eval (f : σ → R) : MvPolynomialMvPolynomial σ R →+* R :=
  eval₂Hom (RingHom.id _) f

Evaluation of multivariate polynomials

Informal description

Given a valuation $f : \sigma \to R$ of the variables, the function $\text{eval}(f)$ is the ring homomorphism from the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$ to $R$ defined by evaluating each polynomial at $f$. Specifically, it satisfies: \[ \text{eval}(f)(1) = 1, \quad \text{eval}(f)(p + q) = \text{eval}(f)(p) + \text{eval}(f)(q), \quad \text{eval}(f)(p \cdot q) = \text{eval}(f)(p) \cdot \text{eval}(f)(q). \]

MvPolynomial.eval_eq theorem

(X : σ → R) (f : MvPolynomial σ R) : eval X f = ∑ d ∈ f.support, f.coeff d * ∏ i ∈ d.support, X i ^ d i

Full source

theorem eval_eq (X : σ → R) (f : MvPolynomial σ R) :
    eval X f = ∑ d ∈ f.support, f.coeff d * ∏ i ∈ d.support, X i ^ d i :=
  rfl

Evaluation Formula for Multivariate Polynomials

Informal description

For any valuation $X \colon \sigma \to R$ of the variables and any multivariate polynomial $f \in \text{MvPolynomial}(\sigma, R)$, the evaluation of $f$ at $X$ is given by: \[ \text{eval}(X, f) = \sum_{d \in \text{support}(f)} \text{coeff}(f, d) \cdot \prod_{i \in \text{support}(d)} X(i)^{d(i)}, \] where $\text{support}(f)$ denotes the finite set of monomials appearing in $f$ with nonzero coefficients, $\text{coeff}(f, d)$ is the coefficient of the monomial $d$ in $f$, and $\text{support}(d)$ is the finite set of variables appearing in the monomial $d$ with nonzero exponents.

MvPolynomial.eval_eq' theorem

[Fintype σ] (X : σ → R) (f : MvPolynomial σ R) : eval X f = ∑ d ∈ f.support, f.coeff d * ∏ i, X i ^ d i

Full source

theorem eval_eq' [Fintype σ] (X : σ → R) (f : MvPolynomial σ R) :
    eval X f = ∑ d ∈ f.support, f.coeff d * ∏ i, X i ^ d i :=
  eval₂_eq' (RingHom.id R) X f

Evaluation Formula for Multivariate Polynomials over Finite Variables

Informal description

Let $\sigma$ be a finite type and $R$ be a commutative semiring. For any valuation $X : \sigma \to R$ and any multivariate polynomial $f \in \text{MvPolynomial}(\sigma, R)$, the evaluation of $f$ at $X$ is given by: \[ \text{eval}(X, f) = \sum_{d \in \text{support}(f)} f_d \cdot \prod_{i \in \sigma} X_i^{d_i} \] where $f_d$ denotes the coefficient of the monomial $d$ in $f$, and $d_i$ is the exponent of variable $i$ in $d$.

MvPolynomial.eval_monomial theorem

: eval f (monomial s a) = a * s.prod fun n e => f n ^ e

Full source

theorem eval_monomial : eval f (monomial s a) = a * s.prod fun n e => f n ^ e :=
  eval₂_monomial _ _

Evaluation of Monomial in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type indexing variables, and $MvPolynomial(\sigma, R)$ the ring of multivariate polynomials over $\sigma$ with coefficients in $R$. Given: - A valuation $f : \sigma \to R$ of the variables - A finitely supported function $s : \sigma \to \mathbb{N}$ representing a monomial - A coefficient $a \in R$ The evaluation of the monomial $aX^s$ at $f$ is given by: \[ \text{eval}(f, aX^s) = a \cdot \prod_{n \in \sigma} (f(n))^{s(n)} \] where the product is taken over all variables $n \in \sigma$ in the support of $s$.

MvPolynomial.eval_C theorem

: ∀ a, eval f (C a) = a

Full source

@[simp]
theorem eval_C : ∀ a, eval f (C a) = a :=
  eval₂_C _ _

Evaluation of Constant Polynomials: $\text{eval}(f, C(a)) = a$

Informal description

For any constant polynomial $C(a) \in \text{MvPolynomial}(\sigma, R)$ and any valuation $f : \sigma \to R$, the evaluation of $C(a)$ at $f$ is equal to $a$, i.e., \[ \text{eval}(f, C(a)) = a. \]

MvPolynomial.eval_X theorem

: ∀ n, eval f (X n) = f n

Full source

@[simp]
theorem eval_X : ∀ n, eval f (X n) = f n :=
  eval₂_X _ _

Evaluation of Variable Monomial: $\text{eval}(f, X_n) = f(n)$

Informal description

For any variable index $n \in \sigma$, the evaluation of the monomial $X_n$ (the polynomial variable corresponding to $n$) at a valuation $f : \sigma \to R$ satisfies $\text{eval}(f, X_n) = f(n)$.

MvPolynomial.eval_ofNat theorem

(n : Nat) [n.AtLeastTwo] : (ofNat(n) : MvPolynomial σ R).eval f = ofNat(n)

Full source

@[simp] theorem eval_ofNat (n : Nat) [n.AtLeastTwo] :
    (ofNat(n) : MvPolynomial σ R).eval f = ofNat(n) :=
  map_ofNat _ n

Evaluation of Constant Polynomials ≥ 2 in Multivariate Polynomial Ring

Informal description

For any natural number $n \geq 2$ and any valuation $f : \sigma \to R$, the evaluation of the constant polynomial $n$ in the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$ equals $n$, i.e., $\text{eval}(f)(n) = n$.

MvPolynomial.smul_eval theorem

(x) (p : MvPolynomial σ R) (s) : eval x (s • p) = s * eval x p

Full source

@[simp]
theorem smul_eval (x) (p : MvPolynomial σ R) (s) : eval x (s • p) = s * eval x p := by
  rw [smul_eq_C_mul, (eval x).map_mul, eval_C]

Scalar Multiplication Commutes with Evaluation: $\text{eval}(x)(s \cdot p) = s \cdot \text{eval}(x)(p)$

Informal description

For any scalar $s$ in the coefficient ring $R$, any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, and any valuation $x : \sigma \to R$, the evaluation of the scalar multiple $s \cdot p$ at $x$ satisfies: \[ \text{eval}(x)(s \cdot p) = s \cdot \text{eval}(x)(p). \]

MvPolynomial.eval_add theorem

: eval f (p + q) = eval f p + eval f q

Full source

theorem eval_add : eval f (p + q) = eval f p + eval f q :=
  eval₂_add _ _

Additivity of Multivariate Polynomial Evaluation

Informal description

Given a valuation $f : \sigma \to R$ of the variables, the evaluation of the sum of two multivariate polynomials $p$ and $q$ in $\text{MvPolynomial}(\sigma, R)$ satisfies: \[ \text{eval}(f)(p + q) = \text{eval}(f)(p) + \text{eval}(f)(q). \]

MvPolynomial.eval_mul theorem

: eval f (p * q) = eval f p * eval f q

Full source

theorem eval_mul : eval f (p * q) = eval f p * eval f q :=
  eval₂_mul _ _

Multiplicativity of Multivariate Polynomial Evaluation: $\text{eval}(f)(p \cdot q) = \text{eval}(f)(p) \cdot \text{eval}(f)(q)$

Informal description

Given a valuation $f : \sigma \to R$ of the variables, the evaluation of the product of two multivariate polynomials $p$ and $q$ in $\text{MvPolynomial}(\sigma, R)$ satisfies: \[ \text{eval}(f)(p \cdot q) = \text{eval}(f)(p) \cdot \text{eval}(f)(q). \]

MvPolynomial.eval_pow theorem

: ∀ n, eval f (p ^ n) = eval f p ^ n

Full source

theorem eval_pow : ∀ n, eval f (p ^ n) = eval f p ^ n :=
  fun _ => eval₂_pow _ _

Power Evaluation of Multivariate Polynomials: $\text{eval}(f, p^n) = \text{eval}(f, p)^n$

Informal description

For any natural number $n$ and any valuation $f : \sigma \to R$ of the variables, the evaluation of the $n$-th power of a multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$ is equal to the $n$-th power of the evaluation of $p$, i.e., \[ \text{eval}(f, p^n) = (\text{eval}(f, p))^n. \]

MvPolynomial.eval_sum theorem

 {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) : eval g (∑ i ∈ s, f i) = ∑ i ∈ s, eval g (f i)

Full source

theorem eval_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
    eval g (∑ i ∈ s, f i) = ∑ i ∈ s, eval g (f i) :=
  map_sum (eval g) _ _

Evaluation Homomorphism Preserves Finite Sums of Multivariate Polynomials

Informal description

Let $\sigma$ and $R$ be types with $R$ a commutative semiring, and let $\iota$ be an arbitrary type. For any finite set $s \subseteq \iota$, any family of multivariate polynomials $f : \iota \to \text{MvPolynomial}(\sigma, R)$, and any valuation $g : \sigma \to R$, we have: \[ \text{eval}(g)\left(\sum_{i \in s} f(i)\right) = \sum_{i \in s} \text{eval}(g)(f(i)) \] where $\text{eval}(g)$ is the evaluation homomorphism that substitutes each variable $X_i$ with $g(i)$.

MvPolynomial.eval_prod theorem

 {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) : eval g (∏ i ∈ s, f i) = ∏ i ∈ s, eval g (f i)

Full source

@[to_additive existing]
theorem eval_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
    eval g (∏ i ∈ s, f i) = ∏ i ∈ s, eval g (f i) :=
  map_prod (eval g) _ _

Evaluation Commutes with Finite Products of Multivariate Polynomials

Informal description

Let $\sigma$ and $R$ be types, with $R$ a commutative semiring, and let $\iota$ be an arbitrary type. For any finite set $s \subseteq \iota$, any family of multivariate polynomials $f_i \in \text{MvPolynomial}(\sigma, R)$ indexed by $i \in s$, and any valuation $g : \sigma \to R$, the evaluation of the product of polynomials $\prod_{i \in s} f_i$ at $g$ equals the product of the evaluations $\prod_{i \in s} \text{eval}(g)(f_i)$. In other words, the evaluation map $\text{eval}(g)$ commutes with finite products: \[ \text{eval}(g)\left(\prod_{i \in s} f_i\right) = \prod_{i \in s} \text{eval}(g)(f_i). \]

MvPolynomial.eval_assoc theorem

 {τ} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPolynomial σ R) : eval (eval g ∘ f) p = eval g (eval₂ C f p)

Full source

theorem eval_assoc {τ} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPolynomial σ R) :
    eval (evaleval g ∘ f) p = eval g (eval₂ C f p) := by
  rw [eval₂_comp_left (eval g)]
  unfold eval; simp only [coe_eval₂Hom]
  congr with a; simp

Associativity of Evaluation for Multivariate Polynomials: $\text{eval}(g \circ f)(p) = \text{eval}(g)(\text{eval}_2(C, f, p))$

Informal description

Let $\sigma$ and $\tau$ be types, $R$ a commutative semiring, $f : \sigma \to \text{MvPolynomial}(\tau, R)$ a valuation of variables, $g : \tau \to R$ another valuation, and $p \in \text{MvPolynomial}(\sigma, R)$ a multivariate polynomial. Then the evaluation of $p$ at the composed valuation $\text{eval}(g) \circ f$ equals the evaluation at $g$ of the polynomial obtained by substituting $f$ into $p$ via the constant coefficient embedding $C$, i.e., \[ \text{eval}(\text{eval}(g) \circ f)(p) = \text{eval}(g)(\text{eval}_2(C, f, p)). \]

MvPolynomial.eval₂_id theorem

{g : σ → R} (p : MvPolynomial σ R) : eval₂ (RingHom.id _) g p = eval g p

Full source

@[simp]
theorem eval₂_id {g : σ → R} (p : MvPolynomial σ R) : eval₂ (RingHom.id _) g p = eval g p :=
  rfl

Equivalence of Evaluation Methods for Multivariate Polynomials with Identity Homomorphism

Informal description

For any valuation $g : \sigma \to R$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the evaluation $\text{eval}_2(\text{RingHom.id}_R, g, p)$ using the identity ring homomorphism on $R$ is equal to the direct evaluation $\text{eval}(g, p)$. In other words: \[ \text{eval}_2(\text{id}_R, g, p) = \text{eval}(g, p). \]

MvPolynomial.eval_eval₂ theorem

 {S τ : Type*} {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

Full source

theorem eval_eval₂ {S τ : Type*} {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 := by
  apply induction_on p
  · simp
  · intro p q hp hq
    simp [hp, hq]
  · intro p n hp
    simp [hp]

Composition of Evaluations for Multivariate Polynomials: $\text{eval}(x) \circ \text{eval}_2(f, g) = \text{eval}_2(\text{eval}(x) \circ f, \text{eval}(x) \circ g)$

Informal description

Let $R$, $S$, and $\tau$ be commutative semirings, and let $x : \tau \to S$ be a valuation of variables. Given a ring homomorphism $f : R \to \text{MvPolynomial}(\tau, S)$, a map $g : \sigma \to \text{MvPolynomial}(\tau, S)$, and a multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the following equality holds: \[ \text{eval}(x, \text{eval}_2(f, g, p)) = \text{eval}_2(\text{eval}(x) \circ f, \lambda s. \text{eval}(x, g(s)), p). \] Here, $\text{eval}(x)$ denotes the evaluation of polynomials in $\text{MvPolynomial}(\tau, S)$ at $x$, and $\circ$ denotes function composition.

MvPolynomial.map definition

: MvPolynomial σ R →+* MvPolynomial σ S₁

Full source

/-- `map f p` maps a polynomial `p` across a ring hom `f` -/
def map : MvPolynomialMvPolynomial σ R →+* MvPolynomial σ S₁ :=
  eval₂Hom (C.comp f) X

Coefficient mapping of multivariate polynomials

Informal description

Given a semiring homomorphism $ f: R \to S_1 $, the function `map f` is the ring homomorphism from the multivariate polynomial ring $ \text{MvPolynomial}(\sigma, R) $ to $ \text{MvPolynomial}(\sigma, S_1) $ obtained by applying $ f $ to each coefficient of the polynomial while keeping the variables unchanged. Specifically, it satisfies: \[ \text{map}\, f\, (1) = 1, \quad \text{map}\, f\, (p + q) = \text{map}\, f\, (p) + \text{map}\, f\, (q), \quad \text{map}\, f\, (p \cdot q) = \text{map}\, f\, (p) \cdot \text{map}\, f\, (q). \]

MvPolynomial.map_monomial theorem

(s : σ →₀ ℕ) (a : R) : map f (monomial s a) = monomial s (f a)

Full source

@[simp]
theorem map_monomial (s : σ →₀ ℕ) (a : R) : map f (monomial s a) = monomial s (f a) :=
  (eval₂_monomial _ _).trans monomial_eq.symm

Mapping of Monomials under Coefficient Homomorphism: $\text{map}\, f\, (aX^s) = f(a)X^s$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $f: R \to S_1$ be a semiring homomorphism. For any finitely supported function $s: \sigma \to \mathbb{N}$ (representing a monomial) and any coefficient $a \in R$, the mapping of the monomial $aX^s$ under $f$ is given by: \[ \text{map}\, f\, (aX^s) = f(a)X^s \] where $X^s$ denotes the monomial $\prod_{i \in \sigma} X_i^{s(i)}$.

MvPolynomial.map_C theorem

: ∀ a : R, map f (C a : MvPolynomial σ R) = C (f a)

Full source

@[simp]
theorem map_C : ∀ a : R, map f (C a : MvPolynomial σ R) = C (f a) :=
  map_monomial _ _

Mapping of Constant Polynomials: $\text{map}\, f\, (C(a)) = C(f(a))$

Informal description

For any commutative semirings $R$ and $S_1$, any type $\sigma$ indexing variables, and any semiring homomorphism $f: R \to S_1$, the mapping of a constant polynomial $C(a) \in \text{MvPolynomial}(\sigma, R)$ under $f$ is equal to the constant polynomial $C(f(a)) \in \text{MvPolynomial}(\sigma, S_1)$. That is, \[ \text{map}\, f\, (C(a)) = C(f(a)). \]

MvPolynomial.map_ofNat theorem

(n : Nat) [n.AtLeastTwo] : (ofNat(n) : MvPolynomial σ R).map f = ofNat(n)

Full source

@[simp] protected theorem map_ofNat (n : Nat) [n.AtLeastTwo] :
    (ofNat(n) : MvPolynomial σ R).map f = ofNat(n) :=
  _root_.map_ofNat _ _

Preservation of Numerals ≥ 2 under Coefficient Mapping in Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type, and $f: R \to S_1$ be a semiring homomorphism. For any natural number $n \geq 2$, the mapping of the constant polynomial $n$ in $\text{MvPolynomial}(\sigma, R)$ under $f$ equals the constant polynomial $n$ in $\text{MvPolynomial}(\sigma, S_1)$, i.e., \[ \text{map}\, f\, (n) = n. \]

MvPolynomial.map_X theorem

: ∀ n : σ, map f (X n : MvPolynomial σ R) = X n

Full source

@[simp]
theorem map_X : ∀ n : σ, map f (X n : MvPolynomial σ R) = X n :=
  eval₂_X _ _

Invariance of Variables under Coefficient Mapping: $\text{map}\, f\, (X_n) = X_n$

Informal description

For any index $n \in \sigma$ and any semiring homomorphism $f: R \to S_1$, the mapping of the variable polynomial $X_n$ under $f$ satisfies $\text{map}\, f\, (X_n) = X_n$.

MvPolynomial.map_id theorem

: ∀ p : MvPolynomial σ R, map (RingHom.id R) p = p

Full source

theorem map_id : ∀ p : MvPolynomial σ R, map (RingHom.id R) p = p :=
  eval₂_eta

Identity Mapping Preserves Multivariate Polynomials

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the mapping of $p$ under the identity ring homomorphism $\text{id}_R \colon R \to R$ returns $p$ itself, i.e., \[ \text{map}\, \text{id}_R\, p = p. \]

MvPolynomial.map_map theorem

[CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) : map g (map f p) = map (g.comp f) p

Full source

theorem map_map [CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) :
    map g (map f p) = map (g.comp f) p :=
  (eval₂_comp_left (map g) (C.comp f) X p).trans <| by
    congr
    · ext1 a
      simp only [map_C, comp_apply, RingHom.coe_comp]
    · ext1 n
      simp only [map_X, comp_apply]

Composition of Coefficient Mappings for Multivariate Polynomials: $\text{map}\, g \circ \text{map}\, f = \text{map}\, (g \circ f)$

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings, and let $f \colon R \to S_1$ and $g \colon S_1 \to S_2$ be semiring homomorphisms. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the composition of mappings satisfies: \[ \text{map}\, g\, (\text{map}\, f\, p) = \text{map}\, (g \circ f)\, p. \]

MvPolynomial.eval₂_eq_eval_map theorem

(g : σ → S₁) (p : MvPolynomial σ R) : p.eval₂ f g = eval g (map f p)

Full source

theorem eval₂_eq_eval_map (g : σ → S₁) (p : MvPolynomial σ R) : p.eval₂ f g = eval g (map f p) := by
  unfold map eval; simp only [coe_eval₂Hom]

  have h := eval₂_comp_left (eval₂Hom (RingHom.id S₁) g) (C.comp f) X p
  -- Porting note: the Lean 3 version of `h` was full of metavariables which
  -- were later unified during `rw [h]`. Also needed to add `-eval₂_id`.
  dsimp [-eval₂_id] at h
  rw [h]
  congr
  · ext1 a
    simp only [coe_eval₂Hom, RingHom.id_apply, comp_apply, eval₂_C, RingHom.coe_comp]
  · ext1 n
    simp only [comp_apply, eval₂_X]

Equivalence of $\text{eval}_2$ and composition of $\text{map}$ with $\text{eval}$ for multivariate polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $f \colon R \to S_1$ a semiring homomorphism, $g \colon \sigma \to S_1$ a valuation of variables, and $p \in \text{MvPolynomial}(\sigma, R)$ a multivariate polynomial. Then the evaluation of $p$ via $\text{eval}_2$ equals the evaluation of the mapped polynomial via $\text{eval}$: \[ \text{eval}_2(f, g, p) = \text{eval}(g, \text{map}\, f\, p). \]

MvPolynomial.eval₂_comp_right theorem

 {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) : k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p)

Full source

theorem eval₂_comp_right {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) :
    k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p) := by
  apply MvPolynomial.induction_on p
  · intro r
    rw [eval₂_C, map_C, eval₂_C]
  · intro p q hp hq
    rw [eval₂_add, k.map_add, (map f).map_add, eval₂_add, hp, hq]
  · intro p s hp
    rw [eval₂_mul, k.map_mul, (map f).map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X]
    rfl

Compatibility of Evaluation with Semiring Homomorphism Composition: $k \circ \text{eval}_2(f, g, \cdot) = \text{eval}_2(k, k \circ g, \text{map}\, f\, \cdot)$

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings, and let $f \colon R \to S_1$ and $k \colon S_1 \to S_2$ be semiring homomorphisms. For any valuation $g \colon \sigma \to S_1$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the following equality holds: \[ k(\text{eval}_2(f, g, p)) = \text{eval}_2(k, k \circ g, \text{map}\, f\, p). \]

MvPolynomial.map_eval₂ theorem

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

Full source

theorem map_eval₂ (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R) :
    map f (eval₂ C g p) = eval₂ C (mapmap f ∘ g) (map f p) := by
  apply MvPolynomial.induction_on p
  · intro r
    rw [eval₂_C, map_C, map_C, eval₂_C]
  · intro p q hp hq
    rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
  · intro p s hp
    rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X]
    rfl

Commutativity of Map and Evaluation for Multivariate Polynomials: $\text{map}\, f\, \circ \text{eval}_2(C, g) = \text{eval}_2(C, \text{map}\, f\, \circ g) \circ \text{map}\, f$

Informal description

Let $R$, $S_1$, $S_2$, and $S_3$ be commutative semirings, and let $f: R \to S_1$ be a semiring homomorphism. For any polynomial $p \in \text{MvPolynomial}(S_2, R)$ and any map $g: S_2 \to \text{MvPolynomial}(S_3, R)$, the following equality holds: \[ \text{map}\, f\, \big(\text{eval}_2(C, g, p)\big) = \text{eval}_2\big(C, \text{map}\, f\, \circ g, \text{map}\, f\, p\big), \] where $C: R \to \text{MvPolynomial}(S_3, R)$ is the constant embedding.

MvPolynomial.coeff_map theorem

(p : MvPolynomial σ R) : ∀ m : σ →₀ ℕ, coeff m (map f p) = f (coeff m p)

Full source

theorem coeff_map (p : MvPolynomial σ R) : ∀ m : σ →₀ ℕ, coeff m (map f p) = f (coeff m p) := by
  classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    rw [map_C]
    simp only [coeff_C]
    split_ifs
    · rfl
    rw [f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add]
    rw [f.map_add]
  · intro p i hp m
    simp only [hp, (map f).map_mul, map_X]
    simp only [hp, mem_support_iff, coeff_mul_X']
    split_ifs
    · rfl
    rw [f.map_zero]

Coefficient Mapping Formula: $\text{coeff}_m (\text{map}\, f\, p) = f(\text{coeff}_m p)$

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$ and any monomial $m \in \sigma \to_{\text{f}} \mathbb{N}$, the coefficient of $m$ in the polynomial obtained by applying the semiring homomorphism $f: R \to S_1$ to $p$ is equal to $f$ applied to the coefficient of $m$ in $p$. That is, \[ \text{coeff}_m (\text{map}\, f\, p) = f(\text{coeff}_m p). \]

MvPolynomial.map_injective theorem

(hf : Function.Injective f) : Function.Injective (map f : MvPolynomial σ R → MvPolynomial σ S₁)

Full source

theorem map_injective (hf : Function.Injective f) :
    Function.Injective (map f : MvPolynomial σ R → MvPolynomial σ S₁) := by
  intro p q h
  simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢
  intro m
  exact hf (h m)

Injectivity of Coefficient Mapping for Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ a type indexing variables, and $f: R \to S_1$ an injective semiring homomorphism. Then the induced map $\text{map}\, f : \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is also injective.

MvPolynomial.map_injective_iff theorem

: Function.Injective (map (σ := σ) f) ↔ Function.Injective f

Full source

theorem map_injective_iff : Function.InjectiveFunction.Injective (map (σ := σ) f) ↔ Function.Injective f :=
  ⟨fun h r r' eq ↦ by simpa using h (a₁ := C r) (a₂ := C r') (by simpa), map_injective f⟩

Injectivity Criterion for Coefficient Mapping in Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ a type indexing variables, and $f: R \to S_1$ a semiring homomorphism. The induced map $\text{map}\, f : \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is injective if and only if $f$ is injective.

MvPolynomial.map_surjective theorem

(hf : Function.Surjective f) : Function.Surjective (map f : MvPolynomial σ R → MvPolynomial σ S₁)

Full source

theorem map_surjective (hf : Function.Surjective f) :
    Function.Surjective (map f : MvPolynomial σ R → MvPolynomial σ S₁) := fun p => by
  induction p using MvPolynomial.induction_on' with
  | monomial i fr =>
    obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  | add a b ha hb =>
    obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, RingHom.map_add _ _ _⟩

Surjectivity of Coefficient Mapping for Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $f: R \to S_1$ be a surjective semiring homomorphism. Then the induced map $\text{map}\, f : \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is also surjective.

MvPolynomial.map_surjective_iff theorem

: Function.Surjective (map (σ := σ) f) ↔ Function.Surjective f

Full source

theorem map_surjective_iff : Function.SurjectiveFunction.Surjective (map (σ := σ) f) ↔ Function.Surjective f :=
  ⟨fun h s ↦ let ⟨p, h⟩ := h (C s); ⟨p.coeff 0, by simpa [coeff_map] using congr(coeff 0 $h)⟩,
    map_surjective f⟩

Surjectivity Criterion for Coefficient Mapping in Multivariate Polynomials

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, and $f: R \to S_1$ be a semiring homomorphism. The induced map $\text{map}\, f : \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is surjective if and only if $f$ is surjective.

MvPolynomial.map_leftInverse theorem

 {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse f g) :
  Function.LeftInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g)

Full source

/-- If `f` is a left-inverse of `g` then `map f` is a left-inverse of `map g`. -/
theorem map_leftInverse {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse f g) :
    Function.LeftInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g) := fun X => by
  rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), map_id]

Left Inverse Property of Coefficient Mapping for Multivariate Polynomials: $\text{map}\, g \circ \text{map}\, f = \text{id}$

Informal description

Let $R$ and $S_1$ be commutative semirings, and let $f \colon R \to S_1$ and $g \colon S_1 \to R$ be semiring homomorphisms. If $f$ is a left inverse of $g$ (i.e., $f \circ g = \text{id}_{S_1}$), then the induced map $\text{map}\, f \colon \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is a left inverse of $\text{map}\, g \colon \text{MvPolynomial}(\sigma, S_1) \to \text{MvPolynomial}(\sigma, R)$. In other words, for any polynomial $p \in \text{MvPolynomial}(\sigma, R)$, we have: \[ \text{map}\, g\, (\text{map}\, f\, p) = p. \]

MvPolynomial.map_rightInverse theorem

 {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.RightInverse f g) :
  Function.RightInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g)

Full source

/-- If `f` is a right-inverse of `g` then `map f` is a right-inverse of `map g`. -/
theorem map_rightInverse {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.RightInverse f g) :
    Function.RightInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g) :=
  (map_leftInverse hf.leftInverse).rightInverse

Right Inverse Property of Coefficient Mapping for Multivariate Polynomials: $\text{map}\, f \circ \text{map}\, g = \text{id}$

Informal description

Let $R$ and $S_1$ be commutative semirings, and let $f \colon R \to S_1$ and $g \colon S_1 \to R$ be semiring homomorphisms. If $f$ is a right inverse of $g$ (i.e., $f(g(y)) = y$ for all $y \in S_1$), then the induced map $\text{map}\, f \colon \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is a right inverse of $\text{map}\, g \colon \text{MvPolynomial}(\sigma, S_1) \to \text{MvPolynomial}(\sigma, R)$. In other words, for any polynomial $p \in \text{MvPolynomial}(\sigma, S_1)$, we have: \[ \text{map}\, f\, (\text{map}\, g\, p) = p. \]

MvPolynomial.eval_map theorem

(f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : eval g (map f p) = eval₂ f g p

Full source

@[simp]
theorem eval_map (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
    eval g (map f p) = eval₂ f g p := by
  apply MvPolynomial.induction_on p <;> · simp +contextual

Equivalence of Evaluation Methods for Mapped Polynomials: $\text{eval}(g, \text{map}(f)(p)) = \text{eval}_2(f, g, p)$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ be a type indexing variables, $f \colon R \to S_1$ be a semiring homomorphism, and $g \colon \sigma \to S_1$ be a valuation of the variables. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the evaluation of the mapped polynomial $\text{map}(f)(p)$ at $g$ equals the evaluation of $p$ via $\text{eval}_2$ with $f$ and $g$, i.e., \[ \text{eval}(g, \text{map}(f)(p)) = \text{eval}_2(f, g, p). \]

MvPolynomial.eval₂_comp theorem

(f : R →+* S₁) (g : σ → R) (p : MvPolynomial σ R) : f (eval g p) = eval₂ f (f ∘ g) p

Full source

theorem eval₂_comp (f : R →+* S₁) (g : σ → R) (p : MvPolynomial σ R) :
    f (eval g p) = eval₂ f (f ∘ g) p := by
  rw [← p.map_id, eval_map, eval₂_comp_right]

Compatibility of Evaluation with Semiring Homomorphism: $f(\text{eval}(g, p)) = \text{eval}_2(f, f \circ g, p)$

Informal description

Let $R$ and $S_1$ be commutative semirings, $f \colon R \to S_1$ be a semiring homomorphism, and $g \colon \sigma \to R$ be a valuation of the variables. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the image under $f$ of the evaluation of $p$ at $g$ equals the evaluation of $p$ via $\text{eval}_2$ with $f$ and $f \circ g$, i.e., \[ f(\text{eval}(g, p)) = \text{eval}_2(f, f \circ g, p). \]

MvPolynomial.eval₂_map theorem

 [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
  eval₂ φ g (map f p) = eval₂ (φ.comp f) g p

Full source

@[simp]
theorem eval₂_map [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂)
    (p : MvPolynomial σ R) : eval₂ φ g (map f p) = eval₂ (φ.comp f) g p := by
  rw [← eval_map, ← eval_map, map_map]

Evaluation of Mapped Polynomial via Composition of Homomorphisms: $\text{eval}_2(\phi, g, \text{map}(f)(p)) = \text{eval}_2(\phi \circ f, g, p)$

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings, and let $f \colon R \to S_1$ and $\phi \colon S_1 \to S_2$ be semiring homomorphisms. For any valuation $g \colon \sigma \to S_2$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the evaluation of the mapped polynomial $\text{map}(f)(p)$ via $\text{eval}_2$ with $\phi$ and $g$ equals the evaluation of $p$ via $\text{eval}_2$ with the composed homomorphism $\phi \circ f$ and $g$, i.e., \[ \text{eval}_2(\phi, g, \text{map}(f)(p)) = \text{eval}_2(\phi \circ f, g, p). \]

MvPolynomial.eval₂Hom_map_hom theorem

 [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
  eval₂Hom φ g (map f p) = eval₂Hom (φ.comp f) g p

Full source

@[simp]
theorem eval₂Hom_map_hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂)
    (p : MvPolynomial σ R) : eval₂Hom φ g (map f p) = eval₂Hom (φ.comp f) g p :=
  eval₂_map f g φ p

Compatibility of Evaluation Homomorphism with Coefficient Mapping: $\text{eval₂Hom}(\phi, g) \circ \text{map}(f) = \text{eval₂Hom}(\phi \circ f, g)$

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings, and let $f \colon R \to S_1$ and $\phi \colon S_1 \to S_2$ be semiring homomorphisms. For any valuation $g \colon \sigma \to S_2$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the evaluation homomorphism $\text{eval₂Hom}(\phi, g)$ applied to the mapped polynomial $\text{map}(f)(p)$ equals the evaluation homomorphism $\text{eval₂Hom}(\phi \circ f, g)$ applied to $p$, i.e., \[ \text{eval₂Hom}(\phi, g)(\text{map}(f)(p)) = \text{eval₂Hom}(\phi \circ f, g)(p). \]

MvPolynomial.constantCoeff_map theorem

(f : R →+* S₁) (φ : MvPolynomial σ R) : constantCoeff (MvPolynomial.map f φ) = f (constantCoeff φ)

Full source

@[simp]
theorem constantCoeff_map (f : R →+* S₁) (φ : MvPolynomial σ R) :
    constantCoeff (MvPolynomial.map f φ) = f (constantCoeff φ) :=
  coeff_map f φ 0

Constant Coefficient Preservation under Coefficient Mapping: $\text{constantCoeff}(\text{map}\, f\, \varphi) = f(\text{constantCoeff}(\varphi))$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ a type indexing variables, and $f: R \to S_1$ a semiring homomorphism. For any multivariate polynomial $\varphi \in \text{MvPolynomial}(\sigma, R)$, the constant coefficient of the polynomial obtained by applying $f$ to each coefficient of $\varphi$ equals $f$ applied to the constant coefficient of $\varphi$. That is, \[ \text{constantCoeff}(\text{map}\, f\, \varphi) = f(\text{constantCoeff}(\varphi)). \]

MvPolynomial.constantCoeff_comp_map theorem

(f : R →+* S₁) : (constantCoeff : MvPolynomial σ S₁ →+* S₁).comp (MvPolynomial.map f) = f.comp constantCoeff

Full source

theorem constantCoeff_comp_map (f : R →+* S₁) :
    (constantCoeff : MvPolynomialMvPolynomial σ S₁ →+* S₁).comp (MvPolynomial.map f) = f.comp constantCoeff :=
  by ext <;> simp

Composition of Constant Coefficient with Coefficient Mapping: $\text{constantCoeff} \circ \text{map}\, f = f \circ \text{constantCoeff}$

Informal description

For any commutative semirings $R$ and $S_1$, any type $\sigma$ indexing variables, and any semiring homomorphism $f: R \to S_1$, the composition of the constant coefficient function $\text{constantCoeff}: \text{MvPolynomial}(\sigma, S_1) \to S_1$ with the coefficient mapping $\text{map}\, f: \text{MvPolynomial}(\sigma, R) \to \text{MvPolynomial}(\sigma, S_1)$ is equal to the composition of $f$ with $\text{constantCoeff}: \text{MvPolynomial}(\sigma, R) \to R$. That is, \[ \text{constantCoeff} \circ \text{map}\, f = f \circ \text{constantCoeff}. \]

MvPolynomial.support_map_subset theorem

(p : MvPolynomial σ R) : (map f p).support ⊆ p.support

Full source

theorem support_map_subset (p : MvPolynomial σ R) : (map f p).support ⊆ p.support := by
  intro x
  simp only [mem_support_iff]
  contrapose!
  change p.coeff x = 0 → (map f p).coeff x = 0
  rw [coeff_map]
  intro hx
  rw [hx]
  exact RingHom.map_zero f

Support Inclusion Under Coefficient Mapping: $\text{support}(\text{map}\, f\, p) \subseteq \text{support}(p)$

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the support of the polynomial $\text{map}\, f\, p$ (obtained by applying the semiring homomorphism $f: R \to S_1$ to the coefficients of $p$) is a subset of the support of $p$. That is, \[ \text{support}(\text{map}\, f\, p) \subseteq \text{support}(p). \]

MvPolynomial.support_map_of_injective theorem

(p : MvPolynomial σ R) {f : R →+* S₁} (hf : Injective f) : (map f p).support = p.support

Full source

theorem support_map_of_injective (p : MvPolynomial σ R) {f : R →+* S₁} (hf : Injective f) :
    (map f p).support = p.support := by
  apply Finset.Subset.antisymm
  · exact MvPolynomial.support_map_subset _ _
  intro x hx
  rw [mem_support_iff]
  contrapose! hx
  simp only [Classical.not_not, mem_support_iff]
  replace hx : (map f p).coeff x = 0 := hx
  rw [coeff_map, ← f.map_zero] at hx
  exact hf hx

Support Preservation Under Injective Coefficient Mapping: $\text{support}(\text{map}\, f\, p) = \text{support}(p)$

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$ and any injective semiring homomorphism $f: R \to S_1$, the support of the polynomial $\text{map}\, f\, p$ is equal to the support of $p$. That is, \[ \text{support}(\text{map}\, f\, p) = \text{support}(p). \]

MvPolynomial.C_dvd_iff_map_hom_eq_zero theorem

 (q : R →+* S₁) (r : R) (hr : ∀ r' : R, q r' = 0 ↔ r ∣ r') (φ : MvPolynomial σ R) : C r ∣ φ ↔ map q φ = 0

Full source

theorem C_dvd_iff_map_hom_eq_zero (q : R →+* S₁) (r : R) (hr : ∀ r' : R, q r' = 0 ↔ r ∣ r')
    (φ : MvPolynomial σ R) : CC r ∣ φC r ∣ φ ↔ map q φ = 0 := by
  rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_iff]
  simp only [coeff_map, coeff_zero, hr]

Divisibility by Constant Polynomial vs. Vanishing Under Coefficient Mapping

Informal description

Let $R$ and $S_1$ be commutative semirings, $q: R \to S_1$ a semiring homomorphism, and $r \in R$ such that for all $r' \in R$, $q(r') = 0$ if and only if $r$ divides $r'$. Then for any multivariate polynomial $\varphi \in \text{MvPolynomial}(\sigma, R)$, the constant polynomial $C(r)$ divides $\varphi$ if and only if the mapped polynomial $\text{map}\, q\, \varphi$ is zero in $\text{MvPolynomial}(\sigma, S_1)$.

MvPolynomial.map_mapRange_eq_iff theorem

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

Full source

theorem map_mapRange_eq_iff (f : R →+* S₁) (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) :
    mapmap f (Finsupp.mapRange g hg φ) = φ ↔ ∀ d, f (g (coeff d φ)) = coeff d φ := by
  rw [MvPolynomial.ext_iff]
  apply forall_congr'; intro m
  rw [coeff_map]
  apply eq_iff_eq_cancel_right.mpr
  rfl

Equivalence of Polynomial Mapping and Coefficient Preservation under Composition of $f$ and $g$

Informal description

Given a semiring homomorphism $f \colon R \to S_1$, a function $g \colon S_1 \to R$ satisfying $g(0) = 0$, and a multivariate polynomial $\varphi \in \text{MvPolynomial}(\sigma, S_1)$, the following equivalence holds: \[ \text{map}\, f\, (\text{Finsupp.mapRange}\, g\, hg\, \varphi) = \varphi \quad \text{if and only if} \quad \forall d, \ f(g(\text{coeff}_d\, \varphi)) = \text{coeff}_d\, \varphi. \] Here, $\text{coeff}_d\, \varphi$ denotes the coefficient of the monomial $d$ in $\varphi$.

MvPolynomial.mapAlgHom definition

 [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) : MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂

Full source

/-- If `f : S₁ →ₐ[R] S₂` is a morphism of `R`-algebras, then so is `MvPolynomial.map f`. -/
@[simps!]
def mapAlgHom [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
    MvPolynomialMvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂ :=
  { map (↑f : S₁ →+* S₂) with
    commutes' := fun r => by
      have h₁ : algebraMap R (MvPolynomial σ S₁) r = C (algebraMap R S₁ r) := rfl
      have h₂ : algebraMap R (MvPolynomial σ S₂) r = C (algebraMap R S₂ r) := rfl
      simp_rw [OneHom.toFun_eq_coe]
      -- Porting note: we're missing some `simp` lemmas like `MonoidHom.coe_toOneHom`
      change @DFunLike.coe (_ →+* _) _ _ _ _ _ = _
      rw [h₁, h₂, map, eval₂Hom_C, RingHom.comp_apply, AlgHom.coe_toRingHom, AlgHom.commutes] }

Algebra homomorphism induced by coefficient mapping for multivariate polynomials

Informal description

Given a commutative semiring $ S_2 $ and $ R $-algebra structures on $ S_1 $ and $ S_2 $, the function `mapAlgHom f` is the $ R $-algebra homomorphism from the multivariate polynomial ring $ \text{MvPolynomial}(\sigma, S_1) $ to $ \text{MvPolynomial}(\sigma, S_2) $ induced by an $ R $-algebra homomorphism $ f: S_1 \to S_2 $. It applies $ f $ to each coefficient of the polynomial while preserving the variables and satisfies: \[ \text{mapAlgHom}\, f\, (1) = 1, \quad \text{mapAlgHom}\, f\, (p + q) = \text{mapAlgHom}\, f\, (p) + \text{mapAlgHom}\, f\, (q), \quad \text{mapAlgHom}\, f\, (p \cdot q) = \text{mapAlgHom}\, f\, (p) \cdot \text{mapAlgHom}\, f\, (q). \] Additionally, it commutes with the algebra map from $ R $, i.e., for any $ r \in R $, \[ \text{mapAlgHom}\, f\, (\text{algebraMap}\, R\, (\text{MvPolynomial}\, \sigma\, S_1)\, r) = \text{algebraMap}\, R\, (\text{MvPolynomial}\, \sigma\, S_2)\, r. \]

MvPolynomial.mapAlgHom_id theorem

[Algebra R S₁] : mapAlgHom (AlgHom.id R S₁) = AlgHom.id R (MvPolynomial σ S₁)

Full source

@[simp]
theorem mapAlgHom_id [Algebra R S₁] :
    mapAlgHom (AlgHom.id R S₁) = AlgHom.id R (MvPolynomial σ S₁) :=
  AlgHom.ext map_id

Identity Algebra Homomorphism Preserves Multivariate Polynomial Ring Structure

Informal description

For any commutative semiring $R$ and $R$-algebra $S_1$, the algebra homomorphism `mapAlgHom` applied to the identity algebra homomorphism $\text{id}_{R S_1} \colon S_1 \to S_1$ is equal to the identity algebra homomorphism on the multivariate polynomial ring $\text{MvPolynomial}(\sigma, S_1)$. That is, \[ \text{mapAlgHom}\, \text{id}_{R S_1} = \text{id}_{R (\text{MvPolynomial}\, \sigma\, S_1)}. \]

MvPolynomial.mapAlgHom_coe_ringHom theorem

 [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
  ↑(mapAlgHom f : _ →ₐ[R] MvPolynomial σ S₂) = (map ↑f : MvPolynomial σ S₁ →+* MvPolynomial σ S₂)

Full source

@[simp]
theorem mapAlgHom_coe_ringHom [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
    ↑(mapAlgHom f : _ →ₐ[R] MvPolynomial σ S₂) =
      (map ↑f : MvPolynomialMvPolynomial σ S₁ →+* MvPolynomial σ S₂) :=
  RingHom.mk_coe _ _ _ _ _

Equality of Coefficient Mapping as Algebra and Ring Homomorphisms for Multivariate Polynomials

Informal description

Let $R$, $S_1$, and $S_2$ be commutative semirings with $R$-algebra structures on $S_1$ and $S_2$. For any $R$-algebra homomorphism $f: S_1 \to S_2$, the underlying ring homomorphism of the algebra homomorphism $\text{mapAlgHom}\, f$ from $\text{MvPolynomial}(\sigma, S_1)$ to $\text{MvPolynomial}(\sigma, S_2)$ is equal to the ring homomorphism $\text{map}\, f$ obtained by applying $f$ to the coefficients of the polynomials. In symbols: \[ (\text{mapAlgHom}\, f : \text{MvPolynomial}(\sigma, S_1) \to \text{MvPolynomial}(\sigma, S_2)) = \text{map}\, f \]

MvPolynomial.algebraMap_apply theorem

(r : R) : algebraMap R (MvPolynomial σ S₁) r = C (algebraMap R S₁ r)

Full source

@[simp]
theorem algebraMap_apply (r : R) : algebraMap R (MvPolynomial σ S₁) r = C (algebraMap R S₁ r) := rfl

Algebra Map to Multivariate Polynomial Ring Preserves Constants

Informal description

For any element $r$ in a commutative semiring $R$, the algebra map from $R$ to the multivariate polynomial ring $MvPolynomial(\sigma, S₁)$ evaluated at $r$ is equal to the constant polynomial $C$ applied to the algebra map from $R$ to $S₁$ evaluated at $r$. In other words: $$\text{algebraMap}_{R \to MvPolynomial(\sigma, S₁)}(r) = C(\text{algebraMap}_{R \to S₁}(r))$$

MvPolynomial.aeval definition

: MvPolynomial σ R →ₐ[R] S₁

Full source

/-- A map `σ → S₁` where `S₁` is an algebra over `R` generates an `R`-algebra homomorphism
from multivariate polynomials over `σ` to `S₁`. -/
def aeval : MvPolynomialMvPolynomial σ R →ₐ[R] S₁ :=
  { eval₂Hom (algebraMap R S₁) f with commutes' := fun _r => eval₂_C _ _ _ }

Algebra evaluation of multivariate polynomials

Informal description

Given a commutative semiring $R$ and an $R$-algebra $S₁$, the function $\text{aeval}(f)$ is the $R$-algebra homomorphism from the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$ to $S₁$ induced by a map $f: \sigma \to S₁$. It evaluates a polynomial by substituting each variable $X_i$ with $f(i)$ and mapping the coefficients via the canonical algebra map $R \to S₁$. Specifically, it satisfies: \[ \text{aeval}(f)(1) = 1, \quad \text{aeval}(f)(p + q) = \text{aeval}(f)(p) + \text{aeval}(f)(q), \quad \text{aeval}(f)(p \cdot q) = \text{aeval}(f)(p) \cdot \text{aeval}(f)(q). \]

MvPolynomial.aeval_def theorem

(p : MvPolynomial σ R) : aeval f p = eval₂ (algebraMap R S₁) f p

Full source

theorem aeval_def (p : MvPolynomial σ R) : aeval f p = eval₂ (algebraMap R S₁) f p :=
  rfl

Algebra Evaluation Equals Evaluation via Canonical Map: $\text{aeval}(f)(p) = \text{eval}_2(\text{algebraMap}, f, p)$

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the algebra evaluation $\text{aeval}(f)(p)$ is equal to the evaluation $\text{eval}_2(\text{algebraMap}_{R \to S₁}, f, p)$, where $\text{algebraMap}_{R \to S₁}$ is the canonical algebra homomorphism from $R$ to $S₁$ and $f: \sigma \to S₁$ is the valuation map.

MvPolynomial.aeval_eq_eval₂Hom theorem

(p : MvPolynomial σ R) : aeval f p = eval₂Hom (algebraMap R S₁) f p

Full source

theorem aeval_eq_eval₂Hom (p : MvPolynomial σ R) : aeval f p = eval₂Hom (algebraMap R S₁) f p :=
  rfl

Equality of Algebra Evaluation and Evaluation Homomorphism for Multivariate Polynomials

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the algebra evaluation $\text{aeval}(f)(p)$ equals the evaluation homomorphism $\text{eval₂Hom}(\text{algebraMap}\,R\,S₁, f)(p)$, where $\text{algebraMap}\,R\,S₁$ is the canonical algebra map from $R$ to $S₁$ and $f: \sigma \to S₁$ is the valuation map.

MvPolynomial.coe_aeval_eq_eval theorem

: RingHomClass.toRingHom (MvPolynomial.aeval f) = MvPolynomial.eval f

Full source

@[simp]
lemma coe_aeval_eq_eval : RingHomClass.toRingHom (MvPolynomial.aeval f) = MvPolynomial.eval f :=
  rfl

Equality of Algebra Evaluation and Evaluation as Ring Homomorphisms

Informal description

For any commutative semiring $R$ and any $R$-algebra $S₁$, the ring homomorphism obtained from the algebra evaluation $\text{aeval}(f) : \text{MvPolynomial}(\sigma, R) \to S₁$ (when restricted to its ring homomorphism structure) is equal to the evaluation homomorphism $\text{eval}(f) : \text{MvPolynomial}(\sigma, R) \to R$.

MvPolynomial.aeval_X theorem

(s : σ) : aeval f (X s : MvPolynomial _ R) = f s

Full source

@[simp]
theorem aeval_X (s : σ) : aeval f (X s : MvPolynomial _ R) = f s :=
  eval₂_X _ _ _

Evaluation of Variable Monomial: $\text{aeval}(f)(X_s) = f(s)$

Informal description

For any variable $s \in \sigma$, the algebra evaluation of the monomial $X_s$ (the polynomial variable corresponding to $s$) under the map $f: \sigma \to S₁$ satisfies $\text{aeval}(f)(X_s) = f(s)$.

MvPolynomial.aeval_C theorem

(r : R) : aeval f (C r) = algebraMap R S₁ r

Full source

theorem aeval_C (r : R) : aeval f (C r) = algebraMap R S₁ r :=
  eval₂_C _ _ _

Algebra Evaluation of Constant Polynomials: $\text{aeval}(f)(C(r)) = \text{algebraMap}(r)$

Informal description

For any commutative semiring $R$, any $R$-algebra $S₁$, and any element $r \in R$, the algebra evaluation of the constant polynomial $C(r) \in \text{MvPolynomial}(\sigma, R)$ under the map $f: \sigma \to S₁$ is equal to the image of $r$ under the canonical algebra map from $R$ to $S₁$, i.e., \[ \text{aeval}(f)(C(r)) = \text{algebraMap}_{R \to S₁}(r). \]

MvPolynomial.aeval_ofNat theorem

(n : Nat) [n.AtLeastTwo] : aeval f (ofNat(n) : MvPolynomial σ R) = ofNat(n)

Full source

@[simp] theorem aeval_ofNat (n : Nat) [n.AtLeastTwo] :
    aeval f (ofNat(n) : MvPolynomial σ R) = ofNat(n) :=
  map_ofNat _ _

Preservation of Numerals ≥ 2 under Algebra Evaluation of Multivariate Polynomials

Informal description

For any natural number $n \geq 2$, the algebra evaluation of the multivariate polynomial $n$ (interpreted as a constant polynomial in $\text{MvPolynomial}(\sigma, R)$) under any evaluation map $f \colon \sigma \to S₁$ equals the canonical embedding of $n$ in $S₁$, i.e., \[ \text{aeval}(f)(n) = n. \]

MvPolynomial.aeval_unique theorem

(φ : MvPolynomial σ R →ₐ[R] S₁) : φ = aeval (φ ∘ X)

Full source

theorem aeval_unique (φ : MvPolynomialMvPolynomial σ R →ₐ[R] S₁) : φ = aeval (φ ∘ X) := by
  ext i
  simp

Uniqueness of Algebra Homomorphisms on Multivariate Polynomials via Variable Evaluation

Informal description

For any $R$-algebra homomorphism $\varphi \colon \text{MvPolynomial}(\sigma, R) \to S₁$, we have $\varphi = \text{aeval}(\varphi \circ X)$, where $X$ is the inclusion map of variables into the polynomial ring. In other words, $\varphi$ is uniquely determined by its values on the variables $X_s$ (for $s \in \sigma$).

MvPolynomial.aeval_X_left theorem

: aeval X = AlgHom.id R (MvPolynomial σ R)

Full source

theorem aeval_X_left : aeval X = AlgHom.id R (MvPolynomial σ R) :=
  (aeval_unique (AlgHom.id R _)).symm

Identity Property of Algebra Evaluation with Variable Inclusion: $\text{aeval}(X) = \text{id}$

Informal description

The algebra evaluation homomorphism $\text{aeval}(X)$, where $X$ is the inclusion map of variables into the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$, is equal to the identity algebra homomorphism on $\text{MvPolynomial}(\sigma, R)$. In other words, evaluating a polynomial by substituting each variable $X_i$ with itself yields the original polynomial.

MvPolynomial.aeval_X_left_apply theorem

(p : MvPolynomial σ R) : aeval X p = p

Full source

theorem aeval_X_left_apply (p : MvPolynomial σ R) : aeval X p = p :=
  AlgHom.congr_fun aeval_X_left p

Identity Evaluation of Multivariate Polynomials: $\text{aeval}(X)(p) = p$

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, evaluating $p$ by substituting each variable $X_i$ with itself yields $p$, i.e., $\text{aeval}(X)(p) = p$.

MvPolynomial.comp_aeval theorem

{B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) : φ.comp (aeval f) = aeval fun i => φ (f i)

Full source

theorem comp_aeval {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) :
    φ.comp (aeval f) = aeval fun i => φ (f i) := by
  ext i
  simp

Composition of Algebra Evaluation with Homomorphism: $\varphi \circ \text{aeval}(f) = \text{aeval}(\varphi \circ f)$

Informal description

Let $R$ be a commutative semiring, $S₁$ and $B$ be $R$-algebras, and $f : \sigma \to S₁$ be a map. For any $R$-algebra homomorphism $\varphi : S₁ \to B$, the composition $\varphi \circ \text{aeval}(f)$ equals the algebra evaluation $\text{aeval}(\varphi \circ f)$, where $\text{aeval}(f) : \text{MvPolynomial}(\sigma, R) \to S₁$ is the evaluation homomorphism induced by $f$.

MvPolynomial.comp_aeval_apply theorem

 {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) (p : MvPolynomial σ R) :
  φ (aeval f p) = aeval (fun i ↦ φ (f i)) p

Full source

lemma comp_aeval_apply {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B)
    (p : MvPolynomial σ R) :
    φ (aeval f p) = aeval (fun i ↦ φ (f i)) p := by
  rw [← comp_aeval, AlgHom.coe_comp, comp_apply]

Evaluation of Polynomials under Algebra Homomorphism: $\varphi(\text{aeval}(f)(p)) = \text{aeval}(\varphi \circ f)(p)$

Informal description

Let $R$ be a commutative semiring, $S₁$ and $B$ be $R$-algebras, and $f \colon \sigma \to S₁$ be a map. For any $R$-algebra homomorphism $\varphi \colon S₁ \to B$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, we have: \[ \varphi(\text{aeval}(f)(p)) = \text{aeval}(\varphi \circ f)(p), \] where $\text{aeval}(f) \colon \text{MvPolynomial}(\sigma, R) \to S₁$ is the algebra evaluation homomorphism induced by $f$.

MvPolynomial.map_aeval theorem

 {B : Type*} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
  φ (aeval g p) = eval₂Hom (φ.comp (algebraMap R S₁)) (fun i => φ (g i)) p

Full source

@[simp]
theorem map_aeval {B : Type*} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
    φ (aeval g p) = eval₂Hom (φ.comp (algebraMap R S₁)) (fun i => φ (g i)) p := by
  rw [← comp_eval₂Hom]
  rfl

Compatibility of Algebra Evaluation with Ring Homomorphism for Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, $S₁$ an $R$-algebra, and $B$ another commutative semiring. Given a valuation $g \colon \sigma \to S₁$ and a ring homomorphism $\varphi \colon S₁ \to B$, for any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, we have: \[ \varphi(\text{aeval}(g)(p)) = \text{eval₂Hom}(\varphi \circ \text{algebraMap}(R, S₁), \lambda i, \varphi(g(i)))(p), \] where $\text{aeval}(g)$ is the algebra evaluation homomorphism and $\text{eval₂Hom}$ is the evaluation homomorphism for multivariate polynomials.

MvPolynomial.eval₂Hom_zero theorem

(f : R →+* S₂) : eval₂Hom f (0 : σ → S₂) = f.comp constantCoeff

Full source

@[simp]
theorem eval₂Hom_zero (f : R →+* S₂) : eval₂Hom f (0 : σ → S₂) = f.comp constantCoeff := by
  ext <;> simp

Evaluation Homomorphism with Zero Valuation Equals Composition with Constant Coefficient

Informal description

Given a semiring homomorphism $f \colon R \to S_2$, the evaluation homomorphism $\text{eval₂Hom}(f, 0)$ (where $0$ denotes the zero valuation $\sigma \to S_2$) is equal to the composition of $f$ with the constant coefficient homomorphism $\text{constantCoeff} \colon \text{MvPolynomial}(\sigma, R) \to R$.

MvPolynomial.eval₂Hom_zero' theorem

(f : R →+* S₂) : eval₂Hom f (fun _ => 0 : σ → S₂) = f.comp constantCoeff

Full source

@[simp]
theorem eval₂Hom_zero' (f : R →+* S₂) : eval₂Hom f (fun _ => 0 : σ → S₂) = f.comp constantCoeff :=
  eval₂Hom_zero f

Evaluation Homomorphism with Constant Zero Valuation Equals Composition with Constant Coefficient

Informal description

Given a semiring homomorphism $f \colon R \to S_2$, the evaluation homomorphism $\text{eval₂Hom}(f, \lambda \_, 0)$ (where $\lambda \_, 0$ denotes the constant zero valuation $\sigma \to S_2$) is equal to the composition of $f$ with the constant coefficient homomorphism $\text{constantCoeff} \colon \text{MvPolynomial}(\sigma, R) \to R$.

MvPolynomial.eval₂Hom_zero_apply theorem

(f : R →+* S₂) (p : MvPolynomial σ R) : eval₂Hom f (0 : σ → S₂) p = f (constantCoeff p)

Full source

theorem eval₂Hom_zero_apply (f : R →+* S₂) (p : MvPolynomial σ R) :
    eval₂Hom f (0 : σ → S₂) p = f (constantCoeff p) :=
  RingHom.congr_fun (eval₂Hom_zero f) p

Evaluation at Zero Valuation Equals Constant Coefficient Applied by Homomorphism

Informal description

For any semiring homomorphism $f \colon R \to S_2$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, evaluating $p$ at the zero valuation (where all variables are mapped to $0 \in S_2$) via the homomorphism $f$ yields the same result as applying $f$ to the constant coefficient of $p$. That is: \[ \text{eval₂Hom}(f, 0)(p) = f(\text{constantCoeff}(p)). \]

MvPolynomial.eval₂Hom_zero'_apply theorem

(f : R →+* S₂) (p : MvPolynomial σ R) : eval₂Hom f (fun _ => 0 : σ → S₂) p = f (constantCoeff p)

Full source

theorem eval₂Hom_zero'_apply (f : R →+* S₂) (p : MvPolynomial σ R) :
    eval₂Hom f (fun _ => 0 : σ → S₂) p = f (constantCoeff p) :=
  eval₂Hom_zero_apply f p

Evaluation Homomorphism at Zero Valuation Equals Constant Coefficient Applied by Homomorphism

Informal description

For any semiring homomorphism $f \colon R \to S_2$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, evaluating $p$ at the zero valuation (where all variables are mapped to $0 \in S_2$) via the homomorphism $f$ yields the same result as applying $f$ to the constant coefficient of $p$. That is: \[ \text{eval₂Hom}(f, \lambda \_, 0)(p) = f(\text{constantCoeff}(p)). \]

MvPolynomial.eval₂_zero_apply theorem

(f : R →+* S₂) (p : MvPolynomial σ R) : eval₂ f (0 : σ → S₂) p = f (constantCoeff p)

Full source

@[simp]
theorem eval₂_zero_apply (f : R →+* S₂) (p : MvPolynomial σ R) :
    eval₂ f (0 : σ → S₂) p = f (constantCoeff p) :=
  eval₂Hom_zero_apply _ _

Evaluation of Multivariate Polynomial at Zero Valuation Equals Homomorphism Applied to Constant Coefficient

Informal description

For any semiring homomorphism $f \colon R \to S_2$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, evaluating $p$ at the zero valuation (where all variables are mapped to $0 \in S_2$) via the homomorphism $f$ yields the same result as applying $f$ to the constant coefficient of $p$. That is: \[ \text{eval}_2(f, 0)(p) = f(\text{constantCoeff}(p)). \]

MvPolynomial.eval₂_zero'_apply theorem

(f : R →+* S₂) (p : MvPolynomial σ R) : eval₂ f (fun _ => 0 : σ → S₂) p = f (constantCoeff p)

Full source

@[simp]
theorem eval₂_zero'_apply (f : R →+* S₂) (p : MvPolynomial σ R) :
    eval₂ f (fun _ => 0 : σ → S₂) p = f (constantCoeff p) :=
  eval₂_zero_apply f p

Evaluation at Zero Valuation Equals Homomorphism Applied to Constant Coefficient

Informal description

For any semiring homomorphism $f \colon R \to S_2$ and any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, evaluating $p$ at the zero valuation (where all variables are mapped to $0 \in S_2$) via the homomorphism $f$ yields the same result as applying $f$ to the constant coefficient of $p$. That is: \[ \text{eval}_2(f, \lambda \_, 0)(p) = f(\text{constantCoeff}(p)). \]

MvPolynomial.aeval_zero theorem

(p : MvPolynomial σ R) : aeval (0 : σ → S₁) p = algebraMap _ _ (constantCoeff p)

Full source

@[simp]
theorem aeval_zero (p : MvPolynomial σ R) :
    aeval (0 : σ → S₁) p = algebraMap _ _ (constantCoeff p) :=
  eval₂Hom_zero_apply (algebraMap R S₁) p

Algebra Evaluation at Zero Valuation Equals Constant Coefficient Image

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the algebra evaluation of $p$ at the zero valuation (where all variables are mapped to $0 \in S₁$) is equal to the image of the constant coefficient of $p$ under the canonical algebra map $R \to S₁$. That is: \[ \text{aeval}(0)(p) = \text{algebraMap}(R, S₁)(\text{constantCoeff}(p)). \]

MvPolynomial.aeval_zero' theorem

(p : MvPolynomial σ R) : aeval (fun _ => 0 : σ → S₁) p = algebraMap _ _ (constantCoeff p)

Full source

@[simp]
theorem aeval_zero' (p : MvPolynomial σ R) :
    aeval (fun _ => 0 : σ → S₁) p = algebraMap _ _ (constantCoeff p) :=
  aeval_zero p

Algebra Evaluation at Zero Valuation Yields Constant Coefficient Image

Informal description

For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the algebra evaluation of $p$ at the zero valuation (where all variables are mapped to $0 \in S₁$) is equal to the image of the constant coefficient of $p$ under the canonical algebra map $R \to S₁$. That is: \[ \text{aeval}(0)(p) = \text{algebraMap}(R, S₁)(\text{constantCoeff}(p)). \]

MvPolynomial.eval_zero theorem

: eval (0 : σ → R) = constantCoeff

Full source

@[simp]
theorem eval_zero : eval (0 : σ → R) = constantCoeff :=
  eval₂Hom_zero _

Evaluation at Zero Equals Constant Coefficient

Informal description

The evaluation of a multivariate polynomial in the ring $\text{MvPolynomial}(\sigma, R)$ at the zero valuation (where all variables are mapped to $0 \in R$) is equal to the constant coefficient of the polynomial. In other words, the evaluation homomorphism $\text{eval}(0)$ coincides with the constant coefficient homomorphism $\text{constantCoeff}$.

MvPolynomial.eval_zero' theorem

: eval (fun _ => 0 : σ → R) = constantCoeff

Full source

@[simp]
theorem eval_zero' : eval (fun _ => 0 : σ → R) = constantCoeff :=
  eval₂Hom_zero _

Evaluation at Zero Valuation Equals Constant Coefficient

Informal description

The evaluation of a multivariate polynomial in $\text{MvPolynomial}(\sigma, R)$ at the zero valuation (where all variables are mapped to $0 \in R$) is equal to the constant coefficient homomorphism $\text{constantCoeff}$. That is, for any polynomial $p \in \text{MvPolynomial}(\sigma, R)$, we have: \[ \text{eval}(0)(p) = \text{constantCoeff}(p). \]

MvPolynomial.aeval_monomial theorem

(g : σ → S₁) (d : σ →₀ ℕ) (r : R) : aeval g (monomial d r) = algebraMap _ _ r * d.prod fun i k => g i ^ k

Full source

theorem aeval_monomial (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
    aeval g (monomial d r) = algebraMap _ _ r * d.prod fun i k => g i ^ k :=
  eval₂Hom_monomial _ _ _ _

Algebra Evaluation of Monomial: $\text{aeval}(g)(X^d \cdot r) = \varphi(r) \cdot \prod_i g(i)^{d(i)}$

Informal description

Let $R$ be a commutative semiring and $S₁$ an $R$-algebra. Given a map $g \colon \sigma \to S₁$, an exponent vector $d \colon \sigma \to₀ \mathbb{N}$ with finite support, and a coefficient $r \in R$, the algebra evaluation of the monomial $X^d \cdot r$ satisfies: \[ \text{aeval}(g)(X^d \cdot r) = \varphi(r) \cdot \prod_{i \in \sigma} (g(i))^{d(i)} \] where $\varphi \colon R \to S₁$ is the canonical algebra map and the product is taken over the finite support of $d$.

MvPolynomial.eval₂Hom_eq_zero theorem

 (f : R →+* S₂) (g : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ d, φ.coeff d ≠ 0 → ∃ i ∈ d.support, g i = 0) :
  eval₂Hom f g φ = 0

Full source

theorem eval₂Hom_eq_zero (f : R →+* S₂) (g : σ → S₂) (φ : MvPolynomial σ R)
    (h : ∀ d, φ.coeff d ≠ 0 → ∃ i ∈ d.support, g i = 0) : eval₂Hom f g φ = 0 := by
  rw [φ.as_sum, map_sum]
  refine Finset.sum_eq_zero fun d hd => ?_
  obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (Finsupp.mem_support_iff.mp hd)
  rw [eval₂Hom_monomial, Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
  rw [hgi, zero_pow]
  rwa [← Finsupp.mem_support_iff]

Vanishing of Polynomial Evaluation under Zero Valuation Condition

Informal description

Let $R$ and $S₂$ be commutative semirings, $f \colon R \to S₂$ a semiring homomorphism, and $g \colon \sigma \to S₂$ a valuation. For any multivariate polynomial $\varphi \in \text{MvPolynomial}(\sigma, R)$, if for every nonzero coefficient $r_d$ of $\varphi$ (i.e., $\text{coeff}(d, \varphi) \neq 0$) there exists an index $i$ in the support of $d$ such that $g(i) = 0$, then the evaluation homomorphism satisfies $\text{eval₂Hom}(f, g)(\varphi) = 0$.

MvPolynomial.aeval_eq_zero theorem

 [Algebra R S₂] (f : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ d, φ.coeff d ≠ 0 → ∃ i ∈ d.support, f i = 0) : aeval f φ = 0

Full source

theorem aeval_eq_zero [Algebra R S₂] (f : σ → S₂) (φ : MvPolynomial σ R)
    (h : ∀ d, φ.coeff d ≠ 0 → ∃ i ∈ d.support, f i = 0) : aeval f φ = 0 :=
  eval₂Hom_eq_zero _ _ _ h

Vanishing of Algebra Evaluation under Zero Variable Condition

Informal description

Let $R$ be a commutative semiring, $S₂$ an $R$-algebra, and $\sigma$ a type indexing variables. Given a map $f \colon \sigma \to S₂$ and a multivariate polynomial $\varphi \in \text{MvPolynomial}(\sigma, R)$, if for every nonzero coefficient $r_d$ of $\varphi$ there exists an index $i$ in the support of $d$ such that $f(i) = 0$, then the algebra evaluation $\text{aeval}(f)(\varphi) = 0$.

MvPolynomial.aeval_sum theorem

 {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) : aeval f (∑ i ∈ s, φ i) = ∑ i ∈ s, aeval f (φ i)

Full source

theorem aeval_sum {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) :
    aeval f (∑ i ∈ s, φ i) = ∑ i ∈ s, aeval f (φ i) :=
  map_sum (MvPolynomial.aeval f) _ _

Linearity of Algebra Evaluation over Finite Sums of Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type indexing the variables, and $S₁$ an $R$-algebra. Given a map $f \colon \sigma \to S₁$ and a finite set $s$ of indices of type $\iota$, for any family of multivariate polynomials $\varphi \colon \iota \to \text{MvPolynomial}(\sigma, R)$, the algebra evaluation of the sum of the polynomials $\varphi_i$ over $s$ is equal to the sum of the algebra evaluations of each $\varphi_i$ over $s$. That is, \[ \text{aeval}(f)\left(\sum_{i \in s} \varphi_i\right) = \sum_{i \in s} \text{aeval}(f)(\varphi_i). \]

MvPolynomial.aeval_prod theorem

 {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) : aeval f (∏ i ∈ s, φ i) = ∏ i ∈ s, aeval f (φ i)

Full source

@[to_additive existing]
theorem aeval_prod {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) :
    aeval f (∏ i ∈ s, φ i) = ∏ i ∈ s, aeval f (φ i) :=
  map_prod (MvPolynomial.aeval f) _ _

Product Evaluation of Multivariate Polynomials via Algebra Homomorphism

Informal description

Let $R$ be a commutative semiring, $S₁$ an $R$-algebra, and $\sigma$ a type indexing the variables. For any finite set $s$ of indices of type $\iota$ and any family of multivariate polynomials $\varphi : \iota \to \text{MvPolynomial}(\sigma, R)$, the algebra evaluation of the product of the polynomials $\prod_{i \in s} \varphi(i)$ under a map $f : \sigma \to S₁$ is equal to the product of the evaluations: $\prod_{i \in s} \text{aeval}(f)(\varphi(i))$.

Algebra.adjoin_range_eq_range_aeval theorem

: Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range

Full source

theorem _root_.Algebra.adjoin_range_eq_range_aeval :
    Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range := by
  simp only [← Algebra.map_top, ← MvPolynomial.adjoin_range_X, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, MvPolynomial.aeval_X]

Range of Algebra Evaluation Equals Adjoint of Variable Map Range

Informal description

Let $R$ be a commutative semiring and $S₁$ an $R$-algebra. For any map $f \colon \sigma \to S₁$, the algebra generated by the range of $f$ over $R$ is equal to the range of the algebra evaluation homomorphism $\text{aeval}(f) \colon \text{MvPolynomial}(\sigma, R) \to S₁$. That is, \[ \text{Algebra.adjoin}_R (\text{range}(f)) = \text{range}(\text{aeval}(f)). \]

Algebra.adjoin_eq_range theorem

(s : Set S₁) : Algebra.adjoin R s = (MvPolynomial.aeval ((↑) : s → S₁)).range

Full source

theorem _root_.Algebra.adjoin_eq_range (s : Set S₁) :
    Algebra.adjoin R s = (MvPolynomial.aeval ((↑) : s → S₁)).range := by
  rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]

Algebra Adjoint Equals Range of Evaluation Homomorphism for Subset Inclusion

Informal description

Let $R$ be a commutative semiring and $S₁$ an $R$-algebra. For any subset $s$ of $S₁$, the algebra generated by $s$ over $R$ is equal to the range of the algebra evaluation homomorphism $\text{aeval}(\uparrow) \colon \text{MvPolynomial}(s, R) \to S₁$, where $\uparrow \colon s \to S₁$ is the canonical inclusion map. That is, \[ \text{Algebra.adjoin}_R(s) = \text{range}(\text{aeval}(\uparrow)). \]

MvPolynomial.aevalTower definition

(f : R →ₐ[S] A) (X : σ → A) : MvPolynomial σ R →ₐ[S] A

Full source

/-- Version of `aeval` for defining algebra homs out of `MvPolynomial σ R` over a smaller base ring
  than `R`. -/
def aevalTower (f : R →ₐ[S] A) (X : σ → A) : MvPolynomialMvPolynomial σ R →ₐ[S] A :=
  { eval₂Hom (↑f) X with
    commutes' := fun r => by
      simp [IsScalarTower.algebraMap_eq S R (MvPolynomial σ R), algebraMap_eq] }

Tower algebra homomorphism for multivariate polynomial evaluation

Informal description

Given an algebra homomorphism $ f: R \to A $ over a base semiring $ S $ and a valuation $ X: \sigma \to A $, the function $ \text{aevalTower}(f, X) $ is the algebra homomorphism from the multivariate polynomial ring $ \text{MvPolynomial}(\sigma, R) $ to $ A $ over $ S $, defined by evaluating each polynomial at $ X $ after applying $ f $ to its coefficients. Specifically, it satisfies: \[ \text{aevalTower}(f, X)(1) = 1, \quad \text{aevalTower}(f, X)(p + q) = \text{aevalTower}(f, X)(p) + \text{aevalTower}(f, X)(q), \quad \text{aevalTower}(f, X)(p \cdot q) = \text{aevalTower}(f, X)(p) \cdot \text{aevalTower}(f, X)(q), \] and it commutes with the algebra structure over $ S $.

MvPolynomial.aevalTower_X theorem

(i : σ) : aevalTower g y (X i) = y i

Full source

@[simp]
theorem aevalTower_X (i : σ) : aevalTower g y (X i) = y i :=
  eval₂_X _ _ _

Evaluation of Variable Polynomial via Tower Homomorphism: $\text{aevalTower}(g, y)(X_i) = y(i)$

Informal description

Given an algebra homomorphism $g \colon R \to A$ over a base semiring $S$ and a valuation $y \colon \sigma \to A$, the evaluation of the monomial $X_i$ (the polynomial variable corresponding to index $i \in \sigma$) via $\text{aevalTower}(g, y)$ satisfies $\text{aevalTower}(g, y)(X_i) = y(i)$.

MvPolynomial.aevalTower_C theorem

(x : R) : aevalTower g y (C x) = g x

Full source

@[simp]
theorem aevalTower_C (x : R) : aevalTower g y (C x) = g x :=
  eval₂_C _ _ _

Evaluation of Constant Polynomial via Tower Algebra Homomorphism

Informal description

For any element $x \in R$, the evaluation of the constant polynomial $C(x) \in \text{MvPolynomial}(\sigma, R)$ under the tower algebra homomorphism $\text{aevalTower}(g, y)$ is equal to $g(x)$, i.e., \[ \text{aevalTower}(g, y)(C(x)) = g(x). \]

MvPolynomial.aevalTower_ofNat theorem

(n : Nat) [n.AtLeastTwo] : aevalTower g y (ofNat(n) : MvPolynomial σ R) = ofNat(n)

Full source

@[simp]
theorem aevalTower_ofNat (n : Nat) [n.AtLeastTwo] :
    aevalTower g y (ofNat(n) : MvPolynomial σ R) = ofNat(n) :=
  _root_.map_ofNat _ _

Evaluation of Constant Polynomials via Tower Algebra Homomorphism Preserves Numerals $\geq 2$

Informal description

Let $R$ be a commutative semiring, $S$ a semiring, and $A$ an $S$-algebra. Given an $S$-algebra homomorphism $g \colon R \to A$ and a map $y \colon \sigma \to A$, for any natural number $n \geq 2$, the evaluation of the constant polynomial $n$ under the tower algebra homomorphism $\text{aevalTower}(g, y)$ equals the constant $n$ in $A$, i.e., \[ \text{aevalTower}(g, y)(n) = n. \]

MvPolynomial.aevalTower_comp_C theorem

: (aevalTower g y : MvPolynomial σ R →+* A).comp C = g

Full source

@[simp]
theorem aevalTower_comp_C : (aevalTower g y : MvPolynomialMvPolynomial σ R →+* A).comp C = g :=
  RingHom.ext <| aevalTower_C _ _

Composition of Tower Evaluation with Constant Embedding Equals Algebra Homomorphism

Informal description

The composition of the ring homomorphism $\text{aevalTower}(g, y) \colon \text{MvPolynomial}(\sigma, R) \to A$ with the constant polynomial embedding $C \colon R \to \text{MvPolynomial}(\sigma, R)$ equals the algebra homomorphism $g \colon R \to A$. In other words, for any $x \in R$, we have: \[ \text{aevalTower}(g, y)(C(x)) = g(x). \]

MvPolynomial.aevalTower_algebraMap theorem

(x : R) : aevalTower g y (algebraMap R (MvPolynomial σ R) x) = g x

Full source

theorem aevalTower_algebraMap (x : R) : aevalTower g y (algebraMap R (MvPolynomial σ R) x) = g x :=
  eval₂_C _ _ _

Evaluation of Algebra Map in Multivariate Polynomial Tower

Informal description

Let $R$ be a commutative semiring, $S$ a base semiring, and $A$ an $S$-algebra. Given an $S$-algebra homomorphism $g: R \to A$ and a valuation $y: \sigma \to A$, the evaluation of the algebra map $\text{algebraMap}_R: R \to \text{MvPolynomial}(\sigma, R)$ at $x \in R$ satisfies: \[ \text{aevalTower}(g, y)(\text{algebraMap}_R(x)) = g(x). \]

MvPolynomial.aevalTower_comp_algebraMap theorem

: (aevalTower g y : MvPolynomial σ R →+* A).comp (algebraMap R (MvPolynomial σ R)) = g

Full source

theorem aevalTower_comp_algebraMap :
    (aevalTower g y : MvPolynomialMvPolynomial σ R →+* A).comp (algebraMap R (MvPolynomial σ R)) = g :=
  aevalTower_comp_C _ _

Composition of Tower Evaluation with Algebra Map Equals Algebra Homomorphism

Informal description

Let $R$ be a commutative semiring, $S$ a base semiring, and $A$ an $S$-algebra. Given an $S$-algebra homomorphism $g: R \to A$ and a valuation $y: \sigma \to A$, the composition of the ring homomorphism $\text{aevalTower}(g, y) \colon \text{MvPolynomial}(\sigma, R) \to A$ with the algebra map $\text{algebraMap}_R \colon R \to \text{MvPolynomial}(\sigma, R)$ equals $g$. In other words, for any $x \in R$, we have: \[ \text{aevalTower}(g, y)(\text{algebraMap}_R(x)) = g(x). \]

MvPolynomial.aevalTower_toAlgHom theorem

(x : R) : aevalTower g y (IsScalarTower.toAlgHom S R (MvPolynomial σ R) x) = g x

Full source

theorem aevalTower_toAlgHom (x : R) :
    aevalTower g y (IsScalarTower.toAlgHom S R (MvPolynomial σ R) x) = g x :=
  aevalTower_algebraMap _ _ _

Evaluation of Scalar Tower Algebra Homomorphism in Multivariate Polynomial Tower

Informal description

Let $R$ be a commutative semiring, $S$ a base semiring, and $A$ an $S$-algebra. Given an $S$-algebra homomorphism $g: R \to A$ and a valuation $y: \sigma \to A$, the evaluation of the algebra homomorphism $\text{IsScalarTower.toAlgHom}_{S,R}(\text{MvPolynomial}(\sigma, R))$ at $x \in R$ satisfies: \[ \text{aevalTower}(g, y)(\text{IsScalarTower.toAlgHom}_{S,R}(\text{MvPolynomial}(\sigma, R))(x)) = g(x). \]

MvPolynomial.aevalTower_comp_toAlgHom theorem

: (aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g

Full source

@[simp]
theorem aevalTower_comp_toAlgHom :
    (aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g :=
  AlgHom.coe_ringHom_injective <| aevalTower_comp_algebraMap _ _

Composition of Tower Evaluation with Scalar Tower Homomorphism Equals Algebra Homomorphism

Informal description

Let $R$ be a commutative semiring, $S$ a base semiring, and $A$ an $S$-algebra. Given an $S$-algebra homomorphism $g: R \to A$ and a valuation $y: \sigma \to A$, the composition of the algebra homomorphism $\text{aevalTower}(g, y) \colon \text{MvPolynomial}(\sigma, R) \to A$ with the scalar tower algebra homomorphism $\text{IsScalarTower.toAlgHom}_{S,R}(\text{MvPolynomial}(\sigma, R))$ equals $g$. In other words, for any $x \in R$, we have: \[ \text{aevalTower}(g, y)(\text{IsScalarTower.toAlgHom}_{S,R}(\text{MvPolynomial}(\sigma, R))(x)) = g(x). \]

MvPolynomial.aevalTower_id theorem

: aevalTower (AlgHom.id S S) = (aeval : (σ → S) → MvPolynomial σ S →ₐ[S] S)

Full source

@[simp]
theorem aevalTower_id :
    aevalTower (AlgHom.id S S) = (aeval : (σ → S) → MvPolynomialMvPolynomial σ S →ₐ[S] S) := by
  ext
  simp only [aevalTower_X, aeval_X]

Tower Evaluation with Identity Homomorphism Equals Standard Evaluation

Informal description

The tower evaluation homomorphism $\text{aevalTower}$ with the identity algebra homomorphism $\text{AlgHom.id}$ from $S$ to $S$ is equal to the standard algebra evaluation map $\text{aeval}$ from the multivariate polynomial ring $\text{MvPolynomial}(\sigma, S)$ to $S$ over $S$.

MvPolynomial.aevalTower_ofId theorem

: aevalTower (Algebra.ofId S A) = (aeval : (σ → A) → MvPolynomial σ S →ₐ[S] A)

Full source

@[simp]
theorem aevalTower_ofId :
    aevalTower (Algebra.ofId S A) = (aeval : (σ → A) → MvPolynomialMvPolynomial σ S →ₐ[S] A) := by
  ext
  simp only [aeval_X, aevalTower_X]

Tower Evaluation Equals Algebra Evaluation under Identity Homomorphism

Informal description

The tower algebra homomorphism $\text{aevalTower}$ with the identity algebra homomorphism $\text{Algebra.ofId}\,S\,A$ is equal to the algebra evaluation homomorphism $\text{aeval}$ from $(\sigma \to A)$ to $\text{MvPolynomial}\,\sigma\,S \to_{\text{Alg}[S]} A$.

MvPolynomial.eval₂_mem theorem

 {f : R →+* S} {p : MvPolynomial σ R} {s : subS} (hs : ∀ i ∈ p.support, f (p.coeff i) ∈ s) {v : σ → S}
  (hv : ∀ i, v i ∈ s) : MvPolynomial.eval₂ f v p ∈ s

Full source

theorem eval₂_mem {f : R →+* S} {p : MvPolynomial σ R} {s : subS}
    (hs : ∀ i ∈ p.support, f (p.coeff i) ∈ s) {v : σ → S} (hv : ∀ i, v i ∈ s) :
    MvPolynomial.eval₂MvPolynomial.eval₂ f v p ∈ s := by
  classical
  replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.not_mem_support_iff.1 hi, f.map_zero]
      exact zero_mem s
  induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · have := hs a -- Porting note: was `simpa only [...]`
      rwa [coeff_add, MvPolynomial.not_mem_support_iff.1 ha, add_zero, coeff_monomial,
        if_pos rfl] at this
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.not_mem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this

Closure of Polynomial Evaluation in Subsemiring under Compatible Conditions

Informal description

Let $R$ and $S$ be commutative semirings, $\sigma$ be a type indexing variables, and $p \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. Given: - A semiring homomorphism $f: R \to S$ - A subset $s \subseteq S$ that is closed under the operations of $S$ - For each monomial $i$ in the support of $p$, the image $f(p_i)$ of its coefficient belongs to $s$ - A valuation $v: \sigma \to S$ such that $v(i) \in s$ for all $i \in \sigma$ Then the evaluation $\text{eval}_2(f, v, p)$ belongs to $s$.

MvPolynomial.eval_mem theorem

 {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ p.support, p.coeff i ∈ s) {v : σ → S} (hv : ∀ i, v i ∈ s) :
  MvPolynomial.eval v p ∈ s

Full source

theorem eval_mem {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ p.support, p.coeff i ∈ s) {v : σ → S}
    (hv : ∀ i, v i ∈ s) : MvPolynomial.evalMvPolynomial.eval v p ∈ s :=
  eval₂_mem hs hv

Closure of Polynomial Evaluation in Subsemiring under Coefficient and Variable Conditions

Informal description

Let $S$ be a commutative semiring, $\sigma$ a type indexing variables, and $p \in \text{MvPolynomial}(\sigma, S)$ a multivariate polynomial. Given: - A subset $s \subseteq S$ that is closed under the operations of $S$ - For each monomial $i$ in the support of $p$, its coefficient $p_i$ belongs to $s$ - A valuation $v: \sigma \to S$ such that $v(i) \in s$ for all $i \in \sigma$ Then the evaluation $\text{eval}(v, p)$ belongs to $s$.

MvPolynomial.aeval_sumElim theorem

 {σ τ : Type*} (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)

Full source

lemma aeval_sumElim {σ τ : Type*} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
    (aeval (Sum.elim g (algebraMapalgebraMap S T ∘ f))) p =
      (aeval g) ((aeval (Sum.elim X (CC ∘ f))) p) := by
  induction p using MvPolynomial.induction_on with
  | C r => simp [← IsScalarTower.algebraMap_apply]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i h => cases i <;> simp [h]

Evaluation of Multivariate Polynomials over Sum Types via Algebra Maps

Informal description

Let $R$, $S$, and $T$ be commutative semirings, with $S$ being an $R$-algebra and $T$ being an $S$-algebra. Let $\sigma$ and $\tau$ be types indexing variables, and let $p \in \text{MvPolynomial}(\sigma \oplus \tau, R)$ be a multivariate polynomial. Given maps $f \colon \tau \to S$ and $g \colon \sigma \to T$, the following equality holds: \[ \text{aeval}\big(\text{Sum.elim}\, g\, (\text{algebraMap}\, S\, T \circ f)\big)(p) = \text{aeval}(g)\big(\text{aeval}(\text{Sum.elim}\, X\, (C \circ f))(p)\big), \] where: - $\text{Sum.elim}\, g\, (\text{algebraMap}\, S\, T \circ f) \colon \sigma \oplus \tau \to T$ combines $g$ and the composition of $f$ with the algebra map from $S$ to $T$, - $X$ denotes the variable map $\sigma \to \text{MvPolynomial}(\sigma, R)$, - $C$ is the constant polynomial embedding $R \to \text{MvPolynomial}(\sigma, R)$.

MvPolynomial.algebraMvPolynomial definition

: Algebra (MvPolynomial σ R) (MvPolynomial σ S)

Full source

/--
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.
-/
noncomputable def algebraMvPolynomial : Algebra (MvPolynomial σ R) (MvPolynomial σ S) :=
  (MvPolynomial.map (algebraMap R S)).toAlgebra

Algebra structure on multivariate polynomials via coefficient mapping

Informal description

Given a commutative semiring $R$ and an $R$-algebra $S$, the multivariate polynomial ring $\text{MvPolynomial}(\sigma, S)$ is naturally an algebra over $\text{MvPolynomial}(\sigma, R)$. The algebra structure is induced by the coefficient-wise algebra homomorphism $\text{algebraMap}\, R\, S : R \to S$, extended to polynomials via the map operation.

MvPolynomial.algebraMap_def theorem

: algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = MvPolynomial.map (algebraMap R S)

Full source

@[simp]
lemma algebraMap_def :
    algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = MvPolynomial.map (algebraMap R S) :=
  rfl

Algebra Map Equals Coefficient Mapping for Multivariate Polynomials

Informal description

The algebra map from the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$ to $\text{MvPolynomial}(\sigma, S)$ is equal to the polynomial map induced by the algebra map from $R$ to $S$. That is, the following diagram commutes: \[ \text{algebraMap}\, (MvPolynomial\,\sigma\,R)\, (MvPolynomial\,\sigma\,S) = \text{map}\, (\text{algebraMap}\, R\, S) \]

MvPolynomial.instIsScalarTower instance

: IsScalarTower R (MvPolynomial σ R) (MvPolynomial σ S)

Full source

instance : IsScalarTower R (MvPolynomial σ R) (MvPolynomial σ S) :=
  IsScalarTower.of_algebraMap_eq' (by ext; simp)

Scalar Multiplication Tower Property for Multivariate Polynomials

Informal description

For any commutative semiring $R$ and $R$-algebra $S$, the scalar multiplication operations on the multivariate polynomial rings $\text{MvPolynomial}(\sigma, R)$ and $\text{MvPolynomial}(\sigma, S)$ satisfy the tower property. That is, for any $r \in R$, $p \in \text{MvPolynomial}(\sigma, R)$, and $q \in \text{MvPolynomial}(\sigma, S)$, we have $(r \cdot p) \cdot q = r \cdot (p \cdot q)$, where $\cdot$ denotes the respective scalar multiplication operations.

MvPolynomial.instFaithfulSMul instance

[FaithfulSMul R S] : FaithfulSMul (MvPolynomial σ R) (MvPolynomial σ S)

Full source

instance [FaithfulSMul R S] : FaithfulSMul (MvPolynomial σ R) (MvPolynomial σ S) :=
  (faithfulSMul_iff_algebraMap_injective ..).mpr
    (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

Faithful Scalar Multiplication for Multivariate Polynomials

Informal description

For any commutative semiring $R$ and $R$-algebra $S$, if the scalar multiplication action of $R$ on $S$ is faithful, then the scalar multiplication action of the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$ on $\text{MvPolynomial}(\sigma, S)$ is also faithful.

Mathlib.Algebra.MvPolynomial.Eval

Notation

Definitions