Polynomial.aeval_algebraMap_apply
theorem Polynomial.aeval_algebraMap_apply :
∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B]
[inst_6 : IsScalarTower R A B] (x : A) (p : Polynomial R),
(Polynomial.aeval ((algebraMap A B) x)) p = (algebraMap A B) ((Polynomial.aeval x) p)
The theorem `Polynomial.aeval_algebraMap_apply` states that for any commutative semirings `R` and `A`, a semiring `B`, and any `x` in `A` and polynomial `p` over `R`, if `A` and `B` are `R`-algebras and `B` is an `A`-algebra with `R` being a scalar tower, then the `R`-algebra homomorphism of `p`, created by sending the variable in `p` to `x` mapped into `B`, is equal to the result of mapping the `R`-algebra homomorphism of `p` into `B`, where the homomorphism is created by sending the variable in `p` to `x`. This basically means that mapping `x` into `B` first and then applying the homomorphism is the same as applying the homomorphism first and then mapping the result into `B`.
More concisely: For any commutative semirings R, A, and B, given an R-algebra homomorphism from R[x] to B, an R-algebra homomorphism from A to B, and an element x in A, if R is a scalar tower in B and A is an R-algebra, then evaluating p(x) in B via the homomorphism from A is equivalent to applying the homomorphism from R[x] to B to the polynomial p and then evaluating at x.
|
Polynomial.aeval_map_algebraMap
theorem Polynomial.aeval_map_algebraMap :
∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B]
[inst_6 : IsScalarTower R A B] (x : B) (p : Polynomial R),
(Polynomial.aeval x) (Polynomial.map (algebraMap R A) p) = (Polynomial.aeval x) p
This theorem, `Polynomial.aeval_map_algebraMap`, states that for any commutative semirings `R` and `A`, a semiring `B`, and given the algebra structures over them, if there is a scalar tower of `R`, `A`, and `B`, then for any element `x` of `B` and any polynomial `p` with coefficients in `R`, applying the algebra homomorphism `Polynomial.aeval x` to the polynomial obtained by mapping `p` across the ring homomorphism `algebraMap R A` is exactly the same as applying `Polynomial.aeval x` directly to `p`. This means that the process of mapping the polynomial `p` across the algebra map does not change the result when the polynomial is evaluated at `x` in the algebra structure.
More concisely: For any commutative semirings R, A, and B, and given algebra structures over them with a scalar tower, the application of the algebra homomorphism Polynomial.aeval to a polynomial obtained by mapping across the ring homomorphism algebraMap is equal to directly applying Polynomial.aeval to the polynomial.
|