algebraMap_toAlgHom — Mathlib

English

For a hom f, and any x in the R-ring, aeval on the target equals the algebra map lifting of aeval on the source; i.e., aeval_{P′}(f.x) = algebraMap_{S→S′}(aeval_P(x)).

Русский

Для гомоморфизма f верно, что aeval на целевом кольце равен отображению алгебраического отображения, поднимающему aeval с исходного кольца.

LaTeX

$$$\\forall x,\\ aeval_{P'.val}(f.x) = \\text{algebraMap}_{S S'}( aeval_P(x) )$$$

Lean4

@[simp]
theorem algebraMap_toAlgHom (f : Hom P P') (x) :
    MvPolynomial.aeval P'.val (f.toAlgHom x) = algebraMap S S' (MvPolynomial.aeval P.val x) :=
  by
  suffices
    ((MvPolynomial.aeval P'.val).restrictScalars R).comp f.toAlgHom =
      (IsScalarTower.toAlgHom R S S').comp (MvPolynomial.aeval P.val)
    from DFunLike.congr_fun this x
  apply MvPolynomial.algHom_ext
  intro i
  simp [Hom.toAlgHom]

Похожие утверждения