mathlib documentation

algebra.lie.quotient

Quotients of Lie algebras and Lie modules #

Given a Lie submodule of a Lie module, the quotient carries a natural Lie module structure. In the special case that the Lie module is the Lie algebra itself via the adjoint action, the submodule is a Lie ideal and the quotient carries a natural Lie algebra structure.

We define these quotient structures here. A notable omission at the time of writing (February 2021) is a statement and proof of the universal property of these quotients.

Main definitions #

Tags #

lie algebra, quotient

def lie_submodule.quotient {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
Type w

The quotient of a Lie module by a Lie submodule. It is a Lie module.

def lie_submodule.quotient.mk {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N : lie_submodule R L M} :
M → N.quotient

Map sending an element of M to the corresponding element of M/N, when N is a lie_submodule of the lie_module N.

theorem lie_submodule.quotient.is_quotient_mk {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N : lie_submodule R L M} (m : M) :

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.

Equations
def lie_submodule.quotient.action_as_endo_map {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :

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.

Equations
def lie_submodule.quotient.action_as_endo_map_bracket {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :

Given a Lie module M over a Lie algebra L, together with a Lie submodule N ⊆ M, there is a natural bracket action of L on the quotient M/N.

Equations
@[instance]
def lie_submodule.quotient.lie_quotient_lie_module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :

The quotient of a Lie module by a Lie submodule, is a Lie module.

Equations
@[instance]
Equations
@[simp]
theorem lie_submodule.quotient.mk'_to_linear_map_apply {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (ᾰ : M) :
@[ext]
theorem lie_submodule.quotient.lie_module_hom_ext {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) ⦃f g : N.quotient →ₗ⁅R,L M⦄ (h : f.comp (lie_submodule.quotient.mk' N) = g.comp (lie_submodule.quotient.mk' N)) :
f = g

Two lie_module_homs from a quotient lie module are equal if their compositions with lie_submodule.quotient.mk' are equal.

See note [partially-applied ext lemmas].