localizationLocalizationAtPrimeIsoLocalization

English

There is a canonical algebra structure on Localization.AtPrime p as an R-algebra over Localization (nonZeroDivisors R) obtained via a localization of a submonoid, i.e., Localization.AtPrime p ≃ₐ[R] Localization (nonZeroDivisors R).

Русский

Существует каноническая структура алгебры на Localization.AtPrime p как R-алгебра на Localization (nonZeroDivisors R).

LaTeX

$$IsLocalization (Localization AtPrime p) (Localization (nonZeroDivisors R))$$

Lean4

/-- Given a submodule `M ⊆ R` and a prime ideal `p` of `M⁻¹R`, with `f : R →+* S` the localization
map, then `(M⁻¹R)ₚ` is isomorphic (as an `R`-algebra) to the localization of `R` at `f⁻¹(p)`.
-/
noncomputable def localizationLocalizationAtPrimeIsoLocalization (p : Ideal (Localization M)) [p.IsPrime] :
    Localization.AtPrime (p.comap (algebraMap R (Localization M))) ≃ₐ[R] Localization.AtPrime p :=
  IsLocalization.algEquiv (p.comap (algebraMap R (Localization M))).primeCompl _ _

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