Kostant's module: the Clifford algebra of the Killing form, left-regularly #
For a Killing-semisimple Lie algebra L the adjoint action is skew-adjoint for the Killing form,
so it lifts to the quadratic elements of the Clifford algebra of that form
(CliffordAlgebra.adjointCliffordHom). This file installs the L-module structure that Kostant's
isotypy theorem is about: the Clifford algebra acted on by left multiplication by that lift,
⁅x, c⁆ = adjointCliffordHom K L x * c.
The choice of action is not cosmetic. The other L-module structure the same lift produces is the
inner derivation action ⁅x, c⁆ = ⁅adjointCliffordHom K L x, c⁆ of
CliffordAlgebra.cliffordDerivationRep, which under CliffordAlgebra.equivExterior is the
exterior extension of the adjoint representation and is in general not the isotypic action that
Kostant's theorem is about; the two differ by right multiplication
(CliffordAlgebra.kostant_lie_sub_mul). What distinguishes the left-regular action is that its
submodules include every left ideal (CliffordAlgebra.kostantLieSubmoduleOfLeftIdeal) and its
endomorphisms include every right multiplication (CliffordAlgebra.kostantRightMul), which is the
commutant the isotypy argument runs on.
The two instances are scoped, as the roadmap asks: the Clifford algebra of the Killing form is
not otherwise an L-module, and a global instance would fix one of the two competing actions for
every consumer. Write open scoped CliffordAlgebra to use them.
Main definitions #
CliffordAlgebra.kostantLieRingModuleandCliffordAlgebra.kostantLieModule: the scoped left-regularL-module structure onCliffordAlgebra (killingQuadraticForm K L).CliffordAlgebra.kostantRightMul: right multiplication, as an endomorphism of that module.CliffordAlgebra.kostantLieSubmoduleOfLeftIdeal: a left ideal, as a Lie submodule.
Main results #
CliffordAlgebra.kostant_lie_def: the defining equation of the action.CliffordAlgebra.kostant_lie_ι: its value on a Clifford generator, where the adjoint action ofLreappears together with a right-multiplication term.CliffordAlgebra.kostant_lie_sub_mul: the comparison with the inner derivation action.CliffordAlgebra.kostantLieModuleIsFaithful: the action is faithful, because the adjoint representation of a Killing-semisimple Lie algebra is (CliffordAlgebra.adjointCliffordHom_injective, proved alongside the lift itself).
The carrier is a finite module over K, which is what makes the statement that its simple
submodules are all isomorphic a statement about something; nothing here needs that, so the
instance saying so is left to TauCeti.LinearAlgebra.CliffordAlgebra.Dimension, to be imported
by whichever later file uses it.
References #
This implements the "Kostant's setting, packaged" target (kostantLieRingModule,
kostantLieModule, kostant_lie_def) of Layer 9 in
TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md.
- B. Kostant, Clifford algebra analogue of the Hopf--Koszul--Samelson theorem, Adv. Math. 125 (1997), 275--350.
Kostant's module. The Clifford algebra of the Killing quadratic form, acted on by L
through left multiplication by the adjoint quadratic lift. Scoped: the inner derivation action of
CliffordAlgebra.cliffordDerivationRep is a competing L-module structure on the same carrier,
so neither may be global.
Equations
Instances For
Kostant's module is a Lie module over the base field.
The defining equation of Kostant's module: L acts by left multiplication by the adjoint
quadratic lift.
The action on a Clifford generator. The adjoint action of L on itself is visible in
Kostant's module, but only up to a right-multiplication term: left multiplication is not the
derivation action. Not a simp lemma: CliffordAlgebra.kostant_lie_def already rewrites its
left-hand side, so simp would never see this one in simp-normal form.
Kostant's action minus right multiplication is the inner derivation action. This is the
precise sense in which the left-regular module and the exterior extension of the adjoint
representation are different modules on the same carrier; it is the pointwise form of
LieHom.ad_apply_eq_leftRegularRep_sub_mulRight for the adjoint quadratic lift.
Right multiplication is an endomorphism of Kostant's module. Associativity of the Clifford algebra says that left and right multiplications commute, so every right multiplication lies in the commutant of the action; this is the supply of intertwiners behind the isotypy statement.
Equations
- d.kostantRightMul = { toLinearMap := LinearMap.mulRight K d, map_lie' := ⋯ }
Instances For
A left ideal of the Clifford algebra is a Lie submodule of Kostant's module. The action is by left multiplication, which a left ideal absorbs, so every left ideal is an invariant subspace; what such a submodule decomposes into is the business of the later Kostant theorems, not of this construction.
Equations
- CliffordAlgebra.kostantLieSubmoduleOfLeftIdeal I = { toSubmodule := Submodule.restrictScalars K I, lie_mem := ⋯ }
Instances For
Kostant's module is faithful. Acting on 1 recovers the adjoint quadratic lift, which is
injective because the centre of a Killing-semisimple Lie algebra vanishes.