English
A prime ideal J of S corresponds to a pair consisting of the comap in R being prime and disjoint from M; equivalence with the original prime property.
Русский
Простой идеал J в S соответствует паре: комап в R является простым и Disjoint(M, comap J); и наоборот.
LaTeX
$$$J.IsPrime \\iff (\\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;S)J).IsPrime \\land \\operatorname{Disjoint}(M:\\mathrm{Set}R)\\, (\\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;S)J)$$$
Lean4
/-- If `R` is a ring, then prime ideals in the localization at `M`
correspond to prime ideals in the original ring `R` that are disjoint from `M`.
This lemma gives the particular case for an ideal and its comap,
see `le_rel_iso_of_prime` for the more general relation isomorphism -/
theorem isPrime_iff_isPrime_disjoint (J : Ideal S) :
J.IsPrime ↔ (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint (M : Set R) ↑(Ideal.comap (algebraMap R S) J) :=
by
constructor
· refine fun h =>
⟨⟨?_, ?_⟩,
Set.disjoint_left.mpr fun m hm1 hm2 => h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
· refine fun hJ => h.ne_top ?_
rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
exact le_of_eq hJ.symm
· intro x y hxy
rw [Ideal.mem_comap, RingHom.map_mul] at hxy
exact h.mem_or_mem hxy
· refine fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩
· rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ
· intro x y hxy
obtain ⟨a, s, ha⟩ := mk'_surjective M x
obtain ⟨b, t, hb⟩ := mk'_surjective M y
have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
rw [mk'_mem_iff, ← Ideal.mem_comap] at this
have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
rw [Ideal.mem_comap, Ideal.mem_comap] at this₂
rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]
