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 #

• LieSubmodule.Quotient.lieQuotientLieModule
• LieSubmodule.Quotient.lieQuotientLieAlgebra

Tags #

lie algebra, quotient

instance LieSubmodule.instHasQuotient {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] :

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

Equations
• LieSubmodule.instHasQuotient = { quotient' := fun (N : LieSubmodule R L M) => M N }
instance LieSubmodule.Quotient.addCommGroup {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} :
Equations
instance LieSubmodule.Quotient.module' {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} {S : Type u_1} [] [SMul S R] [Module S M] [] :
Module S (M N)
Equations
• LieSubmodule.Quotient.module' =
instance LieSubmodule.Quotient.module {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} :
Module R (M N)
Equations
• LieSubmodule.Quotient.module =
instance LieSubmodule.Quotient.isCentralScalar {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} {S : Type u_1} [] [SMul S R] [Module S M] [] [SMul Sᵐᵒᵖ R] [] [] [] :
Equations
• =
instance LieSubmodule.Quotient.inhabited {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} :
Equations
• LieSubmodule.Quotient.inhabited = { default := 0 }
@[reducible, inline]
abbrev LieSubmodule.Quotient.mk {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} :
MM 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.

Equations
• LieSubmodule.Quotient.mk = Submodule.Quotient.mk
Instances For
@[simp]
theorem LieSubmodule.Quotient.mk_eq_zero' {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} {m : M} :
m N
theorem LieSubmodule.Quotient.is_quotient_mk {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} (m : M) :
def LieSubmodule.Quotient.lieSubmoduleInvariant {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} [] [LieModule R L M] :
L →ₗ[R] { x : M →ₗ[R] M // x (↑N).compatibleMaps N }

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
Instances For
def LieSubmodule.Quotient.actionAsEndoMap {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule 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
• = { toLinearMap := (↑N).mapQLinear N ∘ₗ LieSubmodule.Quotient.lieSubmoduleInvariant, map_lie' := }
Instances For
instance LieSubmodule.Quotient.actionAsEndoMapBracket {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
Bracket L (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
• = { bracket := fun (x : L) (n : M N) => }
instance LieSubmodule.Quotient.lieQuotientLieRingModule {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
Equations
instance LieSubmodule.Quotient.lieQuotientLieModule {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
LieModule R L (M N)

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

Equations
• =
instance LieSubmodule.Quotient.lieQuotientHasBracket {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :
Bracket (L I) (L I)
Equations
@[simp]
theorem LieSubmodule.Quotient.mk_bracket {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (x : L) (y : L) :
instance LieSubmodule.Quotient.lieQuotientLieRing {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :
LieRing (L I)
Equations
instance LieSubmodule.Quotient.lieQuotientLieAlgebra {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :
LieAlgebra R (L I)
Equations
@[simp]
theorem LieSubmodule.Quotient.mk'_apply {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
∀ (a : M),
def LieSubmodule.Quotient.mk' {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :

LieSubmodule.Quotient.mk as a LieModuleHom.

Equations
• = { toFun := LieSubmodule.Quotient.mk, map_add' := , map_smul' := , map_lie' := }
Instances For
@[simp]
theorem LieSubmodule.Quotient.surjective_mk' {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
@[simp]
theorem LieSubmodule.Quotient.range_mk' {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
.range =
instance LieSubmodule.Quotient.isNoetherian {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] :
Equations
• =
theorem LieSubmodule.Quotient.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] {m : M} :
= 0 m N
@[simp]
theorem LieSubmodule.Quotient.mk'_ker {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] :
.ker = N
@[simp]
theorem LieSubmodule.Quotient.map_mk'_eq_bot_le {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) [] [LieModule R L M] :
N' N
theorem LieSubmodule.Quotient.lieModuleHom_ext_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] {N : LieSubmodule R L M} [] [LieModule R L M] {f : M N →ₗ⁅R,L M} {g : M N →ₗ⁅R,L M} :
f = g f.comp = g.comp
theorem LieSubmodule.Quotient.lieModuleHom_ext {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] ⦃f : M N →ₗ⁅R,L M ⦃g : M N →ₗ⁅R,L M (h : f.comp = g.comp ) :
f = g

Two LieModuleHoms from a quotient lie module are equal if their compositions with LieSubmodule.Quotient.mk' are equal.

See note [partially-applied ext lemmas].

theorem LieSubmodule.Quotient.toEnd_comp_mk' {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) [] [LieModule R L M] (x : L) :
(LieModule.toEnd R L (M N)) x ∘ₗ = ∘ₗ (LieModule.toEnd R L M) x
@[simp]
theorem LieHom.quotKerEquivRange_invFun {R : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R L') :
∀ (a : { x : L' // x }), f.quotKerEquivRange.invFun a = (↑f).quotKerEquivRange.invFun a
@[simp]
theorem LieHom.quotKerEquivRange_toFun {R : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R L') (a : L ) :
f.quotKerEquivRange a = (↑f).quotKerEquivRange a
noncomputable def LieHom.quotKerEquivRange {R : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R L') :
(L f.ker) ≃ₗ⁅R { x : L' // x f.range }

The first isomorphism theorem for morphisms of Lie algebras.

Equations
• f.quotKerEquivRange = { toFun := (↑f).quotKerEquivRange, map_add' := , map_smul' := , map_lie' := , invFun := (↑f).quotKerEquivRange.invFun, left_inv := , right_inv := }
Instances For