English
There is an order isomorphism between submodules of p and submodules of M contained in p.
Русский
Существует линеарно-упорядоченное изоморфизм между подмодулями p и подмодулями M, лежащими внутри p.
LaTeX
$$$$ \text{orderIso} : \text{Submodule }R p \cong_o \{ p' : \text{Submodule }R M \mid p' \le p \} $$$$
Lean4
/-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N`.
See also `Submodule.mapIic`. -/
def orderIso : Submodule R p ≃o { p' : Submodule R M // p' ≤ p }
where
toFun p' := ⟨map p.subtype p', map_subtype_le p _⟩
invFun q := comap p.subtype q
left_inv p' := comap_map_eq_of_injective (by exact Subtype.val_injective) p'
right_inv := fun ⟨q, hq⟩ => Subtype.ext <| by simp [map_comap_subtype p, inf_of_le_right hq]
map_rel_iff'
{p₁ p₂} :=
Subtype.coe_le_coe.symm.trans <| by
dsimp
rw [map_le_iff_le_comap, comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂]
