English
There is a Lie algebra morphism from L to the endomorphisms of the quotient M/N, given by the action of L on M factored through N.
Русский
Существует хомоморфизм Ли-алгебры \(L\) в множество концевых отображений \(M/N\), задаваемый действием Ли на \(M\) по факторизации через \(N\).
LaTeX
$$def actionAsEndoMap : L →ₗ⁅R⁆ Module.End R (M ⧸ N)$$
Lean4
/-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
is a natural Lie algebra morphism from `L` to the linear endomorphism of the quotient `M/N`. -/
def actionAsEndoMap : L →ₗ⁅R⁆ Module.End R (M ⧸ N) :=
{ LinearMap.comp (Submodule.mapQLinear (N : Submodule R M) (N : Submodule R M)) lieSubmoduleInvariant with
map_lie' := fun {_ _} => Submodule.linearMap_qext _ <| LinearMap.ext fun _ => congr_arg mk <| lie_lie _ _ _ }
