toSubmodule_orderEmbedding — Mathlib

English

There is a natural order-embedding from Lie submodules of M to submodules of M given by forgetting the L-action.

Русский

Существует естественное вложение порядков из Ли-подмódулей M в подмодули M, забывающее действие L.

LaTeX

$$toSubmodule_orderEmbedding : LieSubmodule R L M \\hookrightarrow o Submodule R M$$

Lean4

/-- The natural functor that forgets the action of `L` as an order embedding. -/
@[simps]
def toSubmodule_orderEmbedding : LieSubmodule R L M ↪o Submodule R M :=
  { toFun := (↑)
    inj' := toSubmodule_injective
    map_rel_iff' := Iff.rfl }

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