instHasQuotient — Mathlib

English

Let M be a Lie module over a Lie algebra L in the setting of a commutative ring R, and let N be a Lie submodule of M. Then the quotient M/N naturally carries a Lie module structure over L obtained by passing the L-action to cosets.

Русский

Пусть M является представлением Ли-алгебры L над кольцом R и N — Ли-подмодуль M. Тогда фактор-пространство M/N естественно о́бладает структурой модуля Ли над L, полученной по переходу действия Ли на косеты.

LaTeX

$$$M/N$ is a Lie $L$-module.$$

Lean4

/-- The quotient of a Lie module by a Lie submodule. It is a Lie module. -/
instance : HasQuotient M (LieSubmodule R L M) :=
  ⟨fun N => M ⧸ N.toSubmodule⟩

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