# mathlibdocumentation

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 #

• lie_submodule.quotient.lie_quotient_lie_module
• lie_submodule.quotient.lie_quotient_lie_algebra

## Tags #

lie algebra, quotient

@[protected, instance]
def lie_submodule.has_quotient {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
L M)

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

Equations
@[protected, instance]
def lie_submodule.quotient.add_comm_group {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} :
Equations
@[protected, instance]
def lie_submodule.quotient.module' {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} {S : Type u_1} [semiring S] [ R] [ M] [ M] :
(M N)
Equations
@[protected, instance]
def lie_submodule.quotient.module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} :
(M N)
Equations
@[protected, instance]
def lie_submodule.quotient.is_central_scalar {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} {S : Type u_1} [semiring S] [ R] [ M] [ M] [ R] [ M] [ M] [ M] :
(M N)
@[protected, instance]
def lie_submodule.quotient.inhabited {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} :
Equations
@[reducible]
def lie_submodule.quotient.mk {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} :
M → M N

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] [ L] [ M] [ M] [ L M] {N : M} (m : M) :
def lie_submodule.quotient.lie_submodule_invariant {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : 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] [ L] [ M] [ M] [ L M] (N : M) :
L →ₗ⁅R (M N)

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
@[protected, instance]
def lie_submodule.quotient.action_as_endo_map_bracket {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
(M N)

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
@[protected, instance]
def lie_submodule.quotient.lie_quotient_lie_ring_module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
(M N)
Equations
@[protected, instance]
def lie_submodule.quotient.lie_quotient_lie_module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
L (M N)

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

Equations
@[protected, instance]
def lie_submodule.quotient.lie_quotient_has_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} :
has_bracket (L I) (L I)
Equations
@[simp]
theorem lie_submodule.quotient.mk_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} (x y : L) :
@[protected, instance]
def lie_submodule.quotient.lie_quotient_lie_ring {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} :
Equations
@[protected, instance]
def lie_submodule.quotient.lie_quotient_lie_algebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} :
(L I)
Equations
def lie_submodule.quotient.mk' {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :

lie_submodule.quotient.mk as a lie_module_hom.

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] [ L] [ M] [ M] [ L M] (N : M) (ᾰ : M) :
@[simp]
theorem lie_submodule.quotient.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) {m : M} :
= 0 m N
@[simp]
theorem lie_submodule.quotient.mk'_ker {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
@[simp]
theorem lie_submodule.quotient.map_mk'_eq_bot_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : M) :
N' N
@[ext]
theorem lie_submodule.quotient.lie_module_hom_ext {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) ⦃f g : M N →ₗ⁅R,L M⦄ (h : = ) :
f = g

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

@[simp]
theorem lie_hom.quot_ker_equiv_range_to_lie_hom_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (ᾰ : L ) :
@[simp]
theorem lie_hom.quot_ker_equiv_range_inv_fun {R : Type u_1} {L : Type u_2} {L' : Type u_3} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (ᾰ : ) :
noncomputable def lie_hom.quot_ker_equiv_range {R : Type u_1} {L : Type u_2} {L' : Type u_3} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') :

The first isomorphism theorem for morphisms of Lie algebras.

Equations
@[simp]
theorem lie_hom.quot_ker_equiv_range_to_lie_hom_to_linear_map_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (ᾰ : L ) :