The trace-form Casimir on the CAR module

Let Fᵢⱼ be the normal-ordered quadratic lift of the matrix unit Eᵢⱼ to the Clifford algebra of the trace form. The trace-form Casimir acts on the left-regular CAR module by left multiplication with ∑ i, j, Fᵢⱼ Fⱼᵢ. This file proves that this Clifford element is the scalar

N (2 N² - 1) / 4.

This scalar is the Casimir invariant used with the CAR occupation spectrum to constrain the highest weights of irreducible constituents. It is therefore an input to the constituent-weight comparison and the resulting isotypic decomposition of the left-regular CAR module.

Main results

• TauCeti.representation_glCasimir_car_apply: the Casimir acts on every CAR vector by the scalar N (2 N² - 1) / 4.

References

• D. Panyushev, The exterior algebra and "spin" of an orthogonal g-module, Transformation Groups 6 (2001), 371–396, Proposition 2.4 and Example 2.5(1).
• B. Kostant, Clifford algebra analogue of the Hopf--Koszul--Samelson theorem, Advances in Mathematics 125 (1997), 275–350.

@[simp]

theorem TauCeti.representation_glCasimir_car_apply (F : Type u) [Field F] [Invertible 2] (N : ℕ) (c : CliffordAlgebra (traceQuadraticForm F (Fin N))) : ((UniversalEnvelopingAlgebra.representation F (Matrix (Fin N) (Fin N) F) (CliffordAlgebra (traceQuadraticForm F (Fin N)))) (glCasimir F (Fin N))) c = (↑N * (2 * ↑N ^ 2 - 1) / 4) • c

The trace-form Casimir acts on the left-regular CAR module by the scalar N (2 N² - 1) / 4.