Algebra towers for polynomial #
This file proves some basic results about the algebra tower structure for the type polynomial R.
This structure itself is provided elsewhere as polynomial.is_scalar_tower
theorem
is_scalar_tower.aeval_apply
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(x : A)
(p : R[X]) :
⇑(polynomial.aeval x) p = ⇑(polynomial.aeval x) (polynomial.map (algebra_map R S) p)
theorem
is_scalar_tower.algebra_map_aeval
(R : Type u)
(A : Type w)
(B : Type u₁)
[comm_semiring R]
[comm_semiring A]
[semiring B]
[algebra R A]
[algebra A B]
[algebra R B]
[is_scalar_tower R A B]
(x : A)
(p : R[X]) :
⇑(algebra_map A B) (⇑(polynomial.aeval x) p) = ⇑(polynomial.aeval (⇑(algebra_map A B) x)) p
theorem
is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero
(R : Type u)
(A : Type w)
(B : Type u₁)
[comm_semiring R]
[comm_semiring A]
[semiring B]
[algebra R A]
[algebra A B]
[algebra R B]
[is_scalar_tower R A B]
{x : A}
{p : R[X]}
(h : function.injective ⇑(algebra_map A B))
(hp : ⇑(polynomial.aeval (⇑(algebra_map A B) x)) p = 0) :
⇑(polynomial.aeval x) p = 0
theorem
is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[field A]
[comm_semiring B]
[nontrivial B]
[algebra R A]
[algebra R B]
[algebra A B]
[is_scalar_tower R A B]
{x : A}
{p : R[X]}
(h : ⇑(polynomial.aeval (⇑(algebra_map A B) x)) p = 0) :
⇑(polynomial.aeval x) p = 0
@[simp]
theorem
subalgebra.aeval_coe
(R : Type u)
{A : Type w}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
{S : subalgebra R A}
{x : ↥S}
{p : R[X]} :
⇑(polynomial.aeval ↑x) p = ↑(⇑(polynomial.aeval x) p)