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.
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)
:
↑(MvPolynomial.aeval x) (↑(MvPolynomial.map (algebraMap R A)) p) = ↑(MvPolynomial.aeval x) p
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)
:
↑(MvPolynomial.aeval (↑(algebraMap A B) ∘ x)) p = ↑(algebraMap A B) (↑(MvPolynomial.aeval x) p)
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)
:
↑(MvPolynomial.aeval (↑(algebraMap A B) ∘ x)) p = 0 ↔ ↑(MvPolynomial.aeval x) p = 0
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))
:
↑(MvPolynomial.aeval (↑(algebraMap A B) ∘ x)) p = 0 ↔ ↑(MvPolynomial.aeval x) p = 0
@[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 : σ → { x // x ∈ S })
(p : MvPolynomial σ R)
:
↑(MvPolynomial.aeval fun i => ↑(x i)) p = ↑(↑(MvPolynomial.aeval x) p)