English
Let f: R → S be the localization map for M ⊆ R and g: R → P a ring homomorphism with g(y) invertible for all y ∈ M. If f(x) = f(y) in S, then g(x) = g(y) in P.
Русский
Пусть f: R → S — локализационное отображение по M ⊆ R и g: R → P — кольцевой гомоморфизм с обратимыми элементами g(y) для всех y ∈ M. Если f(x) = f(y) в S, то g(x) = g(y) в P.
LaTeX
$$$ \\forall x,y \\in R, \\ (f(x) = f(y)) \\Rightarrow (g(x) = g(y)), \\quad \\text{где } f = \\mathrm{algebraMap}_{R,S}. $$$
Lean4
/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →+* P` such that `g(M) ⊆ Units P`, `f x = f y → g x = g y` for all `x y : R`. -/
theorem eq_of_eq {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) {x y} (h : (algebraMap R S) x = (algebraMap R S) y) :
g x = g y :=
Submonoid.LocalizationMap.eq_of_eq (toLocalizationMap M S) (g := g.toMonoidHom) hg h
