English
An isomorphism j: R ≃+* P carrying M to T induces an isomorphism of localizations S ≃+* Q, provided the corresponding compatibility condition on submonoids holds.
Русский
Изоморфизм j: R ≃+* P, переводящий M в T, порождает изоморфизм локализаций S ≃+* Q при условии совместимости подмножест, указанного выше.
LaTeX
$$$$ \\text{IsLocalization}(M, S) \\implies \\text{IsLocalization}(M^g, S) \\text{ via } j $$$$
Lean4
/-- If `S`, `Q` are localizations of `R` and `P` at submonoids `M, T` respectively, an
isomorphism `j : R ≃+* P` such that `j(M) = T` induces an isomorphism of localizations
`S ≃+* Q`. -/
@[simps]
noncomputable def ringEquivOfRingEquiv (h : R ≃+* P) (H : M.map h.toMonoidHom = T) : S ≃+* Q :=
have H' : T.map h.symm.toMonoidHom = M :=
by
rw [← M.map_id, ← H, Submonoid.map_map]
congr
ext
apply h.symm_apply_apply
{
map Q (h : R →+* P)
(M.le_comap_of_map_le
(le_of_eq H)) with
toFun := map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H))
invFun := map S (h.symm : P →+* R) (T.le_comap_of_map_le (le_of_eq H'))
left_inv := fun x => by
rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
simp
right_inv := fun x => by
rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
simp }
