isLocalization_isLocalization_atPrime_isLocalization

English

Let p be a prime ideal of S, and assume T is the localization of S at p. Then T viewed as an R-algebra localized at p.comap(algebraMap R S) is a localization: i.e. AtPrime p is a localization of R via the comap.

Русский

Пусть p — простая идеал в S, и T — локализация S по p. Тогда T, как алгебра R, локализуется по p.comap(algebraMap R S); т.е. AtPrime p является локализацией R.

LaTeX

$$$IsLocalization\AtPrime p \text{ over } R \text{ with respect to } p^{\mathrm{comap}}(algebraMap\ R\ S).$$$

Lean4

/-- Given a submodule `M ⊆ R` and a prime ideal `p` of `S = M⁻¹R`, with `f : R →+* S` the localization
map, then `T = Sₚ` is the localization of `R` at `f⁻¹(p)`.
-/
theorem isLocalization_isLocalization_atPrime_isLocalization (p : Ideal S) [Hp : p.IsPrime]
    [IsLocalization.AtPrime T p] : IsLocalization.AtPrime T (p.comap (algebraMap R S)) :=
  by
  apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T
  intro x hx hx'
  exact (Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)

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