# Algebra towers for multivariate polynomial #

This file proves some basic results about the algebra tower structure for the type `MvPolynomial σ R`.

This structure itself is provided elsewhere as `MvPolynomial.isScalarTower`

When you update this file, you can also try to make a corresponding update in `RingTheory.Polynomial.Tower`.

source
theorem MvPolynomial.aeval_map_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : σ → B) (p : MvPolynomial σ R) :
(aeval x) ((map (algebraMap R A)) p) = (aeval x) p
source
theorem MvPolynomial.aeval_algebraMap_apply {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : σ → A) (p : MvPolynomial σ R) :
(aeval (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((aeval x) p)
source
@[simp]
theorem MvPolynomial.aeval_C_comp_left {R : Type u_1} {A : Type u_2} {σ : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_5} (f : σ → A) (p : MvPolynomial σ R) :
(aeval (⇑C ∘ f)) p = C ((aeval f) p)
source
theorem MvPolynomial.aeval_algebraMap_eq_zero_iff {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [NoZeroSMulDivisors A B] [Nontrivial B] (x : σ → A) (p : MvPolynomial σ R) :
(aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0
source
theorem MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : σ → A} {p : MvPolynomial σ R} (h : Function.Injective ⇑(algebraMap A B)) :
(aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0
source
@[simp]
theorem Subalgebra.mvPolynomial_aeval_coe {R : Type u_1} {A : Type u_2} {σ : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (x : σ → ↥S) (p : MvPolynomial σ R) :
(MvPolynomial.aeval fun (i : σ) => ↑(x i)) p = ↑((MvPolynomial.aeval x) p)