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.

@[simp]

theorem Polynomial.aeval_map_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : B) (p : Polynomial R) : (Polynomial.aeval x) (Polynomial.map (algebraMap R A) p) = (Polynomial.aeval x) p

@[simp]

theorem Polynomial.eval_map_algebraMap {R : Type u_1} (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] (P : Polynomial R) (a : A) : Polynomial.eval a (Polynomial.map (algebraMap R A) P) = (Polynomial.aeval a) P

theorem Polynomial.aeval_algebraMap_apply {R : Type u_1} {A : Type u_2} (B : Type u_3) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : A) (p : Polynomial R) : (Polynomial.aeval ((algebraMap A B) x)) p = (algebraMap A B) ((Polynomial.aeval x) p)

@[simp]

theorem Polynomial.aeval_algebraMap_eq_zero_iff {R : Type u_1} {A : Type u_2} (B : Type u_3) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [NoZeroSMulDivisors A B] [Nontrivial B] (x : A) (p : Polynomial R) : (Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0

theorem Polynomial.aeval_algebraMap_eq_zero_iff_of_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} {p : Polynomial R} (h : Function.Injective ⇑(algebraMap A B)) : (Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0

@[simp]

theorem Subalgebra.aeval_coe {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (p : Polynomial R) : (Polynomial.aeval ↑x) p = ↑((Polynomial.aeval x) p)