Quotients of Lie algebras and Lie modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
@[protected, instance]
def
lie_submodule.has_quotient
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M] :
has_quotient M (lie_submodule R L M)
The quotient of a Lie module by a Lie submodule. It is a Lie module.
Equations
- lie_submodule.has_quotient = {quotient' := λ (N : lie_submodule R L M), M ⧸ N.to_submodule}
@[protected, instance]
def
lie_submodule.quotient.add_comm_group
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M} :
add_comm_group (M ⧸ N)
@[protected, instance]
def
lie_submodule.quotient.module'
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M}
{S : Type u_1}
[semiring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M] :
@[protected, instance]
def
lie_submodule.quotient.module
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M} :
@[protected, instance]
def
lie_submodule.quotient.is_central_scalar
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M}
{S : Type u_1}
[semiring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M]
[has_smul Sᵐᵒᵖ R]
[module Sᵐᵒᵖ M]
[is_scalar_tower Sᵐᵒᵖ R M]
[is_central_scalar S M] :
is_central_scalar S (M ⧸ N)
@[protected, instance]
def
lie_submodule.quotient.inhabited
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M} :
Equations
@[reducible]
def
lie_submodule.quotient.mk
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M} :
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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M} :
L →ₗ[R] ↥(N.to_submodule.compatible_maps N.to_submodule)
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
- lie_submodule.quotient.lie_submodule_invariant = linear_map.cod_restrict (N.to_submodule.compatible_maps N.to_submodule) ↑(lie_module.to_endomorphism R L M) lie_submodule.quotient.lie_submodule_invariant._proof_3
def
lie_submodule.quotient.action_as_endo_map
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule 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
- lie_submodule.quotient.action_as_endo_map N = {to_linear_map := {to_fun := ((↑N.mapq_linear ↑N).comp lie_submodule.quotient.lie_submodule_invariant).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
@[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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M) :
has_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
- lie_submodule.quotient.action_as_endo_map_bracket N = {bracket := λ (x : L) (n : M ⧸ N), ⇑(⇑(lie_submodule.quotient.action_as_endo_map N) x) n}
@[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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M) :
lie_ring_module L (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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M) :
lie_module R L (M ⧸ N)
The quotient of a Lie module by a Lie submodule, is a Lie module.
@[protected, instance]
def
lie_submodule.quotient.lie_quotient_has_bracket
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
{I : lie_ideal R L} :
has_bracket (L ⧸ I) (L ⧸ I)
Equations
- lie_submodule.quotient.lie_quotient_has_bracket = {bracket := λ (x y : L ⧸ I), quotient.lift_on₂' x y (λ (x' y' : L), lie_submodule.quotient.mk ⁅x', y'⁆) lie_submodule.quotient.lie_quotient_has_bracket._proof_1}
@[simp]
theorem
lie_submodule.quotient.mk_bracket
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
{I : lie_ideal R 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]
[lie_algebra R L]
{I : lie_ideal R L} :
Equations
@[protected, instance]
def
lie_submodule.quotient.lie_quotient_lie_algebra
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
{I : lie_ideal R L} :
lie_algebra R (L ⧸ I)
Equations
def
lie_submodule.quotient.mk'
{R : Type u}
{L : Type v}
{M : Type w}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M) :
lie_submodule.quotient.mk as a lie_module_hom.
Equations
- lie_submodule.quotient.mk' N = {to_linear_map := {to_fun := lie_submodule.quotient.mk N, map_add' := _, map_smul' := _}, map_lie' := _}
@[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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M)
{m : M} :
⇑(lie_submodule.quotient.mk' N) 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M) :
(lie_submodule.quotient.mk' N).ker = N
@[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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N N' : lie_submodule R L M) :
lie_submodule.map (lie_submodule.quotient.mk' N) N' = ⊥ ↔ 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(N : lie_submodule R L M)
⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄
(h : f.comp (lie_submodule.quotient.mk' N) = g.comp (lie_submodule.quotient.mk' N)) :
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]
[lie_algebra R L]
[lie_ring L']
[lie_algebra R L']
(f : L →ₗ⁅R⁆ L')
(ᾰ : L ⧸ linear_map.ker ↑f) :
⇑(f.quot_ker_equiv_range.to_lie_hom) ᾰ = ⇑(↑f.quot_ker_equiv_range) ᾰ
@[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]
[lie_algebra R L]
[lie_ring L']
[lie_algebra R L']
(f : L →ₗ⁅R⁆ L')
(ᾰ : ↥(linear_map.range ↑f)) :
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]
[lie_algebra R L]
[lie_ring L']
[lie_algebra R L']
(f : L →ₗ⁅R⁆ L') :
The first isomorphism theorem for morphisms of Lie algebras.
Equations
- f.quot_ker_equiv_range = {to_lie_hom := {to_linear_map := {to_fun := ⇑(↑f.quot_ker_equiv_range), map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := ↑f.quot_ker_equiv_range.inv_fun, left_inv := _, right_inv := _}
@[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]
[lie_algebra R L]
[lie_ring L']
[lie_algebra R L']
(f : L →ₗ⁅R⁆ L')
(ᾰ : L ⧸ linear_map.ker ↑f) :