English
Define a local ring hom from Localization.AtPrime I to Localization.AtPrime J for a suitable f and hIJ; this map is induced by f and respects the localization structure.
Русский
Определим локальный окружной однородный гомоморфизм от Localization.AtPrime I к Localization.AtPrime J для подходящего отображения f и hIJ; отображение индуцировано f и сохраняет структуру локализации.
LaTeX
$$$$ \text{Localization.localRingHom } I\ J\ f\ hIJ $$$$
Lean4
/-- For a ring hom `f : R →+* S` and a prime ideal `J` in `S`, the induced ring hom from the
localization of `R` at `J.comap f` to the localization of `S` at `J`.
To make this definition more flexible, we allow any ideal `I` of `R` as input, together with a proof
that `I = J.comap f`. This can be useful when `I` is not definitionally equal to `J.comap f`.
-/
noncomputable def localRingHom (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = J.comap f) :
Localization.AtPrime I →+* Localization.AtPrime J :=
IsLocalization.map (Localization.AtPrime J) f (le_comap_primeCompl_iff.mpr (ge_of_eq hIJ))
