Trivial Lie modules and Abelian Lie algebras #
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 #
LieModule.IsTrivial
IsLieAbelian
commutative_ring_iff_abelian_lie_ring
LieModule.ker
LieModule.maxTrivSubmodule
LieAlgebra.center
Tags #
lie algebra, abelian, commutative, center
A Lie algebra is Abelian iff it is trivial as a Lie module over itself.
Equations
- IsLieAbelian L = LieModule.IsTrivial L L
Instances For
The kernel of the action of a Lie algebra L
on a Lie module M
as a Lie ideal in L
.
Equations
- LieModule.ker R L M = (LieModule.toEnd R L M).ker
Instances For
The largest submodule of a Lie module M
on which the Lie algebra L
acts trivially.
Equations
Instances For
maxTrivSubmodule
is functorial.
Equations
- LieModule.maxTrivHom f = { toFun := fun (m : ↥(LieModule.maxTrivSubmodule R L M)) => ⟨f ↑m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
Instances For
The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action on it is trivial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- LieAlgebra.center R L = LieModule.maxTrivSubmodule R L L
Instances For
A type synonym for an R
-module to have a trivial Lie module structure.
Equations
- TrivialLieModule R L M = M
Instances For
Equations
Equations
- TrivialLieModule.instModule R L M = inferInstanceAs (Module R M)
The linear equivalence between a trivial Lie module and its underlying R
-module.
Equations
- TrivialLieModule.equiv R L M = LinearEquiv.refl R M
Instances For
Equations
- TrivialLieModule.instLieRingModule R L M = { bracket := fun (x : L) (m : TrivialLieModule R L M) => 0, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }