Mathlib.RingTheory.MvPolynomial.Tower

Module docstring

{"# 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. "}

MvPolynomial.aeval_map_algebraMap theorem

(x : σ → B) (p : MvPolynomial σ R) : aeval x (map (algebraMap R A) p) = aeval x p

Full source

theorem aeval_map_algebraMap (x : σ → B) (p : MvPolynomial σ R) :
    aeval x (map (algebraMap R A) p) = aeval x p := by
  rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

Evaluation Invariance under Polynomial Map via Algebra Homomorphism

Informal description

Let $R$, $A$, and $B$ be commutative rings with algebra homomorphisms $R \to A \to B$. For any polynomial $p \in \mathrm{MvPolynomial}(\sigma, R)$ and any evaluation map $x : \sigma \to B$, the evaluation of the polynomial $\mathrm{map}(\mathrm{algebraMap}_{R,A})(p)$ under $x$ equals the evaluation of $p$ under $x$. In other words: \[ \mathrm{aeval}(x)(\mathrm{map}(\mathrm{algebraMap}_{R,A})(p)) = \mathrm{aeval}(x)(p) \]

MvPolynomial.aeval_algebraMap_apply theorem

(x : σ → A) (p : MvPolynomial σ R) : aeval (algebraMap A B ∘ x) p = algebraMap A B (MvPolynomial.aeval x p)

Full source

theorem aeval_algebraMap_apply (x : σ → A) (p : MvPolynomial σ R) :
    aeval (algebraMapalgebraMap A B ∘ x) p = algebraMap A B (MvPolynomial.aeval x p) := by
  rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq]
  -- Porting note: added
  simp only [Function.comp_def]

Compatibility of Multivariate Polynomial Evaluation with Algebra Maps

Informal description

Let $R$, $A$, and $B$ be commutative rings with $R \to A \to B$ algebra homomorphisms. For any polynomial $p \in \mathrm{MvPolynomial}(\sigma, R)$ and any evaluation map $x : \sigma \to A$, the evaluation of $p$ under the composed map $\mathrm{algebraMap}_{A,B} \circ x$ equals the image under $\mathrm{algebraMap}_{A,B}$ of the evaluation of $p$ under $x$. In other words: \[ \mathrm{aeval}(\mathrm{algebraMap}_{A,B} \circ x)(p) = \mathrm{algebraMap}_{A,B}(\mathrm{aeval}(x)(p)) \]

MvPolynomial.aeval_algebraMap_eq_zero_iff theorem

 [NoZeroSMulDivisors A B] [Nontrivial B] (x : σ → A) (p : MvPolynomial σ R) :
  aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0

Full source

theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : σ → A)
    (p : MvPolynomial σ R) : aevalaeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0 := by
  rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]

Zero Evaluation Criterion for Multivariate Polynomials via Algebra Maps with No Zero Divisors

Informal description

Let $R$, $A$, and $B$ be commutative rings with algebra homomorphisms $R \to A \to B$, where $B$ is a nontrivial ring and $A \to B$ has no zero divisors under scalar multiplication. For any polynomial $p \in \mathrm{MvPolynomial}(\sigma, R)$ and any evaluation map $x : \sigma \to A$, the evaluation of $p$ under the composed map $\mathrm{algebraMap}_{A,B} \circ x$ equals zero if and only if the evaluation of $p$ under $x$ equals zero. In other words: \[ \mathrm{aeval}(\mathrm{algebraMap}_{A,B} \circ x)(p) = 0 \leftrightarrow \mathrm{aeval}(x)(p) = 0 \]

MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective theorem

 {x : σ → A} {p : MvPolynomial σ R} (h : Function.Injective (algebraMap A B)) :
  aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0

Full source

theorem aeval_algebraMap_eq_zero_iff_of_injective {x : σ → A} {p : MvPolynomial σ R}
    (h : Function.Injective (algebraMap A B)) :
    aevalaeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0 := by
  rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Injectivity Criterion for Multivariate Polynomial Evaluation via Algebra Maps

Informal description

Let $R$, $A$, and $B$ be commutative rings with algebra homomorphisms $R \to A \to B$, and let $\mathrm{algebraMap}_{A,B}: A \to B$ be injective. For any polynomial $p \in \mathrm{MvPolynomial}(\sigma, R)$ and any evaluation map $x : \sigma \to A$, the evaluation of $p$ under the composed map $\mathrm{algebraMap}_{A,B} \circ x$ equals zero if and only if the evaluation of $p$ under $x$ equals zero. In other words: \[ \mathrm{aeval}(\mathrm{algebraMap}_{A,B} \circ x)(p) = 0 \leftrightarrow \mathrm{aeval}(x)(p) = 0 \]

Subalgebra.mvPolynomial_aeval_coe theorem

(S : Subalgebra R A) (x : σ → S) (p : MvPolynomial σ R) : aeval (fun i => (x i : A)) p = aeval x p

Full source

@[simp]
theorem mvPolynomial_aeval_coe (S : Subalgebra R A) (x : σ → S) (p : MvPolynomial σ R) :
    aeval (fun i => (x i : A)) p = aeval x p := by convert aeval_algebraMap_apply A x p

Subalgebra Evaluation Consistency for Multivariate Polynomials

Informal description

Let $R$ and $A$ be commutative rings with an algebra homomorphism $R \to A$, and let $S$ be a subalgebra of $A$ over $R$. For any polynomial $p \in \mathrm{MvPolynomial}(\sigma, R)$ and any evaluation map $x : \sigma \to S$, the evaluation of $p$ under the map obtained by composing $x$ with the inclusion $S \hookrightarrow A$ equals the evaluation of $p$ under $x$ itself. In other words: \[ \mathrm{aeval}(\lambda i, (x(i) : A))(p) = \mathrm{aeval}(x)(p) \]