English
Let R be a commutative semiring, M a submonoid, S a commutative semiring with R-algebra structure, and S a localization of R at M. For any ideal I of R, the image of I under the localization map is proper (not the whole ring) if and only if I is disjoint from M as a subset of R.
Русский
Пусть R — коммутативная полугруппа, M подмоной, S коммутативная полугруппа с структурой алгебры над R, и S — локализация R по M. Для любого идеала I в R образ I в S через локализационную карту является proper тогда и только если I не пересекается с M как подмножество R.
LaTeX
$$$ I.map(\\mathrm{algebraMap}\\;R\\;S) \\neq \\top \\;\\Longleftrightarrow\\; \\operatorname{Disjoint}(M:\\mathrm{Set}R)(I:\\mathrm{Set}R) $$$
Lean4
theorem map_algebraMap_ne_top_iff_disjoint (I : Ideal R) :
I.map (algebraMap R S) ≠ ⊤ ↔ Disjoint (M : Set R) (I : Set R) :=
by
simp only [ne_eq, Ideal.eq_top_iff_one, ← map_one (algebraMap R S), not_iff_comm,
IsLocalization.algebraMap_mem_map_algebraMap_iff M]
simp [Set.disjoint_left]
