orderIsoOfPrime — Mathlib

English

The prime ideals in localization S are in order-preserving bijection with prime ideals of R contained in I.

Русский

Простые идеалы локализации S соответствуют по порядку простым идеалам R, содержащимся в I.

LaTeX

$$$$ \text{orderIsoOfPrime} : { p \in {\text{PrimeIdeals}}(S) } \cong_o { p \in {\text{PrimeIdeals}}(R) \mid p \le I } $$$$

Lean4

/-- The prime ideals in the localization of a commutative ring at a prime ideal I are in
order-preserving bijection with the prime ideals contained in I. -/
@[simps!]
def orderIsoOfPrime : { p : Ideal S // p.IsPrime } ≃o { p : Ideal R // p.IsPrime ∧ p ≤ I } :=
  (IsLocalization.orderIsoOfPrime I.primeCompl S).trans <|
    .setCongr _ _ <| show setOf _ = setOf _ by ext; simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left]

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