Mathlib.RingTheory.Polynomial.Tower

Module docstring

{"# Algebra towers for polynomial

This file proves some basic results about the algebra tower structure for the type R[X].

This structure itself is provided elsewhere as Polynomial.isScalarTower

When you update this file, you can also try to make a corresponding update in RingTheory.MvPolynomial.Tower. "}

Polynomial.aeval_map_algebraMap theorem

(x : B) (p : R[X]) : aeval x (map (algebraMap R A) p) = aeval x p

Full source

@[simp]
theorem aeval_map_algebraMap (x : B) (p : R[X]) : aeval x (map (algebraMap R A) p) = aeval x p := by
  rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

Equality of Polynomial Evaluations via Algebra Maps

Informal description

Let $R$, $A$, and $B$ be commutative rings such that $A$ is an $R$-algebra and $B$ is an $A$-algebra. For any polynomial $p \in R[X]$ and any element $x \in B$, the evaluation of the polynomial $\text{map}(\text{algebraMap}_{R \to A}, p)$ at $x$ is equal to the evaluation of $p$ at $x$ via the algebra structure, i.e., \[ \text{aeval}_B(x, \text{map}(\text{algebraMap}_{R \to A}, p)) = \text{aeval}_B(x, p). \]

Polynomial.eval_map_algebraMap theorem

(P : R[X]) (b : B) : (map (algebraMap R B) P).eval b = aeval b P

Full source

@[simp]
lemma eval_map_algebraMap (P : R[X]) (b : B) :
    (map (algebraMap R B) P).eval b = aeval b P := by
  rw [aeval_def, eval_map]

Equality of Polynomial Evaluations via Algebra Map

Informal description

Let $R$ and $B$ be commutative rings such that $B$ is an $R$-algebra. For any polynomial $P \in R[X]$ and any element $b \in B$, the evaluation of the polynomial $\text{map}(\text{algebraMap}_{R \to B}, P)$ at $b$ is equal to the evaluation of $P$ at $b$ via the algebra structure, i.e., \[ \text{eval}_B(b, \text{map}(\text{algebraMap}_{R \to B}, P)) = \text{aeval}_B(b, P). \]

Polynomial.aeval_algebraMap_apply theorem

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

Full source

theorem aeval_algebraMap_apply (x : A) (p : R[X]) :
    aeval (algebraMap A B x) p = algebraMap A B (aeval x p) := by
  rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]

Algebra Map Commutes with Polynomial Evaluation

Informal description

Let $R$, $A$, and $B$ be commutative rings such that $A$ is an $R$-algebra and $B$ is an $A$-algebra. For any polynomial $p \in R[X]$ and any element $x \in A$, the evaluation of $p$ at the image of $x$ under the algebra map $\text{algebraMap}_{A \to B}$ is equal to the image under $\text{algebraMap}_{A \to B}$ of the evaluation of $p$ at $x$, i.e., \[ \text{aeval}_B(\text{algebraMap}_{A \to B}(x), p) = \text{algebraMap}_{A \to B}(\text{aeval}_A(x, p)). \]

Polynomial.aeval_algebraMap_eq_zero_iff theorem

[NoZeroSMulDivisors A B] [Nontrivial B] (x : A) (p : R[X]) : aeval (algebraMap A B x) p = 0 ↔ aeval x p = 0

Full source

@[simp]
theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : A) (p : R[X]) :
    aevalaeval (algebraMap A B x) p = 0 ↔ aeval x p = 0 := by
  rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]

Equivalence of Zero Evaluations via Algebra Map in Polynomial Algebra Tower

Informal description

Let $R$, $A$, and $B$ be commutative rings such that $A$ is an $R$-algebra and $B$ is an $A$-algebra, with $B$ being a nontrivial ring and having no zero smul divisors over $A$. For any polynomial $p \in R[X]$ and any element $x \in A$, the evaluation of $p$ at the image of $x$ under the algebra map $\text{algebraMap}_{A \to B}$ is zero if and only if the evaluation of $p$ at $x$ is zero, i.e., \[ \text{aeval}_B(\text{algebraMap}_{A \to B}(x), p) = 0 \leftrightarrow \text{aeval}_A(x, p) = 0. \]

Polynomial.aeval_algebraMap_eq_zero_iff_of_injective theorem

{x : A} {p : R[X]} (h : Function.Injective (algebraMap A B)) : aeval (algebraMap A B x) p = 0 ↔ aeval x p = 0

Full source

theorem aeval_algebraMap_eq_zero_iff_of_injective {x : A} {p : R[X]}
    (h : Function.Injective (algebraMap A B)) : aevalaeval (algebraMap A B x) p = 0 ↔ aeval x p = 0 := by
  rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Injective Algebra Map Preserves Zero Evaluation of Polynomials

Informal description

Let $R$, $A$, and $B$ be commutative rings such that $A$ is an $R$-algebra and $B$ is an $A$-algebra. If the algebra map $\text{algebraMap}_{A \to B}$ is injective, then for any polynomial $p \in R[X]$ and any element $x \in A$, the evaluation of $p$ at the image of $x$ under $\text{algebraMap}_{A \to B}$ is zero if and only if the evaluation of $p$ at $x$ is zero, i.e., \[ \text{aeval}_B(\text{algebraMap}_{A \to B}(x), p) = 0 \leftrightarrow \text{aeval}_A(x, p) = 0. \]

Subalgebra.aeval_coe theorem

(S : Subalgebra R A) (x : S) (p : R[X]) : aeval (x : A) p = aeval x p

Full source

@[simp]
theorem aeval_coe (S : Subalgebra R A) (x : S) (p : R[X]) : aeval (x : A) p = aeval x p :=
  aeval_algebraMap_apply A x p

Subalgebra Evaluation Consistency for Polynomials

Informal description

Let $R$ and $A$ be commutative rings such that $A$ is an $R$-algebra, and let $S$ be a subalgebra of $A$ over $R$. For any polynomial $p \in R[X]$ and any element $x \in S$, the evaluation of $p$ at $x$ (viewed as an element of $A$) is equal to the evaluation of $p$ at $x$ within the subalgebra $S$, i.e., \[ \text{aeval}_A(x, p) = \text{aeval}_S(x, p). \]