English
An equivalence of Lie modules yields an order-preserving equivalence of their lattices of Lie submodules.
Русский
Эквивалентность Ли-модулей порождает упорядоченное эквивалентное соответствие их решёток Ли-подмодулей.
LaTeX
$$$ \text{orderIsoMapComap}(e) : LieSubmodule(R,L,M) \simeq_o LieSubmodule(R,L,M') $$$
Lean4
/-- An equivalence of Lie modules yields an order-preserving equivalence of their lattices of Lie
Submodules. -/
@[simps]
def orderIsoMapComap (e : M ≃ₗ⁅R,L⁆ M') : LieSubmodule R L M ≃o LieSubmodule R L M'
where
toFun := map e
invFun := comap e
left_inv := fun N ↦ by ext; simp
right_inv := fun N ↦ by ext; simp [e.apply_eq_iff_eq_symm_apply]
map_rel_iff' := fun {_ _} ↦ Set.image_subset_image_iff e.injective
