restrictLie — Mathlib

English

The map from LieSubalgebra to Submodule is injective.

Русский

Отображение подалгебры в подподмножество инъективно.

LaTeX

$$$$\forall {R} {L} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L],\ \text{Function.Injective} (\uparrow) : \text{LieSubalgebra } R L \to \text{Submodule } R L.$$$$

Lean4

/-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra
`L' ⊆ L`. -/
def _root_.LieModuleHom.restrictLie (f : M →ₗ⁅R,L⁆ N) (L' : LieSubalgebra R L) : M →ₗ⁅R,L'⁆ N :=
  { (f : M →ₗ[R] N) with map_lie' := @fun x m ↦ f.map_lie (↑x) m }

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