English
There is an order-embedding of ideals from the localization S into ideals of R given by comap along the localization map; this embedding is compatible with the order and is a left inverse to map_comap.
Русский
Существуют вложения по порядку между множествами идеалов локализации S в идеалы R через comap вдоль локализационной карты; это вложение сохраняет порядок и является левым обратным к map_comap.
LaTeX
$$$\\text{orderEmbedding}: \\mathrm{Ideal}S \\hookrightarrow_o \\mathrm{Ideal}R,\\; J \\mapsto \\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;S)\\,J,\\quad \\text{inj'},\\; \\text{map_rel_iff}'$$$
Lean4
/-- If `S` is the localization of `R` at a submonoid, the ordering of ideals of `S` is
embedded in the ordering of ideals of `R`. -/
def orderEmbedding : Ideal S ↪o Ideal R
where
toFun J := Ideal.comap (algebraMap R S) J
inj' := Function.LeftInverse.injective (map_comap M S)
map_rel_iff' := by
rintro J₁ J₂
constructor
· exact fun hJ => (map_comap M S) J₁ ▸ (map_comap M S) J₂ ▸ Ideal.map_mono hJ
· exact fun hJ => Ideal.comap_mono hJ
