A highest-weight vector in the CAR algebra

For the left gl_n-action on the Clifford algebra of the trace quadratic form, this file constructs the ordered-product candidate

∏_{i < j} dᵢⱼ,

where dᵢⱼ = ι(Eᵢⱼ), for any finite linearly ordered index type. Over any field, the candidate is nonzero. When 2 is invertible, it is a highest-weight vector of weight i ↦ 1/2 * (1 + 2 * #{j | i < j}). For n = Fin N, this is the half-shifted staircase (N - 1/2, N - 3/2, …, 1/2); in characteristic zero it is also the scalar extension of the rational staircase required by the later CAR simple-submodule and isotypy results.

Main definitions

• TauCeti.carPositiveMatrixUnitFamily: the canonically ordered positive matrix units.
• TauCeti.carHighestWeightVector: their ordered Clifford product candidate.

Main results

• TauCeti.carHighestWeightVector_ne_zero: the candidate is nonzero over any field.
• TauCeti.carHighestWeightVector_eq_one_of_subsingleton: in ranks zero and one the empty ordered product is 1.
• TauCeti.isGlHighestWeightVector_carHighestWeightVector: its direct highest-weight equation.
• TauCeti.isGlHighestWeightVector_glHalfStaircase_carHighestWeightVector: the Fin N half-staircase form over any field in which two is invertible.
• TauCeti.isGlHighestWeightVector_glStaircase_carHighestWeightVector: the Fin N staircase form.

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). The construction below formalizes its gl_N on M_N worked instance.
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

The ordered positive-root product

def TauCeti.carPositiveRootPairs (n : Type u_1) [Fintype n] [LinearOrder n] : Finset (n × n)

The positive roots of gl_n, represented by strictly upper-triangular index pairs.

Equations

• TauCeti.carPositiveRootPairs n = {ij : n × n | ij.1 < ij.2}

@[simp]

theorem TauCeti.mem_carPositiveRootPairs {n : Type u_1} [Fintype n] [LinearOrder n] {i j : n} : (i, j) ∈ carPositiveRootPairs n ↔ i < j

Membership in carPositiveRootPairs means that the first index is strictly below the second.

noncomputable def TauCeti.carPositiveRootPairOrderEmbedding (n : Type u_1) [Fintype n] [LinearOrder n] : Fin (carPositiveRootPairs n).card ↪o Lex (n × n)

The increasing enumeration of positive-root pairs, valued in the lexicographically ordered pair type.

Equations

• TauCeti.carPositiveRootPairOrderEmbedding n = RelEmbedding.trans ((TauCeti.carPositiveRootPairs n).orderEmbOfFin ⋯) { toFun := ⇑toLex, inj' := ⋯, map_rel_iff' := ⋯ }

noncomputable def TauCeti.carPositiveRootPair (n : Type u_1) [Fintype n] [LinearOrder n] (r : Fin (carPositiveRootPairs n).card) : n × n

The positive-root pair at a given place in the canonical lexicographic enumeration.

Equations

• TauCeti.carPositiveRootPair n r = ((TauCeti.carPositiveRootPairs n).orderEmbOfFin ⋯) r

@[simp]

theorem TauCeti.carPositiveRootPairOrderEmbedding_apply (n : Type u_1) [Fintype n] [LinearOrder n] (r : Fin (carPositiveRootPairs n).card) : ofLex ((carPositiveRootPairOrderEmbedding n) r) = carPositiveRootPair n r

The order embedding enumerates the same pair as carPositiveRootPair.

@[simp]

theorem TauCeti.carPositiveRootPair_mem (n : Type u_1) [Fintype n] [LinearOrder n] (r : Fin (carPositiveRootPairs n).card) : carPositiveRootPair n r ∈ carPositiveRootPairs n

Every pair in the canonical enumeration is a positive-root pair.

theorem TauCeti.range_carPositiveRootPair (n : Type u_1) [Fintype n] [LinearOrder n] : Set.range (carPositiveRootPair n) = ↑(carPositiveRootPairs n)

