English
If there is an algebra equivalence h between localizations, then M-localization passes to P.
Русский
Если существует алгебровое эквивалентное отображение между локализациями, локализация M переносится на P.
LaTeX
$$$\\text{IsLocalization.isLocalization_of_algEquiv}(M,S,h) : \\IsLocalization M P$$$
Lean4
theorem isLocalization_of_algEquiv [Algebra R P] [IsLocalization M S] (h : S ≃ₐ[R] P) : IsLocalization M P :=
by
constructor
· intro y
convert (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom
exact (h.commutes y).symm
· intro y
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)
apply_fun (show S → P from h) at e
simp only [map_mul, h.apply_symm_apply, h.commutes] at e
exact ⟨⟨x, s⟩, e⟩
· intro x y
rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ← h.symm.commutes]
exact id
