English
Let I ⊆ R and J ⊆ P be prime ideals with I = J ∘ f (pullback along a ring map f: R → P). Then the local ring homomorphism coming from localizing at I and J sends the canonical element associated to x ∈ R and y ∈ I-prime-complement to the canonical element at J given by f(x) and a corresponding y-image, i.e., the localization data are compatible with the map f.
Русский
Пусть I ⊆ R и J ⊆ P — ответвления простых идеалов, удовлетворяющие I = J·f, где f: R → P. Тогда локальный кольцевой гомоморфизм, полученный при локализации по I и J, отправляет элемент mk' _ x y локализации в элемент mk'(Localization.AtPrime J) (f x) ⟨f y, доказательство⟩ локализации J, т. е. локализационные данные согласованы с отображением f.
LaTeX
$$$\text{Localization.localRingHom } I\ J\ f\ hIJ\ (\IsLocalization.mk'\ _ x\ y) = \IsLocalization.mk' (Localization.AtPrime J) (f\,x) ⟨f\,y, le_comap_primeCompl_iff.mpr (ge_of_eq hIJ)\, y.2⟩$$$
Lean4
theorem localRingHom_mk' (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = J.comap f) (x : R) (y : I.primeCompl) :
localRingHom I J f hIJ (IsLocalization.mk' _ x y) =
IsLocalization.mk' (Localization.AtPrime J) (f x)
(⟨f y, le_comap_primeCompl_iff.mpr (ge_of_eq hIJ) y.2⟩ : J.primeCompl) :=
map_mk' _ _ _
