The numerical CAR isotypic decomposition

The left-regular Clifford algebra for the trace form on M_N is already known to be isotypic of type glIrreducible N (glHalfStaircase K N). Its top weight space is one-dimensional in the named irreducible and has dimension 2 ^ (N * (N + 1) / 2) in the CAR module. This file turns those two facts into the numerical multiplicity, the dimension of the simple type, and the resulting direct-sum decomposition.

Main results

• isotypicMultiplicity_glIrreducible_car: the CAR multiplicity is 2 ^ (N * (N + 1) / 2).
• finrank_glIrreducible_glHalfStaircase: the named simple carrier has dimension 2 ^ (N * (N - 1) / 2).
• nonempty_lieModuleEquiv_directSum_glIrreducible_car: the left-regular CAR module is the direct sum of the stated number of copies of that simple carrier.

The mathematical decomposition is the gl_N instance described by Panyushev, The exterior algebra and "spin" of an orthogonal g-module, Proposition 2.4 and Example 2.5(1).

Multiplicity and simple dimension

@[simp]

theorem TauCeti.isotypicMultiplicity_glIrreducible_car (K : Type u_1) [Field K] [CharZero K] [IsAlgClosed K] (N : ℕ) : LieModule.isotypicMultiplicity K (Matrix (Fin N) (Fin N) K) (CliffordAlgebra (traceQuadraticForm K (Fin N))) (glIrreducible N (glHalfStaircase K N)) = 2 ^ (N * (N + 1) / 2)

The half-staircase simple occurs in the left-regular CAR module with multiplicity 2 ^ (N * (N + 1) / 2).

@[simp]

theorem TauCeti.finrank_glIrreducible_glHalfStaircase (K : Type u_1) [Field K] [CharZero K] [IsAlgClosed K] (N : ℕ) : Module.finrank K (glIrreducible N (glHalfStaircase K N)) = 2 ^ (N * (N - 1) / 2)

The half-staircase simple has dimension 2 ^ (N * (N - 1) / 2).

The direct-sum endpoint

theorem TauCeti.nonempty_lieModuleEquiv_directSum_glIrreducible_car (K : Type u_1) [Field K] [CharZero K] [IsAlgClosed K] (N : ℕ) : Nonempty (CliffordAlgebra (traceQuadraticForm K (Fin N)) ≃ₗ⁅K,Matrix (Fin N) (Fin N) K⁆ DirectSum (Fin (2 ^ (N * (N + 1) / 2))) fun (x : Fin (2 ^ (N * (N + 1) / 2))) => glIrreducible N (glHalfStaircase K N))

The left-regular CAR module is the direct sum of 2 ^ (N * (N + 1) / 2) copies of the half-staircase simple.