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
instance
LieSubmodule.instHasQuotientLieSubmodule
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
:
HasQuotient M (LieSubmodule R L M)
The quotient of a Lie module by a Lie submodule. It is a Lie module.
instance
LieSubmodule.Quotient.addCommGroup
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
:
AddCommGroup (M ⧸ N)
instance
LieSubmodule.Quotient.module'
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
{S : Type u_1}
[Semiring S]
[SMul S R]
[Module S M]
[IsScalarTower S R M]
:
instance
LieSubmodule.Quotient.module
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
:
instance
LieSubmodule.Quotient.isCentralScalar
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
{S : Type u_1}
[Semiring S]
[SMul S R]
[Module S M]
[IsScalarTower S R M]
[SMul Sᵐᵒᵖ R]
[Module Sᵐᵒᵖ M]
[IsScalarTower Sᵐᵒᵖ R M]
[IsCentralScalar S M]
:
IsCentralScalar S (M ⧸ N)
instance
LieSubmodule.Quotient.inhabited
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
:
@[inline, reducible]
abbrev
LieSubmodule.Quotient.mk
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L 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.
Instances For
theorem
LieSubmodule.Quotient.is_quotient_mk
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
(m : M)
:
def
LieSubmodule.Quotient.lieSubmoduleInvariant
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{N : LieSubmodule R L M}
:
L →ₗ[R] { x // x ∈ Submodule.compatibleMaps ↑N ↑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.
Instances For
def
LieSubmodule.Quotient.actionAsEndoMap
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
L →ₗ⁅R⁆ Module.End 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.
Instances For
instance
LieSubmodule.Quotient.actionAsEndoMapBracket
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule 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.
instance
LieSubmodule.Quotient.lieQuotientLieRingModule
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
LieRingModule L (M ⧸ N)
instance
LieSubmodule.Quotient.lieQuotientLieModule
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
The quotient of a Lie module by a Lie submodule, is a Lie module.
@[simp]
theorem
LieSubmodule.Quotient.mk_bracket
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{I : LieIdeal R L}
(x : L)
(y : L)
:
instance
LieSubmodule.Quotient.lieQuotientLieRing
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{I : LieIdeal R L}
:
instance
LieSubmodule.Quotient.lieQuotientLieAlgebra
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{I : LieIdeal R L}
:
LieAlgebra R (L ⧸ I)
@[simp]
theorem
LieSubmodule.Quotient.mk'_toFun
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
∀ (a : M), ↑(LieSubmodule.Quotient.mk' N) a = LieSubmodule.Quotient.mk a
def
LieSubmodule.Quotient.mk'
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
LieSubmodule.Quotient.mk as a LieModuleHom.
Instances For
theorem
LieSubmodule.Quotient.mk_eq_zero
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
{m : M}
:
↑(LieSubmodule.Quotient.mk' N) m = 0 ↔ m ∈ N
@[simp]
theorem
LieSubmodule.Quotient.mk_eq_zero'
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
{m : M}
:
LieSubmodule.Quotient.mk m = 0 ↔ m ∈ N
@[simp]
theorem
LieSubmodule.Quotient.mk'_ker
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
@[simp]
theorem
LieSubmodule.Quotient.map_mk'_eq_bot_le
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
(N' : LieSubmodule R L M)
:
LieSubmodule.map (LieSubmodule.Quotient.mk' N) N' = ⊥ ↔ N' ≤ N
theorem
LieSubmodule.Quotient.lieModuleHom_ext
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
⦃f : M ⧸ N →ₗ⁅R,L⁆ M⦄
⦃g : M ⧸ N →ₗ⁅R,L⁆ M⦄
(h : LieModuleHom.comp f (LieSubmodule.Quotient.mk' N) = LieModuleHom.comp g (LieSubmodule.Quotient.mk' N))
:
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].
@[simp]
theorem
LieHom.quotKerEquivRange_invFun
{R : Type u_1}
{L : Type u_2}
{L' : Type u_3}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
(f : L →ₗ⁅R⁆ L')
:
∀ (a : { x // x ∈ LinearMap.range ↑f }),
LieEquiv.invFun (LieHom.quotKerEquivRange f) a = LinearEquiv.invFun (LinearMap.quotKerEquivRange ↑f) a
@[simp]
theorem
LieHom.quotKerEquivRange_toFun
{R : Type u_1}
{L : Type u_2}
{L' : Type u_3}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
(f : L →ₗ⁅R⁆ L')
(a : L ⧸ LinearMap.ker ↑f)
:
↑(LieHom.quotKerEquivRange f) a = ↑(LinearMap.quotKerEquivRange ↑f) a
noncomputable def
LieHom.quotKerEquivRange
{R : Type u_1}
{L : Type u_2}
{L' : Type u_3}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
(f : L →ₗ⁅R⁆ L')
:
(L ⧸ LieHom.ker f) ≃ₗ⁅R⁆ { x // x ∈ LieHom.range f }
The first isomorphism theorem for morphisms of Lie algebras.