mapₐ_apply — Mathlib

English

The proof that mapₐ respects the base maps and the localization structure; i.e., mapₐ is well-defined and compatible with algebra maps.

Русский

Доказывается, что mapₐ корректен и совместим с базовыми отображениями и структурой локализации.

LaTeX

$$$\\text{map}_{A_p,B_p,f}(a)\\circ \\text{algebraMap}_{R,A_p} = \\text{algebraMap}_{R,B_p} \\circ f$$$

Lean4

@[simp]
theorem mapₐ_apply (f : A →ₐ[R] B) (a : A) [Away a Aₚ] [Away (f a) Bₚ] (x : Aₚ) :
    mapₐ Aₚ Bₚ f a x = map Aₚ Bₚ f.toRingHom a x :=
  rfl

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