Lie submodules of a Lie algebra #
In this file we define Lie submodules and Lie ideals, we construct the lattice structure on Lie submodules and we use it to define various important operations, notably the Lie span of a subset of a Lie module.
Main definitions #
LieSubmodule
LieSubmodule.wellFounded_of_noetherian
LieSubmodule.lieSpan
LieSubmodule.map
LieSubmodule.comap
LieIdeal
LieIdeal.map
LieIdeal.comap
Tags #
lie algebra, lie submodule, lie ideal, lattice structure
A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket. This is a sufficient condition for the subset itself to form a Lie module.
Instances For
The zero module is a Lie submodule of any Lie module.
Copy of a LieSubmodule
with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Instances For
An ideal of a Lie algebra is a Lie subalgebra.
Instances For
An ideal of L
is a Lie subalgebra of L
, so it is a Lie ring.
Transfer the LieAlgebra
instance from the coercion LieIdeal → LieSubalgebra
.
Transfer the LieRingModule
instance from the coercion LieIdeal → LieSubalgebra
.
Transfer the LieModule
instance from the coercion LieIdeal → LieSubalgebra
.
Given a Lie subalgebra K ⊆ L
, if we view L
as a K
-module by restriction, it contains
a distinguished Lie submodule for the action of K
, namely K
itself.
Instances For
The set of Lie submodules of a Lie module form a complete lattice.
We provide explicit values for the fields bot
, top
, inf
to get more convenient definitions
than we would otherwise obtain from completeLatticeOfInf
.
The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules.
Instances For
Given two nested Lie submodules N ⊆ N'
, the inclusion N ↪ N'
is a morphism of Lie modules.
Instances For
The lieSpan
of a set s ⊆ M
is the smallest Lie submodule of M
that contains s
.
Instances For
lieSpan
forms a Galois insertion with the coercion from LieSubmodule
to Set
.
Instances For
A morphism of Lie modules f : M → M'
pushes forward Lie submodules of M
to Lie submodules
of M'
.
Instances For
A morphism of Lie modules f : M → M'
pulls back Lie submodules of M'
to Lie submodules of
M
.
Instances For
A morphism of Lie algebras f : L → L'
pushes forward Lie ideals of L
to Lie ideals of L'
.
Note that unlike LieSubmodule.map
, we must take the lieSpan
of the image. Mathematically
this is because although f
makes L'
into a Lie module over L
, in general the L
submodules of
L'
are not the same as the ideals of L'
.
Instances For
A morphism of Lie algebras f : L → L'
pulls back Lie ideals of L'
to Lie ideals of L
.
Note that f
makes L'
into a Lie module over L
(turning f
into a morphism of Lie modules)
and so this is a special case of LieSubmodule.comap
but we do not exploit this fact.
Instances For
See also LieIdeal.map_comap_eq
.
Note that this is not a special case of LieSubmodule.subsingleton_of_bot
. Indeed, given
I : LieIdeal R L
, in general the two lattices LieIdeal R I
and LieSubmodule R L I
are
different (though the latter does naturally inject into the former).
In other words, in general, ideals of I
, regarded as a Lie algebra in its own right, are not the
same as ideals of L
contained in I
.
The kernel of a morphism of Lie algebras, as an ideal in the domain.
Instances For
The range of a morphism of Lie algebras as an ideal in the codomain.
Instances For
The condition that the image of a morphism of Lie algebras is an ideal.
Instances For
The kernel of a morphism of Lie algebras, as an ideal in the domain.
Instances For
The range of a morphism of Lie modules f : M → N
is a Lie submodule of N
.
See Note [range copy pattern].
Instances For
The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra.
This is the Lie subalgebra version of Submodule.topEquiv
.
Instances For
The natural equivalence between the 'top' Lie ideal and the enclosing Lie algebra.
This is the Lie ideal version of Submodule.topEquiv
.