Mathlib.Algebra.Polynomial.AlgebraMap

Polynomial.algebraOfAlgebra instance

: Algebra R A[X]

Full source

/-- Note that this instance also provides `Algebra R R[X]`. -/
instance algebraOfAlgebra : Algebra R A[X] where
  smul_def' r p :=
    toFinsupp_injective <| by
      dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
      rw [toFinsupp_smul, toFinsupp_mul, toFinsupp_C]
      exact Algebra.smul_def' _ _
  commutes' r p :=
    toFinsupp_injective <| by
      dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
      simp_rw [toFinsupp_mul, toFinsupp_C]
      convert Algebra.commutes' r p.toFinsupp
  algebraMap := C.comp (algebraMap R A)

Polynomial Ring as Algebra Over Base Ring

Informal description

For any commutative semiring $R$ and any $R$-algebra $A$, the polynomial ring $A[X]$ is naturally an $R$-algebra. This includes the special case where $A = R$, making $R[X]$ an $R$-algebra via the constant polynomial embedding.

Polynomial.algebraMap_apply theorem

(r : R) : algebraMap R A[X] r = C (algebraMap R A r)

Full source

@[simp]
theorem algebraMap_apply (r : R) : algebraMap R A[X] r = C (algebraMap R A r) :=
  rfl

Algebra Map to Polynomial Ring Yields Constant Polynomial

Informal description

For any commutative semiring $R$ and any $R$-algebra $A$, the algebra map from $R$ to the polynomial ring $A[X]$ sends an element $r \in R$ to the constant polynomial $C(\text{algebraMap}_R^A(r))$ in $A[X]$, where $\text{algebraMap}_R^A$ is the algebra structure map from $R$ to $A$.

Polynomial.toFinsupp_algebraMap theorem

(r : R) : (algebraMap R A[X] r).toFinsupp = algebraMap R _ r

Full source

@[simp]
theorem toFinsupp_algebraMap (r : R) : (algebraMap R A[X] r).toFinsupp = algebraMap R _ r :=
  show toFinsupp (C (algebraMap _ _ r)) = _ by
    rw [toFinsupp_C]
    rfl

Compatibility of Algebra Maps with Polynomial Representation: $(\text{algebraMap}(r)).\text{toFinsupp} = \text{algebraMap}(r)$

Informal description

For any element $r$ in a commutative semiring $R$, the image of the algebra map $\text{algebraMap} \colon R \to A[X]$ evaluated at $r$ under the `toFinsupp` map is equal to the algebra map $\text{algebraMap} \colon R \to \text{AddMonoidAlgebra} \ A \ \mathbb{N}$ evaluated at $r$. In other words, the formal representation of the constant polynomial $\text{algebraMap}(r) \in A[X]$ as a finitely supported function in the additive monoid algebra is identical to the image of $r$ under the algebra map to $\text{AddMonoidAlgebra} \ A \ \mathbb{N}$.

Polynomial.ofFinsupp_algebraMap theorem

(r : R) : (⟨algebraMap R _ r⟩ : A[X]) = algebraMap R A[X] r

Full source

theorem ofFinsupp_algebraMap (r : R) : (⟨algebraMap R _ r⟩ : A[X]) = algebraMap R A[X] r :=
  toFinsupp_injective (toFinsupp_algebraMap _).symm

Equality of Polynomial Construction and Algebra Map: $\langle \text{algebraMap}(r) \rangle = \text{algebraMap}(r)$

Informal description

For any element $r$ in a commutative semiring $R$, the polynomial constructed from the image of $r$ under the algebra map to the additive monoid algebra $A[\mathbb{N}]$ is equal to the image of $r$ under the algebra map to the polynomial ring $A[X]$. In other words, the polynomial $\langle \text{algebraMap}_R^{A[\mathbb{N}]}(r) \rangle \in A[X]$ coincides with $\text{algebraMap}_R^{A[X]}(r)$.

Polynomial.C_eq_algebraMap theorem

(r : R) : C r = algebraMap R R[X] r

Full source

/-- When we have `[CommSemiring R]`, the function `C` is the same as `algebraMap R R[X]`.

(But note that `C` is defined when `R` is not necessarily commutative, in which case
`algebraMap` is not available.)
-/
theorem C_eq_algebraMap (r : R) : C r = algebraMap R R[X] r :=
  rfl

Equality of Constant Polynomial and Algebra Map in $R[X]$

Informal description

For any element $r$ in a commutative semiring $R$, the constant polynomial $C(r)$ is equal to the algebra map of $r$ into the polynomial ring $R[X]$, i.e., $C(r) = \text{algebraMap}_{R}(r)$.

Polynomial.algebraMap_eq theorem

: algebraMap R R[X] = C

Full source

@[simp]
theorem algebraMap_eq : algebraMap R R[X] = C :=
  rfl

Algebra Map Equals Constant Embedding for Polynomial Ring

Informal description

The algebra map from a commutative semiring $R$ to the polynomial ring $R[X]$ is equal to the constant polynomial embedding $C : R \to R[X]$. That is, $\text{algebraMap}_R R[X] = C$.

Polynomial.CAlgHom definition

: A →ₐ[R] A[X]

Full source

/-- `Polynomial.C` as an `AlgHom`. -/
@[simps! apply]
def CAlgHom : A →ₐ[R] A[X] where
  toRingHom := C
  commutes' _ := rfl

Constant embedding algebra homomorphism into polynomial ring

Informal description

The algebra homomorphism that embeds an element $a$ of an $R$-algebra $A$ into the polynomial ring $A[X]$ as a constant polynomial. This map preserves both the ring structure and the $R$-algebra structure, meaning: 1. It's a ring homomorphism ($C(a + b) = C(a) + C(b)$, $C(a \cdot b) = C(a) \cdot C(b)$, $C(1) = 1$) 2. It commutes with scalar multiplication by elements of $R$ ($C(r \cdot a) = r \cdot C(a)$ for $r \in R$)

Polynomial.algHom_ext' theorem

{f g : A[X] →ₐ[R] B} (hC : f.comp CAlgHom = g.comp CAlgHom) (hX : f X = g X) : f = g

Full source

/-- Extensionality lemma for algebra maps out of `A'[X]` over a smaller base ring than `A'`
-/
@[ext 1100]
theorem algHom_ext' {f g : A[X]A[X] →ₐ[R] B}
    (hC : f.comp CAlgHom = g.comp CAlgHom)
    (hX : f X = g X) : f = g :=
  AlgHom.coe_ringHom_injective (ringHom_ext' (congr_arg AlgHom.toRingHom hC) hX)

Extensionality of Algebra Homomorphisms on Polynomial Rings via Constants and Variable

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any two $R$-algebra homomorphisms $f, g \colon A[X] \to B$ from the polynomial ring over $A$ to an $R$-algebra $B$, if: 1. The compositions with the constant embedding are equal: $f \circ C = g \circ C$, and 2. They agree on the polynomial variable: $f(X) = g(X)$, then $f = g$.

Polynomial.toFinsuppIsoAlg definition

: R[X] ≃ₐ[R] R[ℕ]

Full source

/-- Algebra isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials. -/
@[simps!]
def toFinsuppIsoAlg : R[X]R[X] ≃ₐ[R] R[ℕ] :=
  { toFinsuppIso R with
    commutes' := fun r => by
      dsimp }

Polynomial ring to monoid algebra algebra isomorphism

Informal description

The algebra isomorphism between the polynomial ring $R[X]$ and the additive monoid algebra $R[\mathbb{N}]$, which preserves the $R$-algebra structure. Specifically: - The forward map sends a polynomial $p \in R[X]$ to its representation as a finitely supported function $\mathbb{N} \to R$ - The inverse map reconstructs a polynomial from such a representation - The isomorphism preserves both the additive and multiplicative structures, as well as the $R$-algebra structure (i.e., it commutes with the algebra maps from $R$) This isomorphism is primarily an implementation detail for transferring results between polynomial and monoid algebra representations.

Polynomial.subalgebraNontrivial instance

[Nontrivial A] : Nontrivial (Subalgebra R A[X])

Full source

instance subalgebraNontrivial [Nontrivial A] : Nontrivial (Subalgebra R A[X]) :=
  ⟨⟨⊥, ⊤, by
      rw [Ne, SetLike.ext_iff, not_forall]
      refine ⟨X, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top,
        algebraMap_apply, not_forall]
      intro x
      rw [ext_iff, not_forall]
      refine ⟨1, ?_⟩
      simp [coeff_C]⟩⟩

Nontriviality of Polynomial Subalgebra over Nontrivial Algebra

Informal description

For any nontrivial $R$-algebra $A$, the subalgebra of $A[X]$ is also nontrivial.

