isLocalization_iff_of_ringEquiv — Mathlib

English

Let h be a ring equivalence between two R-algebras S and P. Then IsLocalization M S holds if and only if IsLocalization M P holds, i.e., localization does not depend on the particular realization of the algebra.

Русский

Пусть h — кольцевое эквивалентность между двумя R-алгебрами S и P. Тогда IsLocalization M S выполняется тогда и только тогда, когда IsLocalization M P выполняется, то есть локализация не зависит от конкретного представления алгебры.

LaTeX

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

Lean4

theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) :
    IsLocalization M S ↔
      haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra;
      IsLocalization M P :=
  letI := (h.toRingHom.comp <| algebraMap R S).toAlgebra
  isLocalization_iff_of_algEquiv M { h with commutes' := fun _ => rfl }

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