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 : σ → ↥S)
(p : MvPolynomial σ R)
:
(MvPolynomial.aeval fun (i : σ) => ↑(x i)) p = ↑((MvPolynomial.aeval x) p)