Modules over a Lie subalgebra which is the whole algebra #
A Lie subalgebra L₁ of L acts on every L-module by restriction along the inclusion. When
L₁ = ⊤ that restriction loses nothing, because every element of L is the underlying element of
one of L₁: the two actions have the same invariant subspaces, hence the same irreducibility, and
a map intertwining the one intertwines the other.
Mathlib has LieSubalgebra.topEquiv, the equivalence (⊤ : LieSubalgebra R L) ≃ₗ⁅R⁆ L of Lie
algebras. That equivalence does not by itself move module-level statements, because a module over
L₁ is not the transport of a module over L along it but the same module with a restricted
action; the three declarations below say what that restriction does to submodules, to
irreducibility, and to equivalences.
The intended use is a Lie algebra presented as generated by a distinguished family, where a
hypothesis is naturally stated over the subalgebra that family generates and the conclusion is
wanted over the whole algebra. TauCeti/Algebra/Lie/Sl2/WeightString.lean classifies modules
irreducible over the subalgebra generated by an sl₂ triple, and
TauCeti/Algebra/Lie/Sl2/Classification.lean converts that into a statement about
LieAlgebra.SpecialLinear.sl (Fin 2) K-modules, the standard triple generating all of
sl (Fin 2) K.
Main definitions #
Ado.lieSubmoduleOfEqTop: a submodule for a Lie subalgebra which is everything, read as a submodule for the whole Lie algebra.Ado.lieModuleEquivOfEqTop: an equivalence of modules over a Lie subalgebra which is everything, read as an equivalence of modules over the whole Lie algebra.
Main results #
Ado.isIrreducible_of_eq_top: a module irreducible over a Lie algebra is irreducible over any Lie subalgebra which is the whole algebra.
Implementation notes #
Neither definition is exposed: each is a repackaging that changes no data, and the equations
Ado.lieSubmoduleOfEqTop_toSubmodule and Ado.lieModuleEquivOfEqTop_apply recording that
are the whole elimination API, so nothing downstream needs to unfold further. Those two equations
are proved by the parenthesised (rfl), which elaborates against the definitions themselves; a
bare rfl in an exported theorem would demand that they be @[expose]d.
A submodule for a Lie subalgebra which is the whole Lie algebra, read as a submodule for the
whole Lie algebra: an element of L acts as the element of L₁ it underlies.
Equations
- Ado.lieSubmoduleOfEqTop hL₁ P = { toSubmodule := ↑P, lie_mem := ⋯ }
Instances For
Irreducibility descends to a Lie subalgebra which is everything. The submodules for the two actions are the same, so the lattice of submodules is simple for the one exactly when it is for the other; only the direction needed in practice is recorded.
An equivalence over a Lie subalgebra which is everything is an equivalence over the whole
algebra. A linear equivalence intertwining the action of every element of L₁ intertwines the
action of every element of L, each of which underlies one of L₁.
Equations
- Ado.lieModuleEquivOfEqTop hL₁ φ = { toLinearMap := ↑φ.toLinearEquiv, map_lie' := ⋯, invFun := φ.toLinearEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }