Complete reducibility for the general linear Lie algebra and its CAR module

The Killing form of gl n is degenerate on the scalar matrices, so Weyl's complete-reducibility theorem does not apply to it directly. It does apply to sl n. This file restricts a gl n-module to sl n, and then promotes an sl n-stable complement back to gl n whenever the identity matrix acts by a scalar.

The final section applies this transfer to the left-regular CAR module. The normal-ordered lift sends the identity matrix to the scalar (card n) ^ 2 / 2; hence the centre preserves every sl n-submodule, and the CAR module is completely reducible.

Main results

• TauCeti.exists_isCompl_gl_of_forall_one_lie_eq_smul: a finite-dimensional gl n-module on which the identity acts by a scalar has a complement to every Lie submodule.
• TauCeti.complementedLattice_lieSubmodule_gl_of_forall_one_lie_eq_smul: the corresponding complemented-lattice statement.
• TauCeti.complementedLattice_lieSubmodule_car: complete reducibility of the CAR module.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.3, for Weyl's complete-reducibility theorem.
• B. Kostant, Clifford algebra analogue of the Hopf--Koszul--Samelson theorem, Adv. Math. 125 (1997), 275--350, for the left-regular Clifford module.

Complete reducibility for scalar-centre gl n modules

theorem TauCeti.exists_isCompl_gl_of_forall_one_lie_eq_smul {K : Type u} [Field K] [CharZero K] {n : Type v} [Fintype n] [DecidableEq n] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] [FiniteDimensional K M] {c : K} (hc : ∀ (m : M), ⁅1, m⁆ = c • m) (N : LieSubmodule K (Matrix n n K) M) : ∃ (N' : LieSubmodule K (Matrix n n K) M), IsCompl N N'

Complete reducibility for a general-linear module with scalar centre. Every Lie submodule has a complement when the identity matrix acts by a scalar. Restriction to sl n supplies a complement by Weyl's theorem, and the scalar action makes that complement stable under all of gl n.

theorem TauCeti.complementedLattice_lieSubmodule_gl_of_forall_one_lie_eq_smul (K : Type u) [Field K] [CharZero K] (n : Type v) [Fintype n] [DecidableEq n] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] [FiniteDimensional K M] {c : K} (hc : ∀ (m : M), ⁅1, m⁆ = c • m) : ComplementedLattice (LieSubmodule K (Matrix n n K) M)

The Lie-submodule lattice of a finite-dimensional gl n-module is complemented when the identity matrix acts by a scalar.

The CAR module

theorem TauCeti.complementedLattice_lieSubmodule_car (K : Type u_1) (n : Type u_2) [Field K] [Fintype n] [CharZero K] : ComplementedLattice (LieSubmodule K (Matrix n n K) (CliffordAlgebra (traceQuadraticForm K n)))

The CAR module is completely reducible. Its Lie-submodule lattice is complemented because the normal-ordered action of the identity matrix is scalar.