localization_specComap_range — Mathlib

English

Let M be a submonoid and S a localization of R at M. The range of comap (algebraMap R S) consists exactly of prime ideals disjoint from M.

Русский

Пусть M — подмножество и S — локализация R по M. Образ comap (algebraMap R S) состоит ровно из простых идеалов, дисjointных с M.

LaTeX

$$Set.range (comap (algebraMap R S)) = {p | Disjoint (M : Set R) p.asIdeal}.$$

Lean4

theorem localization_specComap_range [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    Set.range (algebraMap R S).specComap = {p | Disjoint (M : Set R) p.asIdeal} :=
  by
  refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨p, rfl⟩
    exact ((IsLocalization.isPrime_iff_isPrime_disjoint ..).mp p.2).2
  · use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
    ext1
    exact IsLocalization.comap_map_of_isPrime_disjoint M S _ x.2 h

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