English
The ordering on submodules of the quotient M/p embeds into the ordering on submodules of M via comap along mkQ.
Русский
Порядок подмодулей фактор‑модуля M/p вклинивается в порядок подмодулей M через обратное образование mkQ.
LaTeX
$$$$ \\text{comapMkQOrderEmbedding} : Submodule R (M ⧸ p) \\hookrightarrow Submodule R M. $$$$
Lean4
/-- The correspondence theorem for modules: there is an order isomorphism between submodules of the
quotient of `M` by `p`, and submodules of `M` larger than `p`. -/
def comapMkQRelIso : Submodule R (M ⧸ p) ≃o Set.Ici p
where
toFun p' := ⟨comap p.mkQ p', le_comap_mkQ p _⟩
invFun q := map p.mkQ q
left_inv p' := map_comap_eq_self <| by simp
right_inv := fun ⟨q, hq⟩ => Subtype.ext <| by simpa [comap_map_mkQ p]
map_rel_iff' := comap_le_comap_iff <| range_mkQ _