The canonical enumeration ranges over exactly the positive-root pairs.

noncomputable def TauCeti.carPositiveMatrixUnitFamily (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [LinearOrder n] : Fin (carPositiveRootPairs n).card → Matrix n n K

The positive matrix units in the lexicographic order on their index pairs.

Equations

• TauCeti.carPositiveMatrixUnitFamily K n r = (Matrix.stdBasis K n n) (TauCeti.carPositiveRootPair n r)

@[simp]

theorem TauCeti.carPositiveMatrixUnitFamily_apply (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [LinearOrder n] (r : Fin (carPositiveRootPairs n).card) : carPositiveMatrixUnitFamily K n r = (Matrix.stdBasis K n n) (carPositiveRootPair n r)

The positive matrix-unit family is obtained by applying Matrix.stdBasis to the canonical positive-root enumeration.

noncomputable def TauCeti.carHighestWeightVector (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [LinearOrder n] : CliffordAlgebra (traceQuadraticForm K n)

The ordered product candidate formed from all positive matrix-unit Clifford generators. Over a field with invertible 2, it is a highest-weight vector.

Equations

• TauCeti.carHighestWeightVector K n = (List.map (⇑(CliffordAlgebra.ι (TauCeti.traceQuadraticForm K n))) (List.ofFn (TauCeti.carPositiveMatrixUnitFamily K n))).prod

theorem TauCeti.carHighestWeightVector_def (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [LinearOrder n] : carHighestWeightVector K n = (List.map (⇑(CliffordAlgebra.ι (traceQuadraticForm K n))) (List.ofFn (carPositiveMatrixUnitFamily K n))).prod

The defining ordered-product equation for carHighestWeightVector.

@[simp]

theorem TauCeti.carHighestWeightVector_eq_one_of_subsingleton (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [LinearOrder n] [Subsingleton n] : carHighestWeightVector K n = 1

If the index type has at most one element, there are no positive roots and the ordered-product candidate is 1. This includes both the rank-zero and rank-one boundary cases.

theorem TauCeti.carPositiveMatrixUnitFamily_mem {K : Type u_1} {n : Type u_2} [CommRing K] [Fintype n] [LinearOrder n] {i j : n} (hij : i < j) : Matrix.single i j 1 ∈ List.ofFn (carPositiveMatrixUnitFamily K n)

Every positive matrix unit occurs in the canonical family.

theorem TauCeti.carHighestWeightVector_ne_zero {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [LinearOrder n] : carHighestWeightVector K n ≠ 0

The ordered positive-root product is nonzero over any field.

theorem TauCeti.isGlHighestWeightVector_carHighestWeightVector {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [LinearOrder n] [h2 : Invertible 2] : IsGlHighestWeightVector (fun (i : n) => 2⁻¹ * (1 + 2 * ↑{k : n | i < k}.card)) (carHighestWeightVector K n)

The ordered product of all positive matrix-unit Clifford generators is a highest-weight vector for the left gl_n-action on the CAR algebra. Its weight at i is half of one plus twice the number of indices strictly above i.

theorem TauCeti.isGlHighestWeightVector_glHalfStaircase_carHighestWeightVector {K : Type u_1} [Field K] [h2 : Invertible 2] (N : ℕ) : IsGlHighestWeightVector (glHalfStaircase K N) (carHighestWeightVector K (Fin N))

For Fin N, the direct cardinality weight is the half-shifted staircase over any field in which two is invertible.

theorem TauCeti.isGlHighestWeightVector_glStaircase_carHighestWeightVector {K : Type u_1} [Field K] [h2 : Invertible 2] [CharZero K] (N : ℕ) : IsGlHighestWeightVector (fun (i : Fin N) => (algebraMap ℚ K) (glStaircase N i)) (carHighestWeightVector K (Fin N))

For Fin N in characteristic zero, the direct cardinality weight is the scalar extension of the rational staircase TauCeti.glStaircase N.