Algebra towers for multivariate polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

This structure itself is provided elsewhere as mv_polynomial.is_scalar_tower

When you update this file, you can also try to make a corresponding update in ring_theory.polynomial.tower.

theorem mv_polynomial.aeval_map_algebra_map {R : Type u_1} (A : Type u_2) {B : Type u_3} {σ : Type u_4} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] (x : σ → B) (p : mv_polynomial σ R) :

theorem mv_polynomial.aeval_algebra_map_apply {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] (x : σ → A) (p : mv_polynomial σ R) :

theorem mv_polynomial.aeval_algebra_map_eq_zero_iff {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] [no_zero_smul_divisors A B] [nontrivial B] (x : σ → A) (p : mv_polynomial σ R) :

theorem mv_polynomial.aeval_algebra_map_eq_zero_iff_of_injective {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] {x : σ → A} {p : mv_polynomial σ R} (h : function.injective ⇑(algebra_map A B)) :

@[simp]

theorem subalgebra.mv_polynomial_aeval_coe {R : Type u_1} {A : Type u_2} {σ : Type u_4} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) (x : σ → ↥S) (p : mv_polynomial σ R) :