isPrime_map_of_isLocalizationAtPrime

English

If p ⊆ q with q prime and p prime in R, then the extension p.map(algebraMap R S) is a prime ideal of S when S is localized at q.

Русский

Если p ⊆ q, причем q прост, и p прост в R, то образ p под алгебраическим отображением R → S является простым идеалом в S при локализации по q.

LaTeX

$$(p.map (algebraMap R S)).IsPrime$$

Lean4

theorem isPrime_map_of_isLocalizationAtPrime {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) :
    (p.map (algebraMap R S)).IsPrime :=
  by
  have disj : Disjoint (q.primeCompl : Set R) p := by simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]
  apply IsLocalization.isPrime_of_isPrime_disjoint q.primeCompl _ p (by simpa) disj

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