isLocalization_atPrime_localization_atPrime

English

If p is a prime ideal of Localization M, then Localization.AtPrime p is an IsLocalization of the comap of p along algebraMap R S.

Русский

Если p — простая идеал локализации M, то Localization.AtPrime p является локализацией относительно p.comap(algebraMap).

LaTeX

$$IsLocalization.AtPrime (Localization.AtPrime p) (Ideal.comap (algebraMap R S) p)$$

Lean4

instance isLocalization_atPrime_localization_atPrime (p : Ideal (Localization M)) [p.IsPrime] :
    IsLocalization.AtPrime (Localization.AtPrime p) (p.comap (algebraMap R _)) :=
  isLocalization_isLocalization_atPrime_isLocalization M _ _

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