isLocalization_iff_of_algEquiv — Mathlib

English

Let M be a submonoid of a commutative semiring R, and let S and P be commutative R-algebras. If S and P are isomorphic as R-algebras (via an algebra isomorphism h), then S is a localization of R at M if and only if P is a localization of R at M.

Русский

Пусть M — подмоноид кольца R, и пусть S и P — коммутативные алгебры над R. Если S и P изоморфны как R-алгебры (существует алгебраическое изоморождение h), то S является локализацией R по M тогда и только тогда, когда P является локализацией R по M.

LaTeX

$$$\operatorname{IsLocalization}(M,S) \iff \operatorname{IsLocalization}(M,P)$$$

Lean4

theorem isLocalization_iff_of_algEquiv [Algebra R P] (h : S ≃ₐ[R] P) : IsLocalization M S ↔ IsLocalization M P :=
  ⟨fun _ => isLocalization_of_algEquiv M h, fun _ => isLocalization_of_algEquiv M h.symm⟩

Похожие утверждения