Trivial Lie modules and Abelian Lie algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The action of a Lie algebra L on a module M is trivial if ⁅x, m⁆ = 0 for all x ∈ L and
m ∈ M. In the special case that M = L with the adjoint action, triviality corresponds to the
concept of an Abelian Lie algebra.
In this file we define these concepts and provide some related definitions and results.
Main definitions #
lie_module.is_trivialis_lie_abeliancommutative_ring_iff_abelian_lie_ringlie_module.kerlie_module.max_triv_submodulelie_algebra.center
Tags #
lie algebra, abelian, commutative, center
@[class]
A Lie (ring) module is trivial iff all brackets vanish.
Instances of this typeclass
@[simp]
theorem
trivial_lie_zero
(L : Type v)
(M : Type w)
[has_bracket L M]
[has_zero M]
[lie_module.is_trivial L M]
(x : L)
(m : M) :
@[reducible]
A Lie algebra is Abelian iff it is trivial as a Lie module over itself.
@[protected, instance]
def
lie_ideal.is_lie_abelian_of_trivial
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
[h : lie_module.is_trivial L ↥I] :
theorem
function.injective.is_lie_abelian
{R : Type u}
{L₁ : Type v}
{L₂ : Type w}
[comm_ring R]
[lie_ring L₁]
[lie_ring L₂]
[lie_algebra R L₁]
[lie_algebra R L₂]
{f : L₁ →ₗ⁅R⁆ L₂}
(h₁ : function.injective ⇑f)
(h₂ : is_lie_abelian L₂) :
theorem
function.surjective.is_lie_abelian
{R : Type u}
{L₁ : Type v}
{L₂ : Type w}
[comm_ring R]
[lie_ring L₁]
[lie_ring L₂]
[lie_algebra R L₁]
[lie_algebra R L₂]
{f : L₁ →ₗ⁅R⁆ L₂}
(h₁ : function.surjective ⇑f)
(h₂ : is_lie_abelian L₁) :
theorem
lie_abelian_iff_equiv_lie_abelian
{R : Type u}
{L₁ : Type v}
{L₂ : Type w}
[comm_ring R]
[lie_ring L₁]
[lie_ring L₂]
[lie_algebra R L₁]
[lie_algebra R L₂]
(e : L₁ ≃ₗ⁅R⁆ L₂) :
is_lie_abelian L₁ ↔ is_lie_abelian L₂
theorem
lie_algebra.is_lie_abelian_bot
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
@[protected]
def
lie_module.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] :
lie_ideal R L
The kernel of the action of a Lie algebra L on a Lie module M as a Lie ideal in L.
Equations
- lie_module.ker R L M = (lie_module.to_endomorphism R L M).ker
@[protected, simp]
theorem
lie_module.mem_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]
(x : L) :
def
lie_module.max_triv_submodule
(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] :
lie_submodule R L M
The largest submodule of a Lie module M on which the Lie algebra L acts trivially.
Equations
Instances for ↥lie_module.max_triv_submodule
@[simp]
theorem
lie_module.mem_max_triv_submodule
(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]
(m : M) :
@[protected, instance]
def
lie_module.max_triv_submodule.is_trivial
(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] :
@[simp]
theorem
lie_module.ideal_oper_max_triv_submodule_eq_bot
(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]
(I : lie_ideal R L) :
theorem
lie_module.le_max_triv_iff_bracket_eq_bot
(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} :
theorem
lie_module.trivial_iff_le_maximal_trivial
(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.is_trivial L ↥N ↔ N ≤ lie_module.max_triv_submodule R L M
theorem
lie_module.is_trivial_iff_max_triv_eq_top
(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] :
lie_module.is_trivial L M ↔ lie_module.max_triv_submodule R L M = ⊤
def
lie_module.max_triv_hom
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(f : M →ₗ⁅R,L⁆ N) :
↥(lie_module.max_triv_submodule R L M) →ₗ⁅R,L⁆ ↥(lie_module.max_triv_submodule R L N)
max_triv_submodule is functorial.
Equations
- lie_module.max_triv_hom f = {to_linear_map := {to_fun := λ (m : ↥(lie_module.max_triv_submodule R L M)), ⟨⇑f ↑m, _⟩, map_add' := _, map_smul' := _}, map_lie' := _}
@[simp, norm_cast]
theorem
lie_module.coe_max_triv_hom_apply
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(f : M →ₗ⁅R,L⁆ N)
(m : ↥(lie_module.max_triv_submodule R L M)) :
def
lie_module.max_triv_equiv
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(e : M ≃ₗ⁅R,L⁆ N) :
↥(lie_module.max_triv_submodule R L M) ≃ₗ⁅R,L⁆ ↥(lie_module.max_triv_submodule R L N)
The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent.
Equations
- lie_module.max_triv_equiv e = {to_lie_module_hom := {to_linear_map := {to_fun := ⇑(lie_module.max_triv_hom ↑e), map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := ⇑(lie_module.max_triv_hom ↑(e.symm)), left_inv := _, right_inv := _}
@[simp, norm_cast]
theorem
lie_module.coe_max_triv_equiv_apply
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(e : M ≃ₗ⁅R,L⁆ N)
(m : ↥(lie_module.max_triv_submodule R L M)) :
@[simp]
theorem
lie_module.max_triv_equiv_of_refl_eq_refl
{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] :
@[simp]
theorem
lie_module.max_triv_equiv_of_equiv_symm_eq_symm
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(e : M ≃ₗ⁅R,L⁆ N) :
def
lie_module.max_triv_linear_map_equiv_lie_module_hom
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N] :
A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action on it is trivial.
@[simp]
theorem
lie_module.coe_max_triv_linear_map_equiv_lie_module_hom
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(f : ↥(lie_module.max_triv_submodule R L (M →ₗ[R] N))) :
@[simp]
theorem
lie_module.coe_max_triv_linear_map_equiv_lie_module_hom_symm
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(f : M →ₗ⁅R,L⁆ N) :
@[simp]
theorem
lie_module.coe_linear_map_max_triv_linear_map_equiv_lie_module_hom
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(f : ↥(lie_module.max_triv_submodule R L (M →ₗ[R] N))) :
@[simp]
theorem
lie_module.coe_linear_map_max_triv_linear_map_equiv_lie_module_hom_symm
{R : Type u}
{L : Type v}
{M : Type w}
{N : 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]
[add_comm_group N]
[module R N]
[lie_ring_module L N]
[lie_module R L N]
(f : M →ₗ⁅R,L⁆ N) :
@[reducible]
def
lie_algebra.center
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
lie_ideal R L
The center of a Lie algebra is the set of elements that commute with everything. It can be viewed as the maximal trivial submodule of the Lie algebra as a Lie module over itself via the adjoint representation.
@[protected, instance]
def
lie_algebra.center.is_lie_abelian
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
@[simp]
theorem
lie_algebra.ad_ker_eq_self_module_ker
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
(lie_algebra.ad R L).ker = lie_module.ker R L L
@[simp]
theorem
lie_algebra.self_module_ker_eq_center
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
lie_module.ker R L L = lie_algebra.center R L
theorem
lie_algebra.abelian_of_le_center
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(h : I ≤ lie_algebra.center R L) :
theorem
lie_algebra.is_lie_abelian_iff_center_eq_top
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
is_lie_abelian L ↔ lie_algebra.center R L = ⊤
@[simp]
theorem
lie_submodule.trivial_lie_oper_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)
(I : lie_ideal R L)
[lie_module.is_trivial L M] :