lieSubmoduleInvariant — Mathlib

English

Definition of the natural invariant map from L to endomorphisms of the quotient respecting the submodule structure.

Русский

Определение естественной инвариантной карты от $L$ к концевым отображениям фактор-модуля, сохраняющей подмодуль.

LaTeX

$$$\\text{lieSubmoduleInvariant}: L \\to\\_R \\mathrm{End}(M/N)$$$

Lean4

/-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
is a natural linear map from `L` to the endomorphisms of `M` leaving `N` invariant. -/
def lieSubmoduleInvariant : L →ₗ[R] Submodule.compatibleMaps N.toSubmodule N.toSubmodule :=
  LinearMap.codRestrict _ (LieModule.toEnd R L M) fun _ _ => N.lie_mem

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