Isotypy of the left-regular CAR module

Over an algebraically closed field of characteristic zero, the left-regular Clifford algebra of the trace form is an isotypic gl_N-module. Its simple type has the half-shifted staircase highest weight

(N - 1/2, N - 3/2, ..., 1/2).

To identify the weight, write its coordinates as natural occupation counts shifted by 1/2. Highest-weight dominance makes the counts antitone, while the CAR cut identities bound their proper prefix sums and fix their total. The trace-form Casimir scalar supplies the remaining quadratic equality. The staircase majorization criterion then identifies every coordinate.

Main results

• TauCeti.IsGlHighestWeightVector.eq_glHalfStaircase: every CAR highest-weight vector has the half-shifted staircase weight.
• TauCeti.exists_isGlHighestWeightVector_glHalfStaircase_car: every nonzero CAR submodule contains a highest-weight vector of that weight.
• TauCeti.isIsotypicOfType_glIrreducible_car: the left-regular CAR module is isotypic of the simple module with that highest weight.

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).
• D. Shlyakhtenko, Failure of Strong Convergence of Matrices with Fermionic Entries, arXiv:2606.28648, Section 2.3.

theorem TauCeti.IsGlHighestWeightVector.eq_glHalfStaircase {K : Type u_1} [Field K] [CharZero K] {N : ℕ} {μ : Fin N → K} {v : CliffordAlgebra (traceQuadraticForm K (Fin N))} (hv : IsGlHighestWeightVector μ v) : μ = glHalfStaircase K N

Every highest-weight vector in the left-regular CAR module has the half-shifted staircase weight (N - 1/2, N - 3/2, ..., 1/2).

The result is uniform in the rank, including ranks zero and one.

theorem TauCeti.exists_isGlHighestWeightVector_glHalfStaircase_car (K : Type u_1) [Field K] [CharZero K] [IsAlgClosed K] (N : ℕ) (S : LieSubmodule K (Matrix (Fin N) (Fin N) K) (CliffordAlgebra (traceQuadraticForm K (Fin N)))) (hS : S ≠ ⊥) : ∃ (v : ↥S), IsGlHighestWeightVector (glHalfStaircase K N) v

Every nonzero Lie submodule of the left-regular CAR module contains a highest-weight vector of half-shifted staircase weight.

In particular, this identifies the highest weight occurring in every simple CAR submodule.

theorem TauCeti.isIsotypicOfType_glIrreducible_car (K : Type u_1) [Field K] [CharZero K] [IsAlgClosed K] (N : ℕ) : LieModule.IsIsotypicOfType K (Matrix (Fin N) (Fin N) K) (CliffordAlgebra (traceQuadraticForm K (Fin N))) (glIrreducible N (glHalfStaircase K N))

Over an algebraically closed field of characteristic zero, the left-regular CAR module is isotypic of the simple gl_N-module with half-shifted staircase highest weight.