English
If every y ∈ S maps to a unit under g and f x = f y, then g x = g y. Thus g respects the localization equivalence.
Русский
Если каждый y ∈ S отображается в единицу под=g и f x = f y, тогда g x = g y. Таким образом, g устойчива к эквивалентности локализации.
LaTeX
$$$\forall x,y,\ f(x)=f(y) \Rightarrow g(x)=g(y)\quad(\text{under } \forall y\in S: \ IsUnit(g(y)))$$$
Lean4
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g(S) ⊆ Units P`, `f x = f y → g x = g y` for all `x y : M`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g(S) ⊆ AddUnits P`, `f x = f y → g x = g y`
for all `x y : M`. -/
]
theorem eq_of_eq (hg : ∀ y : S, IsUnit (g y)) {x y} (h : f x = f y) : g x = g y :=
by
obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h
rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.restrict S) hg c]
change _ * g c * _ = _
rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
