English
If R is a domain and M is contained in the non-zero divisors, then the comap of any prime ideal p of S is strictly larger than the bottom ideal in R.
Русский
Если R — область и M вложено в множества без делителей нуля, то comap(prime p) больше нижнего градиента.
LaTeX
$$$\\bot < \\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;S)\\;p$$$
Lean4
theorem bot_lt_comap_prime [IsDomain R] (hM : M ≤ R⁰) (p : Ideal S) [hpp : p.IsPrime] (hp0 : p ≠ ⊥) :
⊥ < Ideal.comap (algebraMap R S) p :=
by
haveI : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM
rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]
convert
(orderIsoOfPrime M S).lt_iff_lt.mpr
(show (⟨⊥, Ideal.bot_prime⟩ : { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)
