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.
Equations
- LieSubmodule.instHasQuotientLieSubmodule = { 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 }
@[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.
Equations
- LieSubmodule.Quotient.mk = Submodule.Quotient.mk
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] ↥(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.
Equations
- LieSubmodule.Quotient.lieSubmoduleInvariant = LinearMap.codRestrict (Submodule.compatibleMaps ↑N ↑N) ↑(LieModule.toEndomorphism R L M) ⋯
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.
Equations
- LieSubmodule.Quotient.actionAsEndoMap N = let __src := Submodule.mapQLinear ↑N ↑N ∘ₗ LieSubmodule.Quotient.lieSubmoduleInvariant; { toLinearMap := __src, map_lie' := ⋯ }
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.
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]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
:
LieRingModule L (M ⧸ N)
Equations
- LieSubmodule.Quotient.lieQuotientLieRingModule N = let __src := LieRingModule.compLieHom (M ⧸ N) (LieSubmodule.Quotient.actionAsEndoMap N); LieRingModule.mk ⋯ ⋯ ⋯
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.
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 = { 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 : L)
(y : L)
:
instance
LieSubmodule.Quotient.lieQuotientLieRing
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{I : LieIdeal R L}
:
Equations
- LieSubmodule.Quotient.lieQuotientLieRing = LieRing.mk ⋯ ⋯ ⋯ ⋯
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
- LieSubmodule.Quotient.lieQuotientLieAlgebra = LieAlgebra.mk ⋯
@[simp]
theorem
LieSubmodule.Quotient.mk'_apply
{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.
Equations
- LieSubmodule.Quotient.mk' N = let __src := Submodule.mkQ ↑N; { toLinearMap := { toAddHom := { 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}
[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.range_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)
:
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]
[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].
theorem
LieSubmodule.Quotient.toEndomorphism_comp_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)
(x : L)
:
(LieModule.toEndomorphism R L (M ⧸ N)) x ∘ₗ ↑(LieSubmodule.Quotient.mk' N) = ↑(LieSubmodule.Quotient.mk' N) ∘ₗ (LieModule.toEndomorphism R L M) x
@[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)), (LieHom.quotKerEquivRange f).invFun a = (LinearMap.quotKerEquivRange ↑f).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)
:
(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⁆ ↥(LieHom.range f)
The first isomorphism theorem for morphisms of Lie algebras.
Equations
- One or more equations did not get rendered due to their size.