English
Given a map f: R → P, a localization S away from r ∈ R, and a localization Q away from f(r) in P, there exists a localization map IsLocalization.Away.map: S → Q compatible with f.
Русский
Пусть есть отображение f: R → P, локализация S away от r ∈ R и локализация Q away от f(r) в P; тогда существует отображение локализации IsLocalization.Away.map: S → Q совместимое с f.
LaTeX
$$$\\text{IsLocalization.Away.map} (f,r): S \\to Q$ с условием совместимости с $f$$$
Lean4
/-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`. -/
noncomputable def map (f : R →+* P) (r : R) [IsLocalization.Away r S] [IsLocalization.Away (f r) Q] : S →+* Q :=
IsLocalization.map Q f
(show Submonoid.powers r ≤ (Submonoid.powers (f r)).comap f
by
rintro x ⟨n, rfl⟩
use n
simp)
