mapOrderEmbedding — Mathlib

English

There is an order-embedding from LieSubmodule(R,L,M) to LieSubmodule(R,L,M') induced by an injective Lie module hom f.

Русский

Существует вложение по порядку между подмодулями Ли, порождённое инъективным гомоморфизмом f.

LaTeX

$$$ \text{mapOrderEmbedding } f\;:\; LieSubmodule(R,L,M) \hookrightarrow_o LieSubmodule(R,L,M') $$$

Lean4

/-- An injective morphism of Lie modules embeds the lattice of submodules of the domain into that
of the target. -/
@[simps]
def mapOrderEmbedding {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective f) : LieSubmodule R L M ↪o LieSubmodule R L M'
    where
  toFun := LieSubmodule.map f
  inj' := map_injective_of_injective hf
  map_rel_iff' := Set.image_subset_image_iff hf

Похожие утверждения