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.instHasQuotient
{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.
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}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
:
AddCommGroup (M ⧸ N)
Equations
- LieSubmodule.Quotient.addCommGroup = Submodule.Quotient.addCommGroup ↑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]
:
Equations
- LieSubmodule.Quotient.module' = Submodule.Quotient.module' ↑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}
:
Equations
- LieSubmodule.Quotient.module = Submodule.Quotient.module ↑N
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)
Equations
- ⋯ = ⋯
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}
:
Equations
- LieSubmodule.Quotient.inhabited = { default := 0 }
@[reducible, inline]
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.
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}
[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
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]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
[LieAlgebra R L]
[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 linear map from L to the endomorphisms of M leaving N invariant.
Equations
- LieSubmodule.Quotient.lieSubmoduleInvariant = LinearMap.codRestrict ((↑N).compatibleMaps ↑N) ↑(LieModule.toEnd R L M) ⋯
Instances For
def
LieSubmodule.Quotient.actionAsEndoMap
{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)
[LieAlgebra R L]
[LieModule 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.
Equations
- LieSubmodule.Quotient.actionAsEndoMap N = { toLinearMap := (↑N).mapQLinear ↑N ∘ₗ LieSubmodule.Quotient.lieSubmoduleInvariant, map_lie' := ⋯ }
Instances For
instance
LieSubmodule.Quotient.actionAsEndoMapBracket
{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)
[LieAlgebra R L]
[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 bracket action of L on the quotient M/N.
Equations
- LieSubmodule.Quotient.actionAsEndoMapBracket N = { bracket := fun (x : L) (n : M ⧸ N) => ((LieSubmodule.Quotient.actionAsEndoMap N) x) n }
instance
LieSubmodule.Quotient.lieQuotientLieRingModule
{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)
[LieAlgebra R L]
[LieModule R L M]
:
LieRingModule L (M ⧸ N)
Equations
instance
LieSubmodule.Quotient.lieQuotientLieModule
{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)
[LieAlgebra R L]
[LieModule R L M]
:
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}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(I : LieIdeal R L)
:
Equations
- LieSubmodule.Quotient.lieQuotientHasBracket I = { bracket := fun (x y : L ⧸ I) => Quotient.liftOn₂' x y (fun (x' y' : L) => LieSubmodule.Quotient.mk ⁅x', y'⁆) ⋯ }
@[simp]
theorem
LieSubmodule.Quotient.mk_bracket
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(I : LieIdeal R L)
(x y : L)
:
instance
LieSubmodule.Quotient.lieQuotientLieRing
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(I : LieIdeal R L)
:
Equations
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)
Equations
def
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)
[LieAlgebra R L]
[LieModule R L M]
:
LieSubmodule.Quotient.mk as a LieModuleHom.
Equations
- LieSubmodule.Quotient.mk' N = { toFun := LieSubmodule.Quotient.mk, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
Instances For
@[simp]
theorem
LieSubmodule.Quotient.mk'_apply
{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)
[LieAlgebra R L]
[LieModule R L M]
(a✝ : M)
:
@[simp]
theorem
LieSubmodule.Quotient.surjective_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)
[LieAlgebra R L]
[LieModule R L M]
:
@[simp]
theorem
LieSubmodule.Quotient.range_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)
[LieAlgebra R L]
[LieModule R L M]
:
(LieSubmodule.Quotient.mk' N).range = ⊤
instance
LieSubmodule.Quotient.isNoetherian
{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)
[IsNoetherian R M]
:
IsNoetherian R (M ⧸ N)
Equations
- ⋯ = ⋯
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)
[LieAlgebra R L]
[LieModule R L M]
{m : M}
:
(LieSubmodule.Quotient.mk' N) m = 0 ↔ m ∈ N
@[simp]
theorem
LieSubmodule.Quotient.mk'_ker
{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)
[LieAlgebra R L]
[LieModule R L M]
:
(LieSubmodule.Quotient.mk' N).ker = N
@[simp]
theorem
LieSubmodule.Quotient.map_mk'_eq_bot_le
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N N' : LieSubmodule R L M)
[LieAlgebra R L]
[LieModule 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]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
[LieModule R L M]
⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄
(h : f.comp (LieSubmodule.Quotient.mk' N) = g.comp (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].
theorem
LieSubmodule.Quotient.toEnd_comp_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)
[LieAlgebra R L]
[LieModule R L M]
(x : L)
:
(LieModule.toEnd R L (M ⧸ N)) x ∘ₗ ↑(LieSubmodule.Quotient.mk' N) = ↑(LieSubmodule.Quotient.mk' N) ∘ₗ (LieModule.toEnd R L M) x
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')
:
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
@[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✝ : ↥(LinearMap.range ↑f))
:
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}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
(f : L →ₗ⁅R⁆ L')
(a : L ⧸ LinearMap.ker ↑f)
:
f.quotKerEquivRange a = (↑f).quotKerEquivRange a