English
If I is a prime ideal of R and I is disjoint from M, then comap(algebraMap R S) (map(algebraMap R S) I) equals I.
Русский
Пусть I — простый идеал R; если I дисjoint относительно M, тогда comap(algebraMap R S)(map(algebraMap R S) I)=I.
LaTeX
$$$I.IsPrime \\Rightarrow (\\operatorname{Disjoint}(M:\\mathrm{Set}R)(I:\\mathrm{Set}R)) \\rightarrow \\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;S)(\\operatorname{Ideal.map}(\\mathrm{algebraMap}\\;R\\;S) I)=I$$$
Lean4
theorem comap_map_of_isPrime_disjoint (I : Ideal R) (hI : I.IsPrime) (hM : Disjoint (M : Set R) I) :
Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I :=
by
refine le_antisymm ?_ Ideal.le_comap_map
refine (fun a ha => ?_)
obtain ⟨⟨b, s⟩, h⟩ := (mem_map_algebraMap_iff M S).1 (Ideal.mem_comap.1 ha)
replace h : algebraMap R S (s * a) = algebraMap R S b := by simpa only [← map_mul, mul_comm] using h
obtain ⟨c, hc⟩ := (eq_iff_exists M S).1 h
have : ↑c * ↑s * a ∈ I := by
rw [mul_assoc, hc]
exact I.mul_mem_left c b.2
exact (hI.mem_or_mem this).resolve_left fun hsc => hM.le_bot ⟨(c * s).2, hsc⟩