Polynomial.algHom_eval₂_algebraMap theorem

 {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (p : R[X]) (f : A →ₐ[R] B)
  (a : A) : f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p

Full source

@[simp]
theorem algHom_eval₂_algebraMap {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
    [Algebra R A] [Algebra R B] (p : R[X]) (f : A →ₐ[R] B) (a : A) :
    f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p := by
  simp only [eval₂_eq_sum, sum_def]
  simp only [map_sum, map_mul, map_pow, eq_intCast, map_intCast, AlgHom.commutes]

Evaluation of Polynomials under Algebra Homomorphisms

Informal description

Let $R$, $A$, and $B$ be commutative semirings, where $A$ and $B$ are also $R$-algebras. For any polynomial $p \in R[X]$, any $R$-algebra homomorphism $f \colon A \to B$, and any element $a \in A$, we have: \[ f\big(\text{eval}_2(\text{algebraMap}_R A, a, p)\big) = \text{eval}_2(\text{algebraMap}_R B, f(a), p), \] where $\text{eval}_2$ denotes the evaluation of the polynomial $p$ at $a$ using the algebra map $\text{algebraMap}_R A \colon R \to A$ (respectively $\text{algebraMap}_R B \colon R \to B$).

Polynomial.eval₂_algebraMap_X theorem

 {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (p : R[X]) (f : R[X] →ₐ[R] A) :
  eval₂ (algebraMap R A) (f X) p = f p

Full source

@[simp]
theorem eval₂_algebraMap_X {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (p : R[X])
    (f : R[X]R[X] →ₐ[R] A) : eval₂ (algebraMap R A) (f X) p = f p := by
  conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]
  simp only [eval₂_eq_sum, sum_def]
  simp only [map_sum, map_mul, map_pow, eq_intCast, map_intCast]
  simp [Polynomial.C_eq_algebraMap]

Evaluation of Polynomials via Algebra Homomorphism at $X$

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring that is also an $R$-algebra. For any polynomial $p \in R[X]$ and any $R$-algebra homomorphism $f \colon R[X] \to A$, the evaluation of $p$ at $f(X)$ via the algebra map $\text{algebraMap}_R A \colon R \to A$ equals $f(p)$. In other words, \[ \text{eval}_2(\text{algebraMap}_R A, f(X), p) = f(p). \]

Polynomial.ringHom_eval₂_intCastRingHom theorem

 {R S : Type*} [Ring R] [Ring S] (p : ℤ[X]) (f : R →+* S) (r : R) :
  f (eval₂ (Int.castRingHom R) r p) = eval₂ (Int.castRingHom S) (f r) p

Full source

@[simp]
theorem ringHom_eval₂_intCastRingHom {R S : Type*} [Ring R] [Ring S] (p : ℤℤ[X]) (f : R →+* S)
    (r : R) : f (eval₂ (Int.castRingHom R) r p) = eval₂ (Int.castRingHom S) (f r) p :=
  algHom_eval₂_algebraMap p f.toIntAlgHom r

Evaluation of Integer Polynomials under Ring Homomorphisms

Informal description

Let $R$ and $S$ be rings, $p \in \mathbb{Z}[X]$ be an integer polynomial, $f \colon R \to S$ be a ring homomorphism, and $r \in R$ be an element. Then: \[ f\big(\text{eval}_2(\text{Int.castRingHom}_R, r, p)\big) = \text{eval}_2(\text{Int.castRingHom}_S, f(r), p), \] where $\text{eval}_2$ denotes the evaluation of the polynomial $p$ at $r$ using the canonical ring homomorphism $\text{Int.castRingHom}_R \colon \mathbb{Z} \to R$ (respectively $\text{Int.castRingHom}_S \colon \mathbb{Z} \to S$).

Polynomial.eval₂_intCastRingHom_X theorem

{R : Type*} [Ring R] (p : ℤ[X]) (f : ℤ[X] →+* R) : eval₂ (Int.castRingHom R) (f X) p = f p

Full source

@[simp]
theorem eval₂_intCastRingHom_X {R : Type*} [Ring R] (p : ℤℤ[X]) (f : ℤℤ[X]ℤ[X] →+* R) :
    eval₂ (Int.castRingHom R) (f X) p = f p :=
  eval₂_algebraMap_X p f.toIntAlgHom

Evaluation of Integer Polynomials via Ring Homomorphism at $X$

Informal description

Let $R$ be a ring, $p \in \mathbb{Z}[X]$ be an integer polynomial, and $f \colon \mathbb{Z}[X] \to R$ be a ring homomorphism. Then the evaluation of $p$ at $f(X)$ via the canonical ring homomorphism $\mathbb{Z} \to R$ equals $f(p)$. In other words, \[ \text{eval}_2(\text{Int.castRingHom}_R, f(X), p) = f(p). \]

Polynomial.eval₂AlgHom' definition

(f : A →ₐ[R] B) (b : B) (hf : ∀ a, Commute (f a) b) : A[X] →ₐ[R] B

Full source

/-- `Polynomial.eval₂` as an `AlgHom` for noncommutative algebras.

This is `Polynomial.eval₂RingHom'` for `AlgHom`s. -/
@[simps!]
def eval₂AlgHom' (f : A →ₐ[R] B) (b : B) (hf : ∀ a, Commute (f a) b) : A[X]A[X] →ₐ[R] B where
  toRingHom := eval₂RingHom' f b hf
  commutes' _ := (eval₂_C _ _).trans (f.commutes _)

Algebra homomorphism induced by polynomial evaluation at a commuting element

Informal description

Given an algebra homomorphism $ f \colon A \to B $ over a commutative semiring $ R $, and an element $ b \in B $ that commutes with every element in the image of $ f $, the function `Polynomial.eval₂AlgHom'` constructs an algebra homomorphism from the polynomial ring $ A[X] $ to $ B $. This homomorphism evaluates each polynomial in $ A[X] $ at $ b $ using the coefficients transformed by $ f $.

Polynomial.mapAlgHom definition

(f : A →ₐ[R] B) : Polynomial A →ₐ[R] Polynomial B

Full source

/-- `Polynomial.map` as an `AlgHom` for noncommutative algebras.

  This is the algebra version of `Polynomial.mapRingHom`. -/
def mapAlgHom (f : A →ₐ[R] B) : PolynomialPolynomial A →ₐ[R] Polynomial B where
  toRingHom := mapRingHom f.toRingHom
  commutes' := by simp

Algebra homomorphism induced by coefficient mapping

Informal description

Given a commutative semiring $R$ and $R$-algebras $A$ and $B$, for any algebra homomorphism $f \colon A \to B$ over $R$, the function `Polynomial.mapAlgHom` constructs an algebra homomorphism from the polynomial ring $A[X]$ to $B[X]$. This homomorphism applies $f$ to each coefficient of a polynomial in $A[X]$, resulting in a polynomial in $B[X]$.

Polynomial.coe_mapAlgHom theorem

(f : A →ₐ[R] B) : ⇑(mapAlgHom f) = map f

Full source

@[simp]
theorem coe_mapAlgHom (f : A →ₐ[R] B) : ⇑(mapAlgHom f) = map f :=
  rfl

Coefficient Mapping of Polynomial Algebra Homomorphism

Informal description

For any commutative semiring $R$ and $R$-algebra homomorphism $f \colon A \to B$, the underlying function of the algebra homomorphism `mapAlgHom f` from $A[X]$ to $B[X]$ is equal to the polynomial coefficient mapping function `map f`.

Polynomial.mapAlgHom_id theorem

: mapAlgHom (AlgHom.id R A) = AlgHom.id R (Polynomial A)

Full source

@[simp]
theorem mapAlgHom_id : mapAlgHom (AlgHom.id R A) = AlgHom.id R (Polynomial A) :=
  AlgHom.ext fun _x => map_id

Identity Mapping of Polynomial Algebra Homomorphism

Informal description

The algebra homomorphism induced by the identity map on an $R$-algebra $A$ is equal to the identity algebra homomorphism on the polynomial ring $A[X]$. In other words, $\text{mapAlgHom}(\text{id}_A) = \text{id}_{A[X]}$.

Polynomial.mapAlgHom_coe_ringHom theorem

(f : A →ₐ[R] B) : ↑(mapAlgHom f : _ →ₐ[R] Polynomial B) = (mapRingHom ↑f : Polynomial A →+* Polynomial B)

Full source

@[simp]
theorem mapAlgHom_coe_ringHom (f : A →ₐ[R] B) :
    ↑(mapAlgHom f : _ →ₐ[R] Polynomial B) = (mapRingHom ↑f : PolynomialPolynomial A →+* Polynomial B) :=
  rfl

Underlying Ring Homomorphism of Polynomial Algebra Homomorphism via Coefficient Mapping

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any algebra homomorphism $f \colon A \to B$ over $R$, the underlying ring homomorphism of the algebra homomorphism $\mathrm{mapAlgHom}\, f \colon A[X] \to B[X]$ is equal to the ring homomorphism $\mathrm{mapRingHom}\, f \colon A[X] \to B[X]$ obtained by applying $f$ to each coefficient.

Polynomial.mapAlgHom_comp theorem

 (C : Type z) [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) :
  (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)

Full source

@[simp]
theorem mapAlgHom_comp (C : Type z) [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) :
    (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g) := by
  apply AlgHom.ext
  intro x
  simp [AlgHom.comp_algebraMap, map_map]
  congr

Composition of Induced Polynomial Algebra Homomorphisms

Informal description

Let $R$ be a commutative semiring, and let $A$, $B$, and $C$ be $R$-algebras. For any $R$-algebra homomorphisms $g \colon A \to B$ and $f \colon B \to C$, the composition of the induced polynomial algebra homomorphisms satisfies: $$(\text{mapAlgHom}\, f) \circ (\text{mapAlgHom}\, g) = \text{mapAlgHom}\, (f \circ g)$$ where $\text{mapAlgHom}$ denotes the extension of an algebra homomorphism to polynomial rings.

Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom theorem

(f : A →ₐ[R] B) : mapAlgHom f = eval₂AlgHom' (CAlgHom.comp f) X (fun a => (commute_X (C (f a))).symm)

Full source

theorem mapAlgHom_eq_eval₂AlgHom'_CAlgHom (f : A →ₐ[R] B) : mapAlgHom f = eval₂AlgHom'
    (CAlgHom.comp f) X (fun a => (commute_X (C (f a))).symm) := by
  apply AlgHom.ext
  intro x
  congr

Equality of Polynomial Algebra Homomorphisms: $\mathrm{mapAlgHom} = \mathrm{eval₂AlgHom}' \circ \mathrm{CAlgHom}$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any $R$-algebra homomorphism $f \colon A \to B$, the algebra homomorphism $\mathrm{mapAlgHom} \colon A[X] \to B[X]$ induced by coefficient-wise application of $f$ is equal to the evaluation homomorphism $\mathrm{eval₂AlgHom}'$ at $X$ composed with the constant embedding homomorphism $\mathrm{CAlgHom} \circ f$, where $X$ commutes with all constant polynomials in $B[X]$.

Polynomial.mapAlgEquiv definition

(f : A ≃ₐ[R] B) : Polynomial A ≃ₐ[R] Polynomial B

Full source

/-- If `A` and `B` are isomorphic as `R`-algebras, then so are their polynomial rings -/
def mapAlgEquiv (f : A ≃ₐ[R] B) : PolynomialPolynomial A ≃ₐ[R] Polynomial B :=
  AlgEquiv.ofAlgHom (mapAlgHom f.toAlgHom) (mapAlgHom f.symm.toAlgHom) (by simp) (by simp)

Algebra isomorphism between polynomial rings induced by coefficient isomorphism

Informal description

Given a commutative semiring $R$ and $R$-algebras $A$ and $B$, for any algebra isomorphism $f \colon A \to B$ over $R$, the function `Polynomial.mapAlgEquiv` constructs an algebra isomorphism between the polynomial rings $A[X]$ and $B[X]$. This isomorphism applies $f$ to each coefficient of a polynomial in $A[X]$, resulting in a polynomial in $B[X]$, and its inverse applies $f^{-1}$ to coefficients in $B[X]$.

Polynomial.coe_mapAlgEquiv theorem

(f : A ≃ₐ[R] B) : ⇑(mapAlgEquiv f) = map f

Full source

@[simp]
theorem coe_mapAlgEquiv (f : A ≃ₐ[R] B) : ⇑(mapAlgEquiv f) = map f :=
  rfl

Coefficient-wise map of polynomial algebra isomorphism equals polynomial map

Informal description

For any commutative semiring $R$ and $R$-algebra isomorphism $f \colon A \to B$, the underlying function of the algebra isomorphism $\mathrm{mapAlgEquiv} \colon A[X] \to B[X]$ is equal to the coefficient-wise application of $f$ to polynomials in $A[X]$.

Polynomial.mapAlgEquiv_id theorem

: mapAlgEquiv (@AlgEquiv.refl R A _ _ _) = AlgEquiv.refl

Full source

@[simp]
theorem mapAlgEquiv_id : mapAlgEquiv (@AlgEquiv.refl R A _ _ _) = AlgEquiv.refl :=
  AlgEquiv.ext fun _x => map_id

Identity Algebra Isomorphism Induces Identity on Polynomial Rings

Informal description

The algebra isomorphism `Polynomial.mapAlgEquiv` applied to the identity algebra isomorphism $\text{AlgEquiv.refl} \colon A \to A$ yields the identity algebra isomorphism on the polynomial ring $A[X]$, i.e., \[ \text{mapAlgEquiv}(\text{AlgEquiv.refl}) = \text{AlgEquiv.refl}. \]

Polynomial.mapAlgEquiv_coe_ringHom theorem

 (f : A ≃ₐ[R] B) : ↑(mapAlgEquiv f : _ ≃ₐ[R] Polynomial B) = (mapRingHom ↑f : Polynomial A →+* Polynomial B)

Full source

@[simp]
theorem mapAlgEquiv_coe_ringHom (f : A ≃ₐ[R] B) :
    ↑(mapAlgEquiv f : _ ≃ₐ[R] Polynomial B) = (mapRingHom ↑f : PolynomialPolynomial A →+* Polynomial B) :=
  rfl

Equality of Ring Homomorphisms Induced by Algebra Isomorphism on Polynomial Rings

Informal description

Given a commutative semiring $R$ and $R$-algebra isomorphism $f \colon A \to B$, the underlying ring homomorphism of the algebra isomorphism `mapAlgEquiv f` between polynomial rings $A[X]$ and $B[X]$ is equal to the polynomial ring homomorphism induced by the underlying ring homomorphism of $f$.

Polynomial.mapAlgEquiv_toAlgHom theorem

(f : A ≃ₐ[R] B) : (mapAlgEquiv f : Polynomial A →ₐ[R] Polynomial B) = mapAlgHom f

Full source

@[simp]
theorem mapAlgEquiv_toAlgHom (f : A ≃ₐ[R] B) :
    (mapAlgEquiv f : PolynomialPolynomial A →ₐ[R] Polynomial B) = mapAlgHom f := rfl

Equality of Algebra Homomorphisms Induced by Polynomial Map of Algebra Isomorphism

Informal description

For any commutative semiring $R$ and $R$-algebra isomorphism $f \colon A \to B$, the algebra homomorphism induced by `mapAlgEquiv f` from $A[X]$ to $B[X]$ is equal to the algebra homomorphism `mapAlgHom f`.

Polynomial.mapAlgEquiv_comp theorem

 (C : Type*) [Semiring C] [Algebra R C] (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) :
  (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Full source

@[simp]
theorem mapAlgEquiv_comp (C : Type*) [Semiring C] [Algebra R C] (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) :
    (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g) := by
  apply AlgEquiv.ext
  intro x
  simp [AlgEquiv.trans_apply, map_map]
  congr

Composition of Polynomial Algebra Isomorphisms Induced by Coefficient Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $A$, $B$, and $C$ be $R$-algebras. Given $R$-algebra isomorphisms $f \colon A \to B$ and $g \colon B \to C$, the composition of the induced algebra isomorphisms $\text{mapAlgEquiv}(f) \colon A[X] \to B[X]$ and $\text{mapAlgEquiv}(g) \colon B[X] \to C[X]$ is equal to the algebra isomorphism $\text{mapAlgEquiv}(f \circ g) \colon A[X] \to C[X]$. In other words, the following diagram commutes: $$ A[X] \xrightarrow{\text{mapAlgEquiv}(f)} B[X] \xrightarrow{\text{mapAlgEquiv}(g)} C[X] = A[X] \xrightarrow{\text{mapAlgEquiv}(f \circ g)} C[X]. $$

Polynomial.aeval definition

: R[X] →ₐ[R] A

Full source

/-- Given a valuation `x` of the variable in an `R`-algebra `A`, `aeval R A x` is
the unique `R`-algebra homomorphism from `R[X]` to `A` sending `X` to `x`.

This is a stronger variant of the linear map `Polynomial.leval`. -/
def aeval : R[X]R[X] →ₐ[R] A :=
  eval₂AlgHom' (Algebra.ofId _ _) x (Algebra.commutes · _)

Polynomial evaluation as an algebra homomorphism

Informal description

Given a commutative semiring $R$ and an $R$-algebra $A$, for any element $x \in A$, the function $\text{aeval}_x \colon R[X] \to A$ is the unique $R$-algebra homomorphism that sends the polynomial variable $X$ to $x$. It evaluates a polynomial $p \in R[X]$ at $x$ by substituting $x$ for $X$ and applying the algebra structure map to the coefficients.

Polynomial.algHom_ext theorem

{f g : R[X] →ₐ[R] B} (hX : f X = g X) : f = g

Full source

@[ext 1200]
theorem algHom_ext {f g : R[X]R[X] →ₐ[R] B} (hX : f X = g X) :
    f = g :=
  algHom_ext' (Subsingleton.elim _ _) hX

Extensionality of Algebra Homomorphisms on Polynomial Rings via Variable Condition

Informal description

Let $R$ be a commutative semiring and $B$ an $R$-algebra. For any two $R$-algebra homomorphisms $f, g \colon R[X] \to B$, if $f(X) = g(X)$, then $f = g$.

Polynomial.aeval_def theorem

(p : R[X]) : aeval x p = eval₂ (algebraMap R A) x p

Full source

theorem aeval_def (p : R[X]) : aeval x p = eval₂ (algebraMap R A) x p :=
  rfl

Equivalence of Polynomial Evaluation via Algebra Homomorphism and $\text{eval}_2$

Informal description

For any polynomial $p \in R[X]$ over a commutative semiring $R$, and any element $x$ in an $R$-algebra $A$, the evaluation of $p$ at $x$ via the algebra homomorphism $\text{aeval}_x$ is equal to the evaluation of $p$ at $x$ using the algebra structure map $\text{algebraMap} \colon R \to A$ and the polynomial evaluation function $\text{eval}_2$.

Polynomial.aeval_zero theorem

: aeval x (0 : R[X]) = 0

Full source

theorem aeval_zero : aeval x (0 : R[X]) = 0 :=
  map_zero (aeval x)

Evaluation of Zero Polynomial Yields Zero

Informal description

For any element $x$ in an $R$-algebra $A$, the evaluation of the zero polynomial at $x$ via the algebra homomorphism $\text{aeval}_x$ yields the zero element of $A$, i.e., $\text{aeval}_x(0) = 0$.

Polynomial.aeval_X theorem

: aeval x (X : R[X]) = x

Full source

@[simp]
theorem aeval_X : aeval x (X : R[X]) = x :=
  eval₂_X _ x

Evaluation of Polynomial Variable: $\text{aeval}_x(X) = x$

Informal description

For any $R$-algebra $A$ and any element $x \in A$, the evaluation of the polynomial variable $X$ at $x$ via the algebra homomorphism $\text{aeval}_x$ equals $x$, i.e., $\text{aeval}_x(X) = x$.

Polynomial.aeval_C theorem

(r : R) : aeval x (C r) = algebraMap R A r

Full source

@[simp]
theorem aeval_C (r : R) : aeval x (C r) = algebraMap R A r :=
  eval₂_C _ x

Evaluation of Constant Polynomial via Algebra Homomorphism

Informal description

For any commutative semiring $R$, any $R$-algebra $A$, and any element $x \in A$, the evaluation of the constant polynomial $C(r) \in R[X]$ at $x$ via the algebra homomorphism $\text{aeval}_x$ is equal to the image of $r$ under the algebra structure map from $R$ to $A$, i.e., $\text{aeval}_x(C(r)) = \text{algebraMap}_{R,A}(r)$.

Polynomial.aeval_monomial theorem

{n : ℕ} {r : R} : aeval x (monomial n r) = algebraMap _ _ r * x ^ n

Full source

@[simp]
theorem aeval_monomial {n : ℕ} {r : R} : aeval x (monomial n r) = algebraMap _ _ r * x ^ n :=
  eval₂_monomial _ _

Evaluation of monomials via algebra homomorphism

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any element $x \in A$, natural number $n \in \mathbb{N}$, and coefficient $r \in R$, the evaluation of the monomial $rX^n$ at $x$ via the algebra homomorphism $\text{aeval}_x$ equals the image of $r$ under the algebra structure map multiplied by $x^n$, i.e., \[ \text{aeval}_x(rX^n) = \iota(r) \cdot x^n \] where $\iota \colon R \to A$ is the $R$-algebra structure map.

Polynomial.aeval_X_pow theorem

{n : ℕ} : aeval x ((X : R[X]) ^ n) = x ^ n

Full source

theorem aeval_X_pow {n : ℕ} : aeval x ((X : R[X]) ^ n) = x ^ n :=
  eval₂_X_pow _ _

Evaluation of $X^n$ via Algebra Homomorphism: $\text{aeval}_x(X^n) = x^n$

Informal description

For any natural number $n$, the algebra homomorphism evaluation of the polynomial $X^n$ at an element $x$ in an $R$-algebra $A$ is equal to $x^n$, i.e., $\text{aeval}_x(X^n) = x^n$.

Polynomial.aeval_add theorem

: aeval x (p + q) = aeval x p + aeval x q

Full source

theorem aeval_add : aeval x (p + q) = aeval x p + aeval x q :=
  map_add _ _ _

Additivity of Polynomial Evaluation Homomorphism

Informal description

For any commutative semiring $R$, $R$-algebra $A$, element $x \in A$, and polynomials $p, q \in R[X]$, the evaluation homomorphism satisfies $\text{aeval}_x(p + q) = \text{aeval}_x(p) + \text{aeval}_x(q)$.

Polynomial.aeval_one theorem

: aeval x (1 : R[X]) = 1

Full source

theorem aeval_one : aeval x (1 : R[X]) = 1 :=
  map_one _

Evaluation of the Constant Polynomial One: $\text{aeval}_x(1) = 1$

Informal description

For any commutative semiring $R$, any $R$-algebra $A$, and any element $x \in A$, the evaluation of the constant polynomial $1 \in R[X]$ at $x$ via the algebra homomorphism $\text{aeval}_x$ is equal to the multiplicative identity $1 \in A$, i.e., $\text{aeval}_x(1) = 1$.

Polynomial.aeval_natCast theorem

(n : ℕ) : aeval x (n : R[X]) = n

Full source

theorem aeval_natCast (n : ℕ) : aeval x (n : R[X]) = n :=
  map_natCast _ _

Evaluation of Constant Polynomials: $\text{aeval}_x(n) = n$

Informal description

For any natural number $n$ and any element $x$ in an $R$-algebra $A$, the evaluation of the constant polynomial $n$ at $x$ via the algebra homomorphism $\text{aeval}_x$ equals $n$, i.e., $\text{aeval}_x(n) = n$.

Polynomial.aeval_mul theorem

: aeval x (p * q) = aeval x p * aeval x q

Full source

theorem aeval_mul : aeval x (p * q) = aeval x p * aeval x q :=
  map_mul _ _ _

Evaluation of Polynomial Product via Algebra Homomorphism

Informal description

For any polynomials $p, q \in R[X]$ and any element $x$ in an $R$-algebra $A$, the evaluation of the product $p * q$ at $x$ equals the product of the evaluations of $p$ and $q$ at $x$, i.e., \[ \text{aeval}_x(p * q) = \text{aeval}_x(p) \cdot \text{aeval}_x(q). \]

Polynomial.comp_eq_aeval theorem

: p.comp q = aeval q p

Full source

theorem comp_eq_aeval : p.comp q = aeval q p := rfl

Composition Equals Evaluation via Algebra Homomorphism

Informal description

For any polynomials $p, q \in R[X]$, the composition $p \circ q$ is equal to the evaluation of $p$ at $q$ via the algebra homomorphism $\text{aeval}$, i.e., $p \circ q = \text{aeval}(q)(p)$.

Polynomial.aeval_comp theorem

{A : Type*} [Semiring A] [Algebra R A] (x : A) : aeval x (p.comp q) = aeval (aeval x q) p

Full source

theorem aeval_comp {A : Type*} [Semiring A] [Algebra R A] (x : A) :
    aeval x (p.comp q) = aeval (aeval x q) p :=
  eval₂_comp' x p q

Evaluation of Polynomial Composition via Algebra Homomorphism

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any polynomials $p, q \in R[X]$ and any element $x \in A$, the evaluation of the composition $p \circ q$ at $x$ equals the evaluation of $p$ at the evaluation of $q$ at $x$. That is, $\text{aeval}_x(p \circ q) = \text{aeval}_{\text{aeval}_x(q)}(p)$.

Polynomial.algEquivOfCompEqX definition

(p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) : R[X] ≃ₐ[R] R[X]

Full source

/-- Two polynomials `p` and `q` such that `p(q(X))=X` and `q(p(X))=X`
  induces an automorphism of the polynomial algebra. -/
@[simps!]
def algEquivOfCompEqX (p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) : R[X]R[X] ≃ₐ[R] R[X] := by
  refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_ <;>
    exact AlgHom.ext fun _ ↦ by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

Algebra automorphism induced by inverse polynomial compositions

Informal description

Given two polynomials $p, q \in R[X]$ over a commutative semiring $R$ such that $p \circ q = X$ and $q \circ p = X$, the function `algEquivOfCompEqX` constructs an $R$-algebra automorphism of $R[X]$. This automorphism is defined by evaluating polynomials at $p$ and $q$ respectively, and it satisfies the condition that composition with these evaluations returns the original polynomial variable $X$.

Polynomial.algEquivOfCompEqX_eq_iff theorem

 (p q p' q' : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) (hpq' : p'.comp q' = X) (hqp' : q'.comp p' = X) :
  algEquivOfCompEqX p q hpq hqp = algEquivOfCompEqX p' q' hpq' hqp' ↔ p = p'

Full source

@[simp]
theorem algEquivOfCompEqX_eq_iff (p q p' q' : R[X])
    (hpq : p.comp q = X) (hqp : q.comp p = X) (hpq' : p'.comp q' = X) (hqp' : q'.comp p' = X) :
    algEquivOfCompEqXalgEquivOfCompEqX p q hpq hqp = algEquivOfCompEqX p' q' hpq' hqp' ↔ p = p' :=
  ⟨fun h ↦ by simpa using congr($h X), fun h ↦ by ext1; simp [h]⟩

Equality of Polynomial Composition Automorphisms iff Leading Polynomials Are Equal

Informal description

Let $R$ be a commutative semiring and let $p, q, p', q' \in R[X]$ be polynomials such that: 1. $p \circ q = X$ and $q \circ p = X$ 2. $p' \circ q' = X$ and $q' \circ p' = X$ Then the algebra automorphisms $\text{algEquivOfCompEqX}_p^q$ and $\text{algEquivOfCompEqX}_{p'}^{q'}$ of $R[X]$ are equal if and only if $p = p'$.

Polynomial.algEquivOfCompEqX_symm theorem

 (p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) :
  (algEquivOfCompEqX p q hpq hqp).symm = algEquivOfCompEqX q p hqp hpq

Full source

@[simp]
theorem algEquivOfCompEqX_symm (p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) :
    (algEquivOfCompEqX p q hpq hqp).symm = algEquivOfCompEqX q p hqp hpq := rfl

Inverse of Polynomial Composition Automorphism

Informal description

Let $R$ be a commutative semiring and let $p, q \in R[X]$ be polynomials such that $p \circ q = X$ and $q \circ p = X$. Then the inverse of the $R$-algebra automorphism $\text{algEquivOfCompEqX}(p, q)$ is equal to $\text{algEquivOfCompEqX}(q, p)$.

Polynomial.algEquivCMulXAddC definition

{R : Type*} [CommRing R] (a b : R) [Invertible a] : R[X] ≃ₐ[R] R[X]

Full source

/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(a * X + b)`,
  with inverse `p(X) ↦ p(a⁻¹ * (X - b))`. -/
@[simps!]
def algEquivCMulXAddC {R : Type*} [CommRing R] (a b : R) [Invertible a] : R[X]R[X] ≃ₐ[R] R[X] :=
  algEquivOfCompEqX (C a * X + C b) (C ⅟ a * (X - C b))
    (by simp [← C_mul, ← mul_assoc]) (by simp [← C_mul, ← mul_assoc])

Polynomial automorphism induced by affine transformation $X \mapsto aX + b$

Informal description

Given a commutative ring $R$ and elements $a, b \in R$ with $a$ invertible, the function `algEquivCMulXAddC` constructs an $R$-algebra automorphism of the polynomial ring $R[X]$. This automorphism maps a polynomial $p(X)$ to $p(aX + b)$, with inverse mapping $p(X)$ to $p(a^{-1}(X - b))$.

Polynomial.algEquivCMulXAddC_symm_eq theorem

 {R : Type*} [CommRing R] (a b : R) [Invertible a] : (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟ a) (-⅟ a * b)

Full source

theorem algEquivCMulXAddC_symm_eq {R : Type*} [CommRing R] (a b : R) [Invertible a] :
    (algEquivCMulXAddC a b).symm =  algEquivCMulXAddC (⅟ a) (- ⅟ a * b) := by
  ext p : 1
  simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]
  congr
  simp [mul_add, sub_eq_add_neg]

Inverse of Affine Polynomial Automorphism: $\text{algEquivCMulXAddC}(a, b)^{-1} = \text{algEquivCMulXAddC}(a^{-1}, -a^{-1}b)$

Informal description

Let $R$ be a commutative ring, and let $a, b \in R$ with $a$ invertible. The inverse of the $R$-algebra automorphism $\text{algEquivCMulXAddC}(a, b)$ of $R[X]$, which maps $p(X)$ to $p(aX + b)$, is equal to $\text{algEquivCMulXAddC}(a^{-1}, -a^{-1}b)$.

Polynomial.algEquivAevalXAddC definition

{R : Type*} [CommRing R] (t : R) : R[X] ≃ₐ[R] R[X]

Full source

/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(X+t)`,
  with inverse `p(X) ↦ p(X-t)`. -/
@[simps!]
def algEquivAevalXAddC {R : Type*} [CommRing R] (t : R) : R[X]R[X] ≃ₐ[R] R[X] :=
  algEquivOfCompEqX (X + C t) (X - C t) (by simp) (by simp)

Polynomial algebra automorphism induced by translation $ X \mapsto X + t $

Informal description

For any commutative ring $ R $ and any element $ t \in R $, the function `algEquivAevalXAddC` defines an $ R $-algebra automorphism of the polynomial ring $ R[X] $. This automorphism maps a polynomial $ p(X) $ to $ p(X + t) $, with its inverse mapping $ p(X) $ to $ p(X - t) $.

Polynomial.algEquivAevalXAddC_eq_iff theorem

{R : Type*} [CommRing R] (t t' : R) : algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t'

Full source

@[simp]
theorem algEquivAevalXAddC_eq_iff {R : Type*} [CommRing R] (t t' : R) :
    algEquivAevalXAddCalgEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t' := by
  simp [algEquivAevalXAddC]

Equality of Polynomial Algebra Automorphisms via Translation Parameters

Informal description

For any commutative ring $R$ and elements $t, t' \in R$, the algebra automorphisms $\text{algEquivAevalXAddC}(t)$ and $\text{algEquivAevalXAddC}(t')$ of the polynomial ring $R[X]$ are equal if and only if $t = t'$.

Polynomial.algEquivAevalXAddC_symm theorem

{R : Type*} [CommRing R] (t : R) : (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

Full source

@[simp]
theorem algEquivAevalXAddC_symm {R : Type*} [CommRing R] (t : R) :
    (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t) := by
  simp [algEquivAevalXAddC, sub_eq_add_neg]

Inverse of Polynomial Translation Automorphism: $\text{algEquivAevalXAddC}(t)^{-1} = \text{algEquivAevalXAddC}(-t)$

Informal description

For any commutative ring $R$ and any element $t \in R$, the inverse of the algebra automorphism $\text{algEquivAevalXAddC}(t)$ of the polynomial ring $R[X]$ is equal to $\text{algEquivAevalXAddC}(-t)$. In other words, the inverse of the automorphism that maps a polynomial $p(X)$ to $p(X + t)$ is the automorphism that maps $p(X)$ to $p(X - t)$.

Polynomial.algEquivAevalNegX definition

{R : Type*} [CommRing R] : R[X] ≃ₐ[R] R[X]

Full source

/-- The involutive automorphism of the polynomial algebra given by `p(X) ↦ p(-X)`. -/
@[simps!]
def algEquivAevalNegX {R : Type*} [CommRing R] : R[X]R[X] ≃ₐ[R] R[X] :=
  algEquivOfCompEqX (-X) (-X) (by simp) (by simp)

Algebra automorphism induced by $X \mapsto -X$

Informal description

The algebra automorphism of the polynomial ring $R[X]$ over a commutative ring $R$ given by mapping a polynomial $p(X)$ to $p(-X)$. This is an involution, meaning applying it twice returns the original polynomial.

Polynomial.comp_neg_X_comp_neg_X theorem

{R : Type*} [CommRing R] (p : R[X]) : (p.comp (-X)).comp (-X) = p

Full source

theorem comp_neg_X_comp_neg_X {R : Type*} [CommRing R] (p : R[X]) :
    (p.comp (-X)).comp (-X) = p := by
  rw [comp_assoc]
  simp only [neg_comp, X_comp, neg_neg, comp_X]

Double Composition with $-X$ Yields Original Polynomial

Informal description

For any commutative ring $R$ and any polynomial $p \in R[X]$, composing $p$ with $-X$ twice yields the original polynomial, i.e., $(p \circ (-X)) \circ (-X) = p$.

Polynomial.aeval_algHom theorem

(f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x)

Full source

theorem aeval_algHom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
  algHom_ext <| by simp only [aeval_X, AlgHom.comp_apply]

Compatibility of Polynomial Evaluation with Algebra Homomorphisms: $\text{aeval}_{f(x)} = f \circ \text{aeval}_x$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any $R$-algebra homomorphism $f \colon A \to B$ and any element $x \in A$, the evaluation homomorphism $\text{aeval}_{f(x)} \colon R[X] \to B$ is equal to the composition of $f$ with the evaluation homomorphism $\text{aeval}_x \colon R[X] \to A$, i.e., $\text{aeval}_{f(x)} = f \circ \text{aeval}_x$.

Polynomial.aeval_X_left theorem

: aeval (X : R[X]) = AlgHom.id R R[X]

Full source

@[simp]
theorem aeval_X_left : aeval (X : R[X]) = AlgHom.id R R[X] :=
  algHom_ext <| aeval_X X

Evaluation at $X$ is the identity algebra homomorphism on $R[X]$

Informal description

The algebra homomorphism $\text{aeval}_X \colon R[X] \to R[X]$, which evaluates a polynomial at the variable $X$, is equal to the identity algebra homomorphism $\text{id} \colon R[X] \to R[X]$.

Polynomial.aeval_X_left_apply theorem

(p : R[X]) : aeval X p = p

Full source

theorem aeval_X_left_apply (p : R[X]) : aeval X p = p :=
  AlgHom.congr_fun (@aeval_X_left R _) p

Evaluation at $X$ is the identity on polynomials

Informal description

For any polynomial $p \in R[X]$, the evaluation of $p$ at the polynomial variable $X$ is equal to $p$ itself, i.e., $\text{aeval}_X(p) = p$.

Polynomial.eval_unique theorem

(φ : R[X] →ₐ[R] A) (p) : φ p = eval₂ (algebraMap R A) (φ X) p

Full source

theorem eval_unique (φ : R[X]R[X] →ₐ[R] A) (p) : φ p = eval₂ (algebraMap R A) (φ X) p := by
  rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]

Uniqueness of Polynomial Evaluation as Algebra Homomorphism: $\varphi(p) = \text{eval}_2(\text{algebraMap}, \varphi(X))(p)$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any $R$-algebra homomorphism $\varphi \colon R[X] \to A$ and any polynomial $p \in R[X]$, the evaluation of $\varphi$ at $p$ equals the evaluation of $p$ at $\varphi(X)$ via the algebra structure map $\text{algebraMap} \colon R \to A$, i.e., \[ \varphi(p) = \text{eval}_2(\text{algebraMap}_R^A, \varphi(X))(p). \]

Polynomial.aeval_algHom_apply theorem

{F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) (x : A) (p : R[X]) : aeval (f x) p = f (aeval x p)

Full source

theorem aeval_algHom_apply {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
    (f : F) (x : A) (p : R[X]) :
    aeval (f x) p = f (aeval x p) := by
  refine Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => ?_)
    (by simp [AlgHomClass.commutes])
  rw [map_add, hp, hq, ← map_add, ← map_add]

Compatibility of Polynomial Evaluation with Algebra Homomorphisms: $\text{aeval}_{f(x)}(p) = f(\text{aeval}_x(p))$

Informal description

Let $R$ be a commutative semiring, $A$ and $B$ be $R$-algebras, and $F$ be a type of $R$-algebra homomorphisms from $A$ to $B$. For any homomorphism $f \in F$, any element $x \in A$, and any polynomial $p \in R[X]$, the evaluation of $p$ at $f(x)$ via the algebra homomorphism $\text{aeval}_{f(x)}$ equals the image under $f$ of the evaluation of $p$ at $x$, i.e., \[ \text{aeval}_{f(x)}(p) = f(\text{aeval}_x(p)). \]

Polynomial.coe_aeval_mk_apply theorem

{S : Subalgebra R A} (h : x ∈ S) : (aeval (⟨x, h⟩ : S) p : A) = aeval x p

Full source

@[simp]
lemma coe_aeval_mk_apply {S : Subalgebra R A} (h : x ∈ S) :
    (aeval (⟨x, h⟩ : S) p : A) = aeval x p :=
  (aeval_algHom_apply S.val (⟨x, h⟩ : S) p).symm

Subalgebra Evaluation Consistency: $\text{aeval}_{\langle x, h \rangle}(p) = \text{aeval}_x(p)$ for $x \in S$

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $S$ a subalgebra of $A$. For any element $x \in A$ that belongs to $S$ (i.e., $x \in S$) and any polynomial $p \in R[X]$, the evaluation of $p$ at the inclusion $\langle x, h \rangle \in S$ (where $h$ is the proof that $x \in S$) is equal to the evaluation of $p$ at $x$ in $A$. That is, \[ \text{aeval}_{\langle x, h \rangle}(p) = \text{aeval}_x(p). \]

Polynomial.aeval_algEquiv theorem

(f : A ≃ₐ[R] B) (x : A) : aeval (f x) = (f : A →ₐ[R] B).comp (aeval x)

Full source

theorem aeval_algEquiv (f : A ≃ₐ[R] B) (x : A) : aeval (f x) = (f : A →ₐ[R] B).comp (aeval x) :=
  aeval_algHom (f : A →ₐ[R] B) x

Compatibility of Polynomial Evaluation with Algebra Isomorphisms: $\text{aeval}_{f(x)} = f \circ \text{aeval}_x$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any $R$-algebra isomorphism $f \colon A \to B$ and any element $x \in A$, the evaluation homomorphism $\text{aeval}_{f(x)} \colon R[X] \to B$ is equal to the composition of $f$ with the evaluation homomorphism $\text{aeval}_x \colon R[X] \to A$, i.e., \[ \text{aeval}_{f(x)} = f \circ \text{aeval}_x. \]

Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval theorem

(x : R) (p : R[X]) : aeval (algebraMap R A x) p = algebraMap R A (p.eval x)

Full source

theorem aeval_algebraMap_apply_eq_algebraMap_eval (x : R) (p : R[X]) :
    aeval (algebraMap R A x) p = algebraMap R A (p.eval x) :=
  aeval_algHom_apply (Algebra.ofId R A) x p

Compatibility of Polynomial Evaluation with Algebra Structure Map: $\text{aeval}(\text{algebraMap}(x), p) = \text{algebraMap}(p(x))$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any element $x \in R$ and any polynomial $p \in R[X]$, the evaluation of $p$ at the image of $x$ under the algebra structure map $\text{algebraMap}_R^A$ equals the image under $\text{algebraMap}_R^A$ of the evaluation of $p$ at $x$. In other words: \[ \text{aeval}(\text{algebraMap}_R^A(x), p) = \text{algebraMap}_R^A(p(x)) \]

Polynomial.aeval_prod theorem

(x : A × B) : aeval (R := R) x = (aeval x.1).prod (aeval x.2)

Full source

/-- Polynomial evaluation on a pair is a product of the evaluations on the components. -/
theorem aeval_prod (x : A × B) : aeval (R := R) x = (aeval x.1).prod (aeval x.2) :=
  aeval_algHom (.fst R A B) x ▸ aeval_algHom (.snd R A B) x ▸
    (aeval x).prod_comp (.fst R A B) (.snd R A B)

Evaluation of Polynomials on Product Algebras: $\text{aeval}_{(x_1, x_2)} = \text{aeval}_{x_1} \times \text{aeval}_{x_2}$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any pair $(x_1, x_2) \in A \times B$, the evaluation homomorphism $\text{aeval}_{(x_1, x_2)} \colon R[X] \to A \times B$ is equal to the product of the evaluation homomorphisms $\text{aeval}_{x_1} \colon R[X] \to A$ and $\text{aeval}_{x_2} \colon R[X] \to B$. That is, \[ \text{aeval}_{(x_1, x_2)} = \text{aeval}_{x_1} \times \text{aeval}_{x_2}. \]

Polynomial.aeval_prod_apply theorem

(x : A × B) (p : Polynomial R) : p.aeval x = (p.aeval x.1, p.aeval x.2)

Full source

/-- Polynomial evaluation on a pair is a pair of evaluations. -/
theorem aeval_prod_apply (x : A × B) (p : Polynomial R) :
    p.aeval x = (p.aeval x.1, p.aeval x.2) := by simp [aeval_prod]

Componentwise Evaluation of Polynomials on Product Algebras: $p(x_1, x_2) = (p(x_1), p(x_2))$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any polynomial $p \in R[X]$ and any pair $(x_1, x_2) \in A \times B$, the evaluation of $p$ at $(x_1, x_2)$ is given by the pair of evaluations $(p(x_1), p(x_2))$. That is, \[ p(x_1, x_2) = (p(x_1), p(x_2)). \]

Polynomial.aeval_pi theorem

(x : Π i, A i) : aeval (R := R) x = Pi.algHom R A (fun i ↦ aeval (x i))

Full source

/-- Polynomial evaluation on an indexed tuple is the indexed product of the evaluations
on the components.
Generalizes `Polynomial.aeval_prod` to indexed products. -/
theorem aeval_pi (x : Π i, A i) : aeval (R := R) x = Pi.algHom R A (fun i ↦ aeval (x i)) :=
  (funext fun i ↦ aeval_algHom (Pi.evalAlgHom R A i) x) ▸
    (Pi.algHom_comp R A (Pi.evalAlgHom R A) (aeval x))

Componentwise Polynomial Evaluation on Product Algebras: $\text{aeval}_x = \prod_i \text{aeval}_{x_i}$

Informal description

Let $R$ be a commutative semiring and $(A_i)_{i \in I}$ be a family of $R$-algebras. For any indexed tuple $x = (x_i)_{i \in I}$ where $x_i \in A_i$ for each $i$, the evaluation of a polynomial $p \in R[X]$ at $x$ is equal to the componentwise evaluation of $p$ at each $x_i$. That is, the algebra homomorphism $\text{aeval}_x \colon R[X] \to \prod_{i \in I} A_i$ is equal to the product of the evaluation homomorphisms $\text{aeval}_{x_i} \colon R[X] \to A_i$ for each $i \in I$.

Polynomial.aeval_pi_apply₂ theorem

(j : I) : p.aeval x j = p.aeval (x j)

Full source

theorem aeval_pi_apply₂ (j : I) : p.aeval x j = p.aeval (x j) :=
  aeval_pi (R := R) x ▸ Pi.algHom_apply R A (fun i ↦ aeval (x i)) p j

Componentwise Polynomial Evaluation: $(p(x))_j = p(x_j)$

Informal description

Let $R$ be a commutative semiring and $(A_i)_{i \in I}$ be a family of $R$-algebras. For any polynomial $p \in R[X]$ and any tuple $x = (x_i)_{i \in I}$ with $x_i \in A_i$ for each $i \in I$, the $j$-th component of the evaluation of $p$ at $x$ equals the evaluation of $p$ at $x_j$. That is, for any index $j \in I$, we have $$(p(x))_j = p(x_j).$$

Polynomial.aeval_pi_apply theorem

: p.aeval x = fun j ↦ p.aeval (x j)

Full source

/-- Polynomial evaluation on an indexed tuple is the indexed tuple of the evaluations
on the components.
Generalizes `Polynomial.aeval_prod_apply` to indexed products. -/
theorem aeval_pi_apply : p.aeval x = fun j ↦ p.aeval (x j) :=
  funext fun j ↦ aeval_pi_apply₂ x p j

Componentwise Polynomial Evaluation: $p(x) = (j \mapsto p(x_j))$

Informal description

Let $R$ be a commutative semiring and $(A_i)_{i \in I}$ be a family of $R$-algebras. For any polynomial $p \in R[X]$ and any tuple $x = (x_i)_{i \in I}$ with $x_i \in A_i$ for each $i \in I$, the evaluation of $p$ at $x$ is equal to the function that maps each index $j \in I$ to the evaluation of $p$ at $x_j$. That is, $$p(x) = \big(j \mapsto p(x_j)\big).$$

Polynomial.coe_aeval_eq_eval theorem

(r : R) : (aeval r : R[X] → R) = eval r

Full source

@[simp]
theorem coe_aeval_eq_eval (r : R) : (aeval r : R[X] → R) = eval r :=
  rfl

Equality of Polynomial Evaluation via Algebra Homomorphism and Standard Evaluation

Informal description

For any element $r$ in a commutative semiring $R$, the evaluation of a polynomial $p \in R[X]$ at $r$ via the algebra homomorphism $\text{aeval}_r$ coincides with the standard polynomial evaluation $\text{eval}_r(p)$. That is, $\text{aeval}_r(p) = \text{eval}_r(p)$ for all $p \in R[X]$.

Polynomial.coe_aeval_eq_evalRingHom theorem

(x : R) : ((aeval x : R[X] →ₐ[R] R) : R[X] →+* R) = evalRingHom x

Full source

@[simp]
theorem coe_aeval_eq_evalRingHom (x : R) :
    ((aeval x : R[X]R[X] →ₐ[R] R) : R[X]R[X] →+* R) = evalRingHom x :=
  rfl

Equality of Evaluation Homomorphisms: $\text{aeval}_x$ and $\text{evalRingHom}_x$

Informal description

For any element $x$ in a commutative semiring $R$, the underlying ring homomorphism of the algebra homomorphism $\text{aeval}_x \colon R[X] \to R$ is equal to the evaluation homomorphism $\text{evalRingHom}_x \colon R[X] \to R$.

Polynomial.aeval_fn_apply theorem

{X : Type*} (g : R[X]) (f : X → R) (x : X) : ((aeval f) g) x = aeval (f x) g

Full source

@[simp]
theorem aeval_fn_apply {X : Type*} (g : R[X]) (f : X → R) (x : X) :
    ((aeval f) g) x = aeval (f x) g :=
  (aeval_algHom_apply (Pi.evalAlgHom R (fun _ => R) x) f g).symm

Polynomial Evaluation Commutes with Function Application: $(\text{aeval}(f)(g))(x) = \text{aeval}(f(x))(g)$

Informal description

Let $R$ be a commutative semiring and $X$ be a type. For any polynomial $g \in R[X]$, any function $f \colon X \to R$, and any element $x \in X$, the evaluation of the polynomial $\text{aeval}(f)(g)$ at $x$ equals the evaluation of $g$ at $f(x)$, i.e., \[ (\text{aeval}(f)(g))(x) = \text{aeval}(f(x))(g). \]

Polynomial.aeval_subalgebra_coe theorem

(g : R[X]) {A : Type*} [Semiring A] [Algebra R A] (s : Subalgebra R A) (f : s) : (aeval f g : A) = aeval (f : A) g

Full source

@[norm_cast]
theorem aeval_subalgebra_coe (g : R[X]) {A : Type*} [Semiring A] [Algebra R A] (s : Subalgebra R A)
    (f : s) : (aeval f g : A) = aeval (f : A) g :=
  (aeval_algHom_apply s.val f g).symm

Compatibility of Polynomial Evaluation with Subalgebra Inclusion: $\text{aeval}_f(g) = \text{aeval}_{(f \in s)}(g)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any polynomial $g \in R[X]$, any $R$-subalgebra $s$ of $A$, and any element $f \in s$, the evaluation of $g$ at $f$ (considered as an element of $s$) equals the evaluation of $g$ at $f$ (considered as an element of $A$). In other words, the following diagram commutes: \[ \text{aeval}_f(g) \text{ in } A = \text{aeval}_{(f \in s)}(g) \text{ in } A. \]

Polynomial.coeff_zero_eq_aeval_zero theorem

(p : R[X]) : p.coeff 0 = aeval 0 p

Full source

theorem coeff_zero_eq_aeval_zero (p : R[X]) : p.coeff 0 = aeval 0 p := by
  simp [coeff_zero_eq_eval_zero]

Constant Term Equals Evaluation at Zero

Informal description

For any polynomial $p \in R[X]$, the constant term (coefficient of $X^0$) equals the evaluation of $p$ at $0$, i.e., $p(0) = p_0$.

Polynomial.coeff_zero_eq_aeval_zero' theorem

(p : R[X]) : algebraMap R A (p.coeff 0) = aeval (0 : A) p

Full source

theorem coeff_zero_eq_aeval_zero' (p : R[X]) : algebraMap R A (p.coeff 0) = aeval (0 : A) p := by
  simp [aeval_def]

Constant Term Evaluation via Algebra Map: $\text{algebraMap}_R^A(p(0)) = p(0_A)$

Informal description

For any polynomial $p \in R[X]$ over a commutative semiring $R$, and any $R$-algebra $A$, the image of the constant term $p(0)$ under the algebra map $R \to A$ is equal to the evaluation of $p$ at $0$ in $A$, i.e., \[ \text{algebraMap}_R^A(p(0)) = p(0_A). \]

Polynomial.map_aeval_eq_aeval_map theorem

 {S T U : Type*} [Semiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U}
  (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : R[X]) (a : S) : ψ (aeval a p) = aeval (ψ a) (p.map φ)

Full source

theorem map_aeval_eq_aeval_map {S T U : Type*} [Semiring S] [CommSemiring T] [Semiring U]
    [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U}
    (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : R[X]) (a : S) :
    ψ (aeval a p) = aeval (ψ a) (p.map φ) := by
  conv_rhs => rw [aeval_def, ← eval_map]
  rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]

Commutativity of Polynomial Evaluation with Ring Homomorphisms: $\psi(p(a)) = p^\phi(\psi(a))$

Informal description

Let $R$ be a commutative semiring, $S$ a semiring with an $R$-algebra structure, $T$ a commutative semiring, and $U$ a semiring with a $T$-algebra structure. Given ring homomorphisms $\phi \colon R \to T$ and $\psi \colon S \to U$ such that the following diagram commutes: \[ \begin{CD} R @>{\phi}>> T \\ @V{\text{algebraMap}_R^S}VV @VV{\text{algebraMap}_T^U}V \\ S @>{\psi}>> U \end{CD} \] then for any polynomial $p \in R[X]$ and any element $a \in S$, we have: \[ \psi\big(\text{aeval}_a(p)\big) = \text{aeval}_{\psi(a)}\big(p.\text{map}(\phi)\big). \] Here, $\text{aeval}_a$ denotes the evaluation of polynomials in $R[X]$ at $a \in S$ via the $R$-algebra structure on $S$, and $p.\text{map}(\phi)$ is the polynomial in $T[X]$ obtained by applying $\phi$ to the coefficients of $p$.

Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero theorem

 [CommSemiring S] [CommSemiring T] [Algebra S T] {p q : S[X]} (h₁ : p ∣ q) {a : T} (h₂ : aeval a p = 0) : aeval a q = 0

Full source

theorem aeval_eq_zero_of_dvd_aeval_eq_zero [CommSemiring S] [CommSemiring T] [Algebra S T]
    {p q : S[X]} (h₁ : p ∣ q) {a : T} (h₂ : aeval a p = 0) : aeval a q = 0 := by
  rw [aeval_def, ← eval_map] at h₂ ⊢
  exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂

Divisibility Implies Zero Evaluation: $p \mid q \Rightarrow (\text{aeval}_a(p) = 0 \to \text{aeval}_a(q) = 0)$

Informal description

Let $S$ and $T$ be commutative semirings with $T$ an $S$-algebra. For any polynomials $p, q \in S[X]$ such that $p$ divides $q$, and for any element $a \in T$, if the evaluation of $p$ at $a$ is zero (i.e., $\text{aeval}_a(p) = 0$), then the evaluation of $q$ at $a$ is also zero (i.e., $\text{aeval}_a(q) = 0$).

Polynomial.aeval_eq_sum_range theorem

[Algebra R S] {p : R[X]} (x : S) : aeval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i

Full source

theorem aeval_eq_sum_range [Algebra R S] {p : R[X]} (x : S) :
    aeval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i := by
  simp_rw [Algebra.smul_def]
  exact eval₂_eq_sum_range (algebraMap R S) x

Polynomial Evaluation as Finite Sum: $\text{aeval}_x(p) = \sum_{i=0}^{\deg p} p_i x^i$

Informal description

Let $R$ be a commutative semiring and $S$ an $R$-algebra. For any polynomial $p \in R[X]$ and any element $x \in S$, the evaluation of $p$ at $x$ via the algebra homomorphism $\text{aeval}_x$ equals the finite sum: \[ \text{aeval}_x(p) = \sum_{i=0}^{\deg p} (p_i) \cdot x^i \] where $p_i$ denotes the coefficient of $X^i$ in $p$ and $\deg p$ is the degree of $p$.

Polynomial.aeval_eq_sum_range' theorem

 [Algebra R S] {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) : aeval x p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i

Full source

theorem aeval_eq_sum_range' [Algebra R S] {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) :
    aeval x p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i := by
  simp_rw [Algebra.smul_def]
  exact eval₂_eq_sum_range' (algebraMap R S) hn x

Polynomial Evaluation as Finite Sum for Degrees Below $n$

Informal description

Let $R$ and $S$ be commutative semirings with $S$ an $R$-algebra, and let $p \in R[X]$ be a polynomial. For any natural number $n$ such that the degree of $p$ is less than $n$, and for any element $x \in S$, the evaluation of $p$ at $x$ via the algebra homomorphism $\text{aeval}$ is equal to the finite sum: \[ \text{aeval}_x(p) = \sum_{i=0}^{n-1} (p_i \cdot x^i) \] where $p_i$ denotes the coefficient of $X^i$ in $p$.

Polynomial.isRoot_of_eval₂_map_eq_zero theorem

(hf : Function.Injective f) {r : R} : eval₂ f (f r) p = 0 → p.IsRoot r

Full source

theorem isRoot_of_eval₂_map_eq_zero (hf : Function.Injective f) {r : R} :
    eval₂ f (f r) p = 0 → p.IsRoot r := by
  intro h
  apply hf
  rw [← eval₂_hom, h, f.map_zero]

Injective Ring Homomorphism Preserves Polynomial Roots via Evaluation

Informal description

Let $R$ and $S$ be commutative semirings, $f: R \to S$ be an injective ring homomorphism, and $p \in R[X]$ be a polynomial. For any $r \in R$, if the evaluation of $p$ at $f(r)$ via $f$ is zero (i.e., $\text{eval}_2\, f\, (f\, r)\, p = 0$), then $r$ is a root of $p$ (i.e., $p(r) = 0$).

Polynomial.isRoot_of_aeval_algebraMap_eq_zero theorem

 [Algebra R S] {p : R[X]} (inj : Function.Injective (algebraMap R S)) {r : R} (hr : aeval (algebraMap R S r) p = 0) :
  p.IsRoot r

Full source

theorem isRoot_of_aeval_algebraMap_eq_zero [Algebra R S] {p : R[X]}
    (inj : Function.Injective (algebraMap R S)) {r : R} (hr : aeval (algebraMap R S r) p = 0) :
    p.IsRoot r :=
  isRoot_of_eval₂_map_eq_zero inj hr

Injective Algebra Map Preserves Polynomial Roots via Evaluation

Informal description

Let $R$ and $S$ be commutative semirings with $S$ an $R$-algebra, and let $p \in R[X]$ be a polynomial. If the algebra map $\text{algebraMap}\, R\, S : R \to S$ is injective, then for any $r \in R$, if the evaluation of $p$ at $\text{algebraMap}\, R\, S\, r$ via the algebra homomorphism $\text{aeval}$ is zero, then $r$ is a root of $p$.

Polynomial.aevalTower definition

(f : R →ₐ[S] A') (x : A') : R[X] →ₐ[S] A'

Full source

/-- Version of `aeval` for defining algebra homs out of `R[X]` over a smaller base ring
  than `R`. -/
def aevalTower (f : R →ₐ[S] A') (x : A') : R[X]R[X] →ₐ[S] A' :=
  eval₂AlgHom' f x fun _ => Commute.all _ _

Algebra homomorphism induced by polynomial evaluation via tower of algebras

Informal description

Given a commutative semiring $ S $, an $ S $-algebra $ R $, and another $ S $-algebra $ A' $, the function `Polynomial.aevalTower` constructs an algebra homomorphism from the polynomial ring $ R[X] $ to $ A' $. It takes as input an algebra homomorphism $ f \colon R \to A' $ over $ S $ and an element $ x \in A' $, and evaluates each polynomial in $ R[X] $ at $ x $ using the coefficients transformed by $ f $. The element $ x $ is required to commute with every element in the image of $ f $.

Polynomial.aevalTower_X theorem

: aevalTower g y X = y

Full source

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

Evaluation of Polynomial Variable in Tower Algebra Homomorphism: $\text{aevalTower}\,g\,y(X) = y$

Informal description

Given a commutative semiring $S$, an $S$-algebra $R$, another $S$-algebra $A'$, an algebra homomorphism $g \colon R \to A'$ over $S$, and an element $y \in A'$ that commutes with every element in the image of $g$, the evaluation of the polynomial variable $X$ under the algebra homomorphism $\text{aevalTower}\,g\,y$ equals $y$.

Polynomial.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 Polynomials in Tower Algebra Homomorphism: $\text{aevalTower}\,g\,y(C(x)) = g(x)$

Informal description

Let $S$ be a commutative semiring, $R$ an $S$-algebra, and $A'$ another $S$-algebra. Given an $S$-algebra homomorphism $g \colon R \to A'$ and an element $y \in A'$ that commutes with every element in the image of $g$, then for any $x \in R$, the evaluation of the constant polynomial $C(x) \in R[X]$ under the algebra homomorphism $\text{aevalTower}\,g\,y$ equals $g(x)$. In other words: \[ \text{aevalTower}\,g\,y(C(x)) = g(x). \]

Polynomial.aevalTower_comp_C theorem

: (aevalTower g y : R[X] →+* A').comp C = g

Full source

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

Composition of Polynomial Evaluation Homomorphism with Constant Embedding Equals Original Homomorphism

Informal description

Let $S$ be a commutative semiring, $R$ an $S$-algebra, and $A'$ another $S$-algebra. Given an $S$-algebra homomorphism $g \colon R \to A'$ and an element $y \in A'$ that commutes with every element in the image of $g$, the composition of the algebra homomorphism $\text{aevalTower}\,g\,y \colon R[X] \to A'$ with the constant polynomial embedding $C \colon R \to R[X]$ equals $g$. In other words: \[ (\text{aevalTower}\,g\,y) \circ C = g. \]

Polynomial.aevalTower_algebraMap theorem

(x : R) : aevalTower g y (algebraMap R R[X] x) = g x

Full source

theorem aevalTower_algebraMap (x : R) : aevalTower g y (algebraMap R R[X] x) = g x :=
  eval₂_C _ _

Evaluation of algebra map under polynomial tower evaluation

Informal description

Let $R$ be a commutative semiring and $A'$ be an $R$-algebra. Given an $R$-algebra homomorphism $g \colon R \to A'$ and an element $y \in A'$ that commutes with every element in the image of $g$, the evaluation of the algebra map $\text{algebraMap} \colon R \to R[X]$ at $x \in R$ under the tower evaluation homomorphism $\text{aevalTower}\, g\, y$ satisfies: \[ \text{aevalTower}\, g\, y\, (\text{algebraMap}\, R\, R[X]\, x) = g\, x \]

Polynomial.aevalTower_comp_algebraMap theorem

: (aevalTower g y : R[X] →+* A').comp (algebraMap R R[X]) = g

Full source

theorem aevalTower_comp_algebraMap : (aevalTower g y : R[X]R[X] →+* A').comp (algebraMap R R[X]) = g :=
  aevalTower_comp_C _ _

Composition of Polynomial Evaluation Homomorphism with Algebra Map Equals Original Homomorphism

Informal description

Let $S$ be a commutative semiring, $R$ an $S$-algebra, and $A'$ another $S$-algebra. Given an $S$-algebra homomorphism $g \colon R \to A'$ and an element $y \in A'$ that commutes with every element in the image of $g$, the composition of the algebra homomorphism $\text{aevalTower}\, g\, y \colon R[X] \to A'$ with the algebra map $\text{algebraMap} \colon R \to R[X]$ equals $g$. In other words: \[ (\text{aevalTower}\, g\, y) \circ \text{algebraMap} = g. \]

Polynomial.aevalTower_toAlgHom theorem

(x : R) : aevalTower g y (IsScalarTower.toAlgHom S R R[X] x) = g x

Full source

theorem aevalTower_toAlgHom (x : R) : aevalTower g y (IsScalarTower.toAlgHom S R R[X] x) = g x :=
  aevalTower_algebraMap _ _ _

Evaluation of scalar tower algebra homomorphism under polynomial tower evaluation

Informal description

Let $S$ be a commutative semiring, $R$ an $S$-algebra, and $A'$ another $S$-algebra. Given an $S$-algebra homomorphism $g \colon R \to A'$ and an element $y \in A'$ that commutes with every element in the image of $g$, the evaluation of the algebra homomorphism $\text{IsScalarTower.toAlgHom}\, S\, R\, R[X]$ at $x \in R$ under the tower evaluation homomorphism $\text{aevalTower}\, g\, y$ satisfies: \[ \text{aevalTower}\, g\, y\, (\text{IsScalarTower.toAlgHom}\, S\, R\, R[X]\, x) = g\, x \]

Polynomial.aevalTower_comp_toAlgHom theorem

: (aevalTower g y).comp (IsScalarTower.toAlgHom S R R[X]) = g

Full source

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

Composition of Polynomial Tower Evaluation with Scalar Tower Homomorphism Equals Original Homomorphism

Informal description

Let $S$ be a commutative semiring, $R$ an $S$-algebra, and $A'$ another $S$-algebra. Given an $S$-algebra homomorphism $g \colon R \to A'$ and an element $y \in A'$ that commutes with every element in the image of $g$, the composition of the algebra homomorphism $\text{aevalTower}\, g\, y \colon R[X] \to A'$ with the scalar tower algebra homomorphism $\text{IsScalarTower.toAlgHom}\, S\, R\, R[X]$ equals $g$. In other words: \[ (\text{aevalTower}\, g\, y) \circ (\text{IsScalarTower.toAlgHom}\, S\, R\, R[X]) = g. \]

Polynomial.aevalTower_id theorem

: aevalTower (AlgHom.id S S) = aeval

Full source

@[simp]
theorem aevalTower_id : aevalTower (AlgHom.id S S) = aeval := by
  ext s
  simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]

$\text{aevalTower}$ with identity homomorphism equals $\text{aeval}$

Informal description

Let $S$ be a commutative semiring. The algebra homomorphism $\text{aevalTower}$ applied to the identity algebra homomorphism $\text{AlgHom.id}\,S\,S$ is equal to the polynomial evaluation homomorphism $\text{aeval}$.

Polynomial.aevalTower_ofId theorem

: aevalTower (Algebra.ofId S A') = aeval

Full source

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

$\text{aevalTower}$ of Identity Algebra Homomorphism Equals $\text{aeval}$

Informal description

For any commutative semiring $S$ and $S$-algebra $A'$, the algebra homomorphism $\text{aevalTower}$ induced by the identity algebra homomorphism $\text{Algebra.ofId}\,S\,A'$ is equal to the standard polynomial evaluation homomorphism $\text{aeval}$.

Polynomial.dvd_term_of_dvd_eval_of_dvd_terms theorem

 {z p : S} {f : S[X]} (i : ℕ) (dvd_eval : p ∣ f.eval z) (dvd_terms : ∀ j ≠ i, p ∣ f.coeff j * z ^ j) :
  p ∣ f.coeff i * z ^ i

Full source

theorem dvd_term_of_dvd_eval_of_dvd_terms {z p : S} {f : S[X]} (i : ℕ) (dvd_eval : p ∣ f.eval z)
    (dvd_terms : ∀ j ≠ i, p ∣ f.coeff j * z ^ j) : p ∣ f.coeff i * z ^ i := by
  by_cases hi : i ∈ f.support
  · rw [eval, eval₂_eq_sum, sum_def] at dvd_eval
    rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.not_mem_erase _ _)] at dvd_eval
    refine (dvd_add_left ?_).mp dvd_eval
    apply Finset.dvd_sum
    intro j hj
    exact dvd_terms j (Finset.ne_of_mem_erase hj)
  · convert dvd_zero p
    rw [not_mem_support_iff] at hi
    simp [hi]

Divisibility of Polynomial Term from Evaluation and Other Terms

Informal description

Let $S$ be a commutative ring, $z, p \in S$, and $f \in S[X]$ a polynomial. For any natural number $i$, if $p$ divides the evaluation $f(z)$ and $p$ divides each term $f_j \cdot z^j$ for all $j \neq i$, then $p$ divides the $i$-th term $f_i \cdot z^i$.

Polynomial.dvd_term_of_isRoot_of_dvd_terms theorem

{r p : S} {f : S[X]} (i : ℕ) (hr : f.IsRoot r) (h : ∀ j ≠ i, p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i

Full source

theorem dvd_term_of_isRoot_of_dvd_terms {r p : S} {f : S[X]} (i : ℕ) (hr : f.IsRoot r)
    (h : ∀ j ≠ i, p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i :=
  dvd_term_of_dvd_eval_of_dvd_terms i (Eq.symm hr ▸ dvd_zero p) h

Divisibility of Polynomial Term from Root Condition and Other Terms

Informal description

Let $S$ be a commutative ring, $r, p \in S$, and $f \in S[X]$ a polynomial. For any natural number $i$, if $r$ is a root of $f$ (i.e., $f(r) = 0$) and $p$ divides each term $f_j \cdot r^j$ for all $j \neq i$, then $p$ divides the $i$-th term $f_i \cdot r^i$.

Polynomial.eval_mul_X_sub_C theorem

{p : R[X]} (r : R) : (p * (X - C r)).eval r = 0

Full source

/-- The evaluation map is not generally multiplicative when the coefficient ring is noncommutative,
but nevertheless any polynomial of the form `p * (X - monomial 0 r)` is sent to zero
when evaluated at `r`.

This is the key step in our proof of the Cayley-Hamilton theorem.
-/
theorem eval_mul_X_sub_C {p : R[X]} (r : R) : (p * (X - C r)).eval r = 0 := by
  simp only [eval, eval₂_eq_sum, RingHom.id_apply]
  have bound :=
    calc
      (p * (X - C r)).natDegree ≤ p.natDegree + (X - C r).natDegree := natDegree_mul_le
      _ ≤ p.natDegree + 1 := add_le_add_left (natDegree_X_sub_C_le _) _
      _ < p.natDegree + 2 := lt_add_one _
  rw [sum_over_range' _ _ (p.natDegree + 2) bound]
  swap
  · simp
  rw [sum_range_succ']
  conv_lhs =>
    congr
    arg 2
    simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ']
  rw [sum_range_sub']
  simp [coeff_monomial]

Vanishing Evaluation of $p \cdot (X - r)$ at $r$

Informal description

For any polynomial $p \in R[X]$ over a ring $R$ and any element $r \in R$, the evaluation of the product $p \cdot (X - r)$ at $r$ is zero, i.e., $$(p \cdot (X - r))(r) = 0.$$

Polynomial.not_isUnit_X_sub_C theorem

[Nontrivial R] (r : R) : ¬IsUnit (X - C r)

Full source

theorem not_isUnit_X_sub_C [Nontrivial R] (r : R) : ¬IsUnit (X - C r) :=
  fun ⟨⟨_, g, _hfg, hgf⟩, rfl⟩ => zero_ne_one' R <| by rw [← eval_mul_X_sub_C, hgf, eval_one]

Non-unit Property of Linear Polynomials in Nontrivial Rings

Informal description

For any nontrivial ring $R$ and any element $r \in R$, the polynomial $X - r$ is not a unit in the polynomial ring $R[X]$.

Polynomial.aeval_endomorphism theorem

 {M : Type*} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) (p : R[X]) :
  aeval f p v = p.sum fun n b => b • (f ^ n) v

Full source

theorem aeval_endomorphism {M : Type*} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M)
    (v : M) (p : R[X]) : aeval f p v = p.sum fun n b => b • (f ^ n) v := by
  rw [aeval_def, eval₂_eq_sum]
  exact map_sum (LinearMap.applyₗ v) _ _

Polynomial Evaluation Formula for Endomorphisms

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $f \colon M \to M$ an $R$-linear endomorphism. For any polynomial $p \in R[X]$ and any vector $v \in M$, the evaluation of $p$ at $f$ applied to $v$ equals the sum over the coefficients of $p$: \[ \text{aeval}_f(p)(v) = \sum_{n \in \text{support}(p)} p_n \cdot f^n(v), \] where $p_n$ is the coefficient of $X^n$ in $p$ and $f^n$ denotes the $n$-fold composition of $f$ with itself.

Polynomial.X_sub_C_pow_dvd_iff theorem

{n : ℕ} : (X - C t) ^ n ∣ p ↔ X ^ n ∣ p.comp (X + C t)

Full source

lemma X_sub_C_pow_dvd_iff {n : ℕ} : (X - C t) ^ n ∣ p(X - C t) ^ n ∣ p ↔ X ^ n ∣ p.comp (X + C t) := by
  convert (map_dvd_iff <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]

Divisibility of $(X - t)^n$ in Polynomial Ring $R[X]$ is Equivalent to Divisibility of $X^n$ in $p(X + t)$

Informal description

For any natural number $n$, the polynomial $(X - t)^n$ divides a polynomial $p$ if and only if $X^n$ divides the composition $p(X + t)$.

Polynomial.comp_X_add_C_eq_zero_iff theorem

: p.comp (X + C t) = 0 ↔ p = 0

Full source

lemma comp_X_add_C_eq_zero_iff : p.comp (X + C t) = 0 ↔ p = 0 :=
  EmbeddingLike.map_eq_zero_iff (f := algEquivAevalXAddC t)

Vanishing of Translated Polynomial Composition: $p(X + t) = 0 \leftrightarrow p = 0$

Informal description

For any polynomial $p \in R[X]$ and any element $t \in R$, the composition $p(X + t)$ is the zero polynomial if and only if $p$ itself is the zero polynomial.

Polynomial.comp_X_add_C_ne_zero_iff theorem

: p.comp (X + C t) ≠ 0 ↔ p ≠ 0

Full source

lemma comp_X_add_C_ne_zero_iff : p.comp (X + C t) ≠ 0p.comp (X + C t) ≠ 0 ↔ p ≠ 0 := comp_X_add_C_eq_zero_iff.not

Non-vanishing of Translated Polynomial Composition: $p(X + t) \neq 0 \leftrightarrow p \neq 0$

Informal description

For any polynomial $p \in R[X]$ and any element $t \in R$, the composition $p(X + t)$ is nonzero if and only if $p$ itself is nonzero.

Polynomial.dvd_comp_C_mul_X_add_C_iff theorem

(p q : R[X]) (a b : R) [Invertible a] : p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟ a * (X - C b)) ∣ q

Full source

lemma dvd_comp_C_mul_X_add_C_iff (p q : R[X]) (a b : R) [Invertible a] :
    p ∣ q.comp (C a * X + C b)p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟ a * (X - C b)) ∣ q := by
  convert map_dvd_iff <| algEquivCMulXAddC a b using 2
  simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]

Divisibility under Affine Composition: $p \mid q(aX + b) \leftrightarrow p\left(\frac{1}{a}(X - b)\right) \mid q$

Informal description

Let $R$ be a commutative ring, $p, q \in R[X]$ be polynomials, and $a, b \in R$ with $a$ invertible. Then $p$ divides the composition $q(aX + b)$ if and only if the composition $p\left(\frac{1}{a}(X - b)\right)$ divides $q$.

Polynomial.dvd_comp_X_sub_C_iff theorem

(p q : R[X]) (a : R) : p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Full source

lemma dvd_comp_X_sub_C_iff (p q : R[X]) (a : R) :
    p ∣ q.comp (X - C a)p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q := by
  let _ := invertibleOne (α := R)
  simpa using dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

Divisibility under Translation Composition: $p \mid q(X - a) \leftrightarrow p(X + a) \mid q$

Informal description

Let $R$ be a commutative ring and $p, q \in R[X]$ be polynomials. For any $a \in R$, the polynomial $p$ divides the composition $q(X - a)$ if and only if the composition $p(X + a)$ divides $q$.

Polynomial.dvd_comp_X_add_C_iff theorem

(p q : R[X]) (a : R) : p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q

Full source

lemma dvd_comp_X_add_C_iff (p q : R[X]) (a : R) :
    p ∣ q.comp (X + C a)p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q := by
  simpa using dvd_comp_X_sub_C_iff p q (-a)

Divisibility under Translation Composition: $p \mid q(X + a) \leftrightarrow p(X - a) \mid q$

Informal description

Let $R$ be a commutative ring and $p, q \in R[X]$ be polynomials. For any $a \in R$, the polynomial $p$ divides the composition $q(X + a)$ if and only if the composition $p(X - a)$ divides $q$.

Polynomial.dvd_comp_neg_X_iff theorem

(p q : R[X]) : p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Full source

lemma dvd_comp_neg_X_iff (p q : R[X]) : p ∣ q.comp (-X)p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q := by
  let _ := invertibleOne (α := R)
  let _ := invertibleNeg (R := R) 1
  simpa using dvd_comp_C_mul_X_add_C_iff p q (-1) 0

Divisibility under Negation Composition: $p \mid q(-X) \leftrightarrow p(-X) \mid q$

Informal description

For any polynomials $p, q$ in the polynomial ring $R[X]$, $p$ divides the composition $q(-X)$ if and only if the composition $p(-X)$ divides $q$.

Polynomial.units_coeff_zero_smul theorem

(c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p

Full source

lemma units_coeff_zero_smul (c : R[X]R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p := by
  rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]

Scalar Multiplication by Constant Term of Invertible Polynomial Equals Polynomial Multiplication

Informal description

For any invertible polynomial $c \in R[X]^\times$ and any polynomial $p \in R[X]$, the scalar multiplication of the constant term of $c$ (i.e., $c_0$) with $p$ is equal to the product of $c$ and $p$ in the polynomial ring $R[X]$. That is, $c_0 \cdot p = c \cdot p$.

Polynomial.aeval_apply_smul_mem_of_le_comap' theorem

 [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (hm : m ∈ q) (p : R[X]) (a : A)
  (hq : q ≤ q.comap (Algebra.lsmul R R M a)) : aeval a p • m ∈ q

Full source

lemma aeval_apply_smul_mem_of_le_comap'
    [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (hm : m ∈ q) (p : R[X]) (a : A)
    (hq : q ≤ q.comap (Algebra.lsmul R R M a)) :
    aevalaeval a p • m ∈ q := by
  induction p using Polynomial.induction_on with
  | C a => simpa using SMulMemClass.smul_mem a hm
  | add f₁ f₂ h₁ h₂ =>
    simp_rw [map_add, add_smul]
    exact Submodule.add_mem q h₁ h₂
  | monomial n t hmq =>
    dsimp only at hmq ⊢
    rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
    rw [← q.map_le_iff_le_comap] at hq
    exact hq ⟨_, hmq, rfl⟩

Polynomial evaluation preserves submodule membership under scalar multiplication tower condition

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $M$ an $A$-module such that the scalar multiplication operations form a tower $R \to A \to M$. Given a submodule $q \subseteq M$, an element $m \in q$, a polynomial $p \in R[X]$, and an element $a \in A$, if $q$ is contained in the pullback of $q$ under the left scalar multiplication map $\text{lsmul}_R(a) : M \to M$, then the evaluation of $p$ at $a$ acting on $m$ (via $\text{aeval}_a(p) \bullet m$) remains in $q$.

Polynomial.aeval_apply_smul_mem_of_le_comap theorem

(hm : m ∈ q) (p : R[X]) (f : Module.End R M) (hq : q ≤ q.comap f) : aeval f p m ∈ q

Full source

lemma aeval_apply_smul_mem_of_le_comap
    (hm : m ∈ q) (p : R[X]) (f : Module.End R M) (hq : q ≤ q.comap f) :
    aevalaeval f p m ∈ q :=
  aeval_apply_smul_mem_of_le_comap' hm p f hq

Polynomial Evaluation Preserves Submodule Membership Under Endomorphism Pullback Condition

Informal description

Let $R$ be a commutative semiring, $M$ an $R$-module, and $q$ a submodule of $M$. For any element $m \in q$, polynomial $p \in R[X]$, and $R$-linear endomorphism $f \in \text{End}_R(M)$, if $q$ is contained in the pullback of $q$ under $f$ (i.e., $q \subseteq f^{-1}(q)$), then the evaluation of $p$ at $f$ applied to $m$ (denoted $\text{aeval}_f(p)(m)$) belongs to $q$.

Polynomial.nmem_nonZeroDivisors_iff theorem

{P : R[X]} : P ∉ R[X]⁰ ↔ ∃ a : R, a ≠ 0 ∧ a • P = 0

Full source

/-- *McCoy theorem*: a polynomial `P : R[X]` is a zerodivisor if and only if there is `a : R`
such that `a ≠ 0` and `a • P = 0`. -/
theorem nmem_nonZeroDivisors_iff {P : R[X]} : P ∉ R[X]⁰P ∉ R[X]⁰ ↔ ∃ a : R, a ≠ 0 ∧ a • P = 0 := by
  refine ⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1 _) <| smul_eq_C_mul a ▸ h⟩
  by_contra! h
  obtain ⟨Q, hQ⟩ := _root_.nmem_nonZeroDivisors_iff.1 hP
  refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))
  contrapose! ha
  exact h a ha

McCoy's Theorem: Characterization of Zero Divisors in Polynomial Rings

Informal description

A polynomial $P \in R[X]$ is a zero divisor if and only if there exists a nonzero element $a \in R$ such that $a \cdot P = 0$.

Polynomial.mem_nonZeroDivisors_iff theorem

{P : R[X]} : P ∈ R[X]⁰ ↔ ∀ a : R, a • P = 0 → a = 0

Full source

protected lemma mem_nonZeroDivisors_iff {P : R[X]} : P ∈ R[X]⁰P ∈ R[X]⁰ ↔ ∀ a : R, a • P = 0 → a = 0 := by
  simpa [not_imp_not] using (nmem_nonZeroDivisors_iff (P := P)).not

Characterization of Non-Zero-Divisors in Polynomial Ring: $P \in R[X]^\times \leftrightarrow \forall a \in R, a \cdot P = 0 \rightarrow a = 0$

Informal description

A polynomial $P \in R[X]$ is a non-zero-divisor if and only if for every element $a \in R$, if $a \cdot P = 0$ then $a = 0$.

Polynomial.mem_nonzeroDivisors_of_coeff_mem theorem

{p : R[X]} (n : ℕ) (hp : p.coeff n ∈ R⁰) : p ∈ R[X]⁰

Full source

lemma mem_nonzeroDivisors_of_coeff_mem {p : R[X]} (n : ℕ) (hp : p.coeff n ∈ R⁰) :
    p ∈ R[X]⁰ :=
  Polynomial.mem_nonZeroDivisors_iff.mpr fun r hr ↦ hp _ (by simpa using congr(coeff $hr n))

Non-zero-divisor coefficient implies polynomial is a non-zero-divisor

Informal description

Let $R$ be a commutative semiring and $R[X]$ be the polynomial ring over $R$. For any polynomial $p \in R[X]$, if there exists a natural number $n$ such that the coefficient of $X^n$ in $p$ is a non-zero-divisor in $R$, then $p$ is a non-zero-divisor in $R[X]$.

Polynomial.X_mem_nonzeroDivisors theorem

: X ∈ R[X]⁰

Full source

lemma X_mem_nonzeroDivisors : XX ∈ R[X]⁰ :=
  mem_nonzeroDivisors_of_coeff_mem 1 (by simp [one_mem])

Polynomial Variable $X$ is a Non-Zero-Divisor in $R[X]$

Informal description

The polynomial variable $X$ in the polynomial ring $R[X]$ is a non-zero-divisor, i.e., $X \in R[X]^\times$.