English
The canonical localization-aware algebra homomorphism compLocalizationAwayAlgHom, when evaluated on the X-variables and the localization coordinate, coincides with the explicit evaluation mapping given by toComp and the algebraMap into the localization, i.e., it reproduces the expected algebra map after localization.
Русский
Каноническое отображение compLocalizationAwayAlgHom, учитывающее локализацию, на X-переменные и координату локализации совпадает с явным отображением через toComp и алгебраическое вложение в локализацию, т.е. восстанавливает ожидаемую карту после локализации.
LaTeX
$$$compLocalizationAwayAlgHom\\ T\\ g\\ P\\ (((localizationAway T g).toComp P).toAlgHom x) = algebraMap P.Ring _ x$$$
Lean4
@[simp]
theorem compLocalizationAwayAlgHom_toAlgHom_toComp (x : P.Ring) :
compLocalizationAwayAlgHom T g P (((localizationAway T g).toComp P).toAlgHom x) = algebraMap P.Ring _ x := by
simp only [toComp_toAlgHom, compLocalizationAwayAlgHom, comp, localizationAway, AlgHom.toRingHom_eq_coe, aeval_rename,
Sum.elim_comp_inr, ← IsScalarTower.toAlgHom_apply (R := R), ← comp_aeval_apply, aeval_X_left_apply]
