English
Compatibility of evaluation of polynomials with the equivalence; C-coercions align under the isomorphism.
Русский
Совместимость вычисления полиномов с эквивалентностью; константы C согласованы через изоморфизм.
LaTeX
$$$\text{aeval}$-compatibility with mvPolynomialOptionEquivPolynomialAdjoin_C: the C-maps match under the isomorphism.$$
Lean4
theorem aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin (hx : AlgebraicIndependent R x) (a : A) :
RingHom.comp
(↑(Polynomial.aeval a : Polynomial (adjoin R (Set.range x)) →ₐ[_] A) :
Polynomial (adjoin R (Set.range x)) →+* A)
hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom =
↑(MvPolynomial.aeval fun o : Option ι => o.elim a x : MvPolynomial (Option ι) R →ₐ[R] A) :=
by
refine MvPolynomial.ringHom_ext ?_ ?_ <;>
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, AlgHom.coe_toRingHom,
AlgHom.coe_toRingHom]
· intro r
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
· rintro (⟨⟩ | ⟨i⟩)
· rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X, Option.elim]
·
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C, hx.algebraMap_aevalEquiv, aeval_X,
aeval_X, Option.elim]
