English
Given a localization map f: S Localization N and a LocalizationMap k: T Localization Q with an isomorphism j: M ≃* P and H: S.map j = T, one obtains a canonical isomorphism between the localizations N and Q.
Русский
Пусть имеется локализационная карта f и локализационная карта k, связанные изоморфизмом между исходными моноидами; тогда локализации N и Q изоморфны через соответствующий канонический изоморфизм.
LaTeX
$$$\text{Given } f: S \to N,\ k: T \to Q,\ j: M \simeq* P,\ H: S.map\ j.toMonoidHom = T,\; N \cong Q.$$$
Lean4
/-- Given Localization maps `f : M →* N, k : P →* U` for Submonoids `S, T` respectively, an
isomorphism `j : M ≃* P` such that `j(S) = T` induces an isomorphism of localizations `N ≃* U`. -/
@[to_additive /-- Given Localization maps `f : M →+ N, k : P →+ U` for Submonoids `S, T` respectively, an
isomorphism `j : M ≃+ P` such that `j(S) = T` induces an isomorphism of localizations `N ≃+ U`. -/
]
noncomputable def mulEquivOfMulEquiv (k : LocalizationMap T Q) {j : M ≃* P} (H : S.map j.toMonoidHom = T) : N ≃* Q :=
f.mulEquivOfLocalizations <| k.ofMulEquivOfDom H
