The CAR module: the Clifford algebra of the trace form of gl n, left-regularly #
The adjoint action of gl n K preserves its trace form, so it lifts to the Clifford algebra of
that form; adding the normal-ordering constant makes the lift the homomorphism
TauCeti.glCliffordHom, whose value on a matrix unit is Eᵢⱼ ↦ ½ ∑ₖ dᵢₖ dₖⱼ. This file installs
the gl n K-module structure that the gl n instance of Kostant's isotypy theorem is about: the
Clifford algebra acted on by left multiplication by that lift,
⁅X, c⁆ = glCliffordHom X * c.
The carrier is the fermionic Fock space: CliffordAlgebra.equivExterior identifies it with
⋀(gl n K), of dimension 2 ^ N² for N the cardinality of n
(TauCeti.finrank_cliffordAlgebra_traceQuadraticForm).
This is the trace-form sibling of CliffordAlgebra.kostantLieRingModule, the left-regular module
of the Killing form of a Killing-semisimple Lie algebra, and everything structural is shared with
it: the same LieHom.leftRegularRep builds the action, so the same right multiplications are
intertwiners (TauCeti.carRightMul) and the same left ideals are submodules
(TauCeti.carLieSubmoduleOfLeftIdeal). What is not shared is faithfulness. The Killing case is
faithful outright, because the centre of a Killing-semisimple Lie algebra vanishes; gl n K is
reductive and not semisimple, its centre is the scalar matrices, and the quadratic part of the
lift therefore has a kernel (TauCeti.ker_traceAdjointSO). The normal-ordering constant repairs
that, but only when N is invertible in K (TauCeti.glCliffordHom_injective), so
TauCeti.carLieModule_isFaithful carries the hypothesis (Fintype.card n : K) ≠ 0 too.
As in the Killing case the two instances are scoped, because the same lift produces a second,
competing gl n K-module structure on the same carrier: the inner derivation action
⁅X, c⁆ = ⁅glCliffordHom X, c⁆ of CliffordAlgebra.cliffordDerivationRep, which differs from this
one by a right multiplication (TauCeti.car_lie_sub_mul) and is not the isotypic action. Write
open scoped TauCeti to use them.
Main definitions #
TauCeti.carLieRingModuleandTauCeti.carLieModule: the scoped left-regulargl n K-module structure onCliffordAlgebra (TauCeti.traceQuadraticForm K n).TauCeti.carRightMul: right multiplication, as an endomorphism of that module.TauCeti.carLieSubmoduleOfLeftIdeal: a left ideal, as a Lie submodule.
Main results #
TauCeti.car_lie_def: the defining equation of the action.CliffordAlgebra.car_one_lie_eq_smul: the scalar by which the identity matrix acts.TauCeti.car_lie_ι: its value on a Clifford generator, where the matrix commutator reappears together with a right-multiplication term.TauCeti.car_lie_sub_mul: the comparison with the inner derivation action.TauCeti.carLieModule_isFaithful: the module is faithful onceFintype.card nis invertible, which is exactlyTauCeti.glCliffordHom_injective.TauCeti.finrank_cliffordAlgebra_traceQuadraticForm: the Fock space has dimension2 ^ N².
References #
This implements the "CAR module" target (carLieRingModule, carLieModule, car_lie_def) of the
gl_N worked instance of Layer 9 in
TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md.
- D. Panyushev, On the irreducibility of the Clifford module of a semisimple Lie algebra, Prop. 2.4 and Ex. 2.5(1).
- B. Kostant, Clifford algebra analogue of the Hopf--Koszul--Samelson theorem, Adv. Math. 125 (1997), 275--350.
The CAR module. The Clifford algebra of the trace form of gl n K, acted on by gl n K
through left multiplication by the normal-ordered quadratic lift. Scoped: the inner derivation
action of CliffordAlgebra.cliffordDerivationRep is a competing gl n K-module structure on the
same carrier, so neither may be global.
Equations
Instances For
The CAR module is a Lie module over the base field.
The defining equation of the CAR module: gl n K acts by left multiplication by the
normal-ordered quadratic lift.
The identity matrix acts on the CAR module by the scalar
(Fintype.card n : K) ^ 2 / 2.
The action on a Clifford generator. The matrix commutator is visible in the CAR module, but
only up to a right-multiplication term: left multiplication is not the derivation action. Not a
simp lemma: TauCeti.car_lie_def already rewrites its left-hand side, so simp would never see
this one in simp-normal form.
The CAR 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 normal-ordered quadratic lift.
Right multiplication is an endomorphism of the CAR 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
- TauCeti.carRightMul d = { toLinearMap := LinearMap.mulRight K d, map_lie' := ⋯ }
Instances For
A left ideal of the Clifford algebra is a Lie submodule of the CAR module. The action is by left multiplication, which a left ideal absorbs, so every left ideal is an invariant subspace.
Equations
- TauCeti.carLieSubmoduleOfLeftIdeal I = { toSubmodule := Submodule.restrictScalars K I, lie_mem := ⋯ }
Instances For
Faithfulness through the normal-ordering constant #
The CAR module is faithful when N is invertible in K. Acting on 1 recovers the
normal-ordered quadratic lift, so faithfulness is exactly its injectivity.
The Fock space #
The carrier of the CAR module is the fermionic Fock space ⋀(gl n K), of dimension
2 ^ N²: the Clifford algebra of any quadratic form on a finite free module has rank two to the
rank of the module, and gl n K has rank N².