The top-weight multiplicity of the CAR module

For the left regular action of gl_N on the Clifford algebra of the trace form, this file computes the dimension of the half-staircase Cartan weight space. The positive-pair occupation elements pᵢⱼ, i < j, are commuting idempotents, and this weight space is their common fixed space.

Each additional fixed-point condition halves the dimension. Indeed, left multiplication by the lowering generator dⱼᵢ exchanges the pᵢⱼ = 1 piece with the pᵢⱼ = 0 piece; on those pieces its inverse is left multiplication by 1/2 dᵢⱼ. Iterating over the choose N 2 positive pairs and using the total Clifford dimension 2 ^ N² gives

2 ^ (N² - choose N 2) = 2 ^ (N * (N + 1) / 2).

The converse fixed-point characterization is obtained row by row. Once the lower rows are fixed, the diagonal equation at row i says that the sum of the remaining commuting upper occupation idempotents has its maximal eigenvalue, so every one of them fixes the vector.

Main result

• TauCeti.finrank_weightSpace_glHalfStaircase_car: the half-staircase weight space has dimension 2 ^ (N * (N + 1) / 2).

References

• D. Panyushev, The exterior algebra and "spin" of an orthogonal g-module, Transform. Groups 6 (2001), Proposition 2.4 and Example 2.5(1).
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

@[simp]

theorem TauCeti.finrank_weightSpace_glHalfStaircase_car {K : Type u_1} [Field K] [CharZero K] [Invertible 2] (N : ℕ) : Module.finrank K ↥(LieModule.weightSpace (CliffordAlgebra (traceQuadraticForm K (Fin N))) ⇑((glWeightEquiv K (Fin N)) (glHalfStaircase K N))) = 2 ^ (N * (N + 1) / 2)

The half-staircase weight space in the left regular CAR module has dimension 2 ^ (N * (N + 1) / 2).