English
The action of mapₐ on a algebra map f, element a ∈ A_p and x ∈ A_p is simply the induced map from f on the underlying ring maps: mapₐ A_p B_p f a x = map A_p B_p f.toRingHom a x.
Русский
Действие mapₐ на отображение алгебры f, элемент a ∈ A_p и x ∈ A_p совпадает с индуцированным отображением по f между соответствующими необработанными отображениями: mapₐ A_p B_p f a x = map A_p B_p f.toRingHom a x.
LaTeX
$$$\\operatorname{map}_{A_p,B_p,f}(a)(x) = (\\operatorname{map}_{R} f)(a) \\cdot x$$$
Lean4
/-- Given a algebra map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map
`Aₐ →ₐ[R] Bₐ`. -/
noncomputable def mapₐ (f : A →ₐ[R] B) (a : A) [Away a Aₚ] [Away (f a) Bₚ] : Aₚ →ₐ[R] Bₚ :=
⟨map Aₚ Bₚ f.toRingHom a, fun r ↦
by
dsimp only [AlgHom.toRingHom_eq_coe, map, RingHom.coe_coe, OneHom.toFun_eq_coe]
rw [IsScalarTower.algebraMap_apply R A Aₚ, IsScalarTower.algebraMap_eq R B Bₚ]
simp⟩
