Type B spin weights in the simply connected character lattice

The spinor module has weights 1 / 2 * (±e₀ ± ⋯ ± e_{n-1}) in the usual orthonormal coordinates. The simply connected type Bₙ datum instead writes its character lattice in the fundamental-weight basis, so a weight is recorded by its pairings with the simple coroots

eᵢ - eᵢ₊₁  (i + 1 < n),       2e_{n-1}  (i + 1 = n).

In those coordinates all spin weights are integral. This file defines the resulting sign-vector family TauCeti.DynkinType.typeBSpinWeight, compares it coordinate by coordinate with TauCeti.spinWeight, and proves that the family spans the full character lattice Fin n → ℤ. The spanning result is the full-weight input needed to construct the simply connected type B Chevalley carrier from the spin representation: the adjoint representation supplies only the index-two root lattice.

The file then describes how the Weyl group moves these weights around, at every rank. A spin weight is minuscule: each of its simple-coroot coordinates is -1, 0 or 1, so the i-th simple reflection carries a spin weight to a spin weight, and it does so by exchanging the signs at the two nonterminal nodes i and i + 1, or by flipping the last sign at the terminal node. That involution of sign sets is TauCeti.DynkinType.typeBSpinReflection; it is identified with reflection in the pinned datum, distinct sign sets are shown to have distinct weights, and every sign set is reached from the all-negative one by a finite sequence of simple reflections. So the spin weights form a single Weyl orbit of pairwise distinct minuscule weights, which is what makes the spin module of the type-B Chevalley carrier irreducible in every characteristic.

Main declarations

• TauCeti.DynkinType.typeBSpinWeight: a spin weight in fundamental-weight coordinates.
• TauCeti.DynkinType.algebraMap_typeBSpinWeight_apply: comparison with the half-integer orthonormal coordinates of TauCeti.spinWeight.
• TauCeti.DynkinType.typeBSpinWeight_univ_eq_single: the all-positive sign vector carries the terminal fundamental weight.
• TauCeti.DynkinType.span_range_typeBSpinWeight_eq_top: the spin weights generate the full simply connected character lattice.
• TauCeti.DynkinType.typeBSpinReflection: the i-th simple reflection as an involution of sign sets, with TauCeti.DynkinType.typeBSpinWeight_typeBSpinReflection_apply the reflection formula against the Bourbaki-numbered Cartan matrix and TauCeti.DynkinType.typeBSimplyConnectedRootDatum_reflection_typeBSpinWeight its identification with reflection in the pinned datum.
• TauCeti.DynkinType.typeBSpinWeight_apply_eq_neg_one_or_eq_zero_or_eq_one: the spin weights are minuscule.
• TauCeti.DynkinType.typeBSpinWeight_injective: distinct sign sets have distinct weights.
• TauCeti.DynkinType.typeBSpinReflection_eq_self_iff: a simple reflection fixes a sign set exactly when the matching coordinate of its weight vanishes.
• TauCeti.DynkinType.exists_typeBSpinReflections_eq: the sign sets form a single orbit of the simple reflections.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Section 20.1.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Section 13.2.

The reflection interface follows the fixed-rank tables of TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E6.MinusculeWeight, which the minuscule weights of type E₆ carry; here the orbit is described uniformly in the rank instead.

Integral spin weights

def TauCeti.DynkinType.typeBSpinWeight {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : ℤ

The weight of a type Bₙ spinor basis vector in fundamental-weight coordinates.

The finite set s records the positive signs. At a nonterminal node the coordinate is the half-difference of two adjacent signs, hence 1, 0, or -1; at the terminal node it is the last sign, because the last simple coroot is 2e_{n-1}.

Equations

• TauCeti.DynkinType.typeBSpinWeight s i = if ↑i + 1 < n then (if i ∈ s then 1 else 0) - if Order.succ i ∈ s then 1 else 0 else (2 * if i ∈ s then 1 else 0) - 1

@[simp]

theorem TauCeti.DynkinType.typeBSpinWeight_apply {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : typeBSpinWeight s i = if ↑i + 1 < n then (if i ∈ s then 1 else 0) - if Order.succ i ∈ s then 1 else 0 else (2 * if i ∈ s then 1 else 0) - 1

The coordinate formula for a type B spin weight.

theorem TauCeti.DynkinType.typeBSpinWeight_eq_neg_one_iff_of_lt {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) (s : Finset (Fin n)) : typeBSpinWeight s i = -1 ↔ i ∉ s ∧ Order.succ i ∈ s

At a nonterminal node, weight -1 means that only the successor has positive sign.

theorem TauCeti.DynkinType.typeBSpinWeight_eq_one_iff_of_lt {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) (s : Finset (Fin n)) : typeBSpinWeight s i = 1 ↔ i ∈ s ∧ Order.succ i ∉ s

At a nonterminal node, weight 1 means that only the node has positive sign.

theorem TauCeti.DynkinType.typeBSpinWeight_eq_neg_one_iff_of_last {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) (s : Finset (Fin n)) : typeBSpinWeight s i = -1 ↔ i ∉ s

At the terminal node, weight -1 means that its sign is negative.

theorem TauCeti.DynkinType.typeBSpinWeight_eq_one_iff_of_last {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) (s : Finset (Fin n)) : typeBSpinWeight s i = 1 ↔ i ∈ s

At the terminal node, weight 1 means that its sign is positive.

theorem TauCeti.DynkinType.algebraMap_typeBSpinWeight_apply {K : Type u_1} [CommRing K] [Invertible 2] {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : (algebraMap ℤ K) (typeBSpinWeight s i) = if ↑i + 1 < n then spinWeight K s i - spinWeight K s (Order.succ i) else spinWeight K s i + spinWeight K s i

The coordinate comparison, in any commutative ring in which 2 is invertible: typeBSpinWeight is obtained from the orthonormal sign weight by pairing with the simple coroot, that is, by taking an adjacent difference away from the terminal node and doubling the terminal coordinate.

theorem TauCeti.DynkinType.algebraMap_typeBSpinWeight {K : Type u_1} [CommRing K] [Invertible 2] {n : ℕ} (s : Finset (Fin n)) : (fun (i : Fin n) => (algebraMap ℤ K) (typeBSpinWeight s i)) = fun (i : Fin n) => if ↑i + 1 < n then spinWeight K s i - spinWeight K s (Order.succ i) else spinWeight K s i + spinWeight K s i

The comparison with half-integer spin weights, as an equality of coordinate vectors.

A spanning family

theorem TauCeti.DynkinType.typeBSpinWeight_univ_apply {n : ℕ} (i : Fin n) : typeBSpinWeight Finset.univ i = if ↑i + 1 = n then 1 else 0

The all-positive sign weight has only its terminal fundamental-weight coordinate nonzero.

theorem TauCeti.DynkinType.typeBSpinWeight_univ_eq_single {n : ℕ} (hn : 1 ≤ n) : typeBSpinWeight Finset.univ = Pi.single ⟨n - 1, ⋯⟩ 1

The all-positive type-B spin weight is the terminal fundamental weight. In fundamental-weight coordinates it has value one at the terminal short node and zero at every other node.

theorem TauCeti.DynkinType.span_range_typeBSpinWeight_eq_top (n : ℕ) : Submodule.span ℤ (Set.range typeBSpinWeight) = ⊤

The type Bₙ spin weights generate the full simply connected character lattice.

For a nonterminal node i, the sign sequence positive through i has weight ωᵢ - ω_{n-1}, while the all-positive sequence has weight ω_{n-1}. At the terminal node the cut sequence is already ω_{n-1}. Thus every fundamental-weight basis vector lies in the span.

The simple reflections on sign sets

def TauCeti.DynkinType.typeBSpinReflection {n : ℕ} (i : Fin n) : Equiv.Perm (Finset (Fin n))

The i-th simple reflection of type Bₙ, acting on spin sign sets.

The spin weights are indexed by the finite set of positive signs, and the Weyl group acts on them by signed permutations of the orthonormal coordinates. At a nonterminal node the simple root is eᵢ - eᵢ₊₁, so its reflection exchanges the signs at i and i + 1; at the terminal node the simple root is e_{n-1}, so its reflection flips the last sign.

Equations

• TauCeti.DynkinType.typeBSpinReflection i = if ↑i + 1 < n then Equiv.finsetCongr (Equiv.swap i (Order.succ i)) else Function.Involutive.toPerm (fun (s : Finset (Fin n)) => symmDiff s {i}) ⋯

theorem TauCeti.DynkinType.typeBSpinReflection_apply_of_lt {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) (s : Finset (Fin n)) : (typeBSpinReflection i) s = Finset.map (Equiv.toEmbedding (Equiv.swap i (Order.succ i))) s

At a nonterminal node the simple reflection transports a sign set along the transposition of the node with its successor.

theorem TauCeti.DynkinType.typeBSpinReflection_apply_of_last {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) (s : Finset (Fin n)) : (typeBSpinReflection i) s = symmDiff s {i}

At the terminal node the simple reflection toggles the membership of that node.

@[simp]

theorem TauCeti.DynkinType.typeBSpinReflection_apply_apply {n : ℕ} (i : Fin n) (s : Finset (Fin n)) : (typeBSpinReflection i) ((typeBSpinReflection i) s) = s

The simple reflections are involutions.

@[simp]

theorem TauCeti.DynkinType.mem_typeBSpinReflection_iff_of_lt {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) {s : Finset (Fin n)} {a : Fin n} : a ∈ (typeBSpinReflection i) s ↔ (Equiv.swap i (Order.succ i)) a ∈ s

Membership in a reflected sign set at a nonterminal node, read through the transposition of the node with its successor.

@[simp]

theorem TauCeti.DynkinType.mem_typeBSpinReflection_iff_of_last {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) {s : Finset (Fin n)} {a : Fin n} : a ∈ (typeBSpinReflection i) s ↔ if a = i then a ∉ s else a ∈ s

Membership in a reflected sign set at the terminal node: only that node's sign changes.

theorem TauCeti.DynkinType.typeBSpinReflection_eq_insert_of_not_mem_last {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) {s : Finset (Fin n)} (hi : i ∉ s) : (typeBSpinReflection i) s = insert i s

The terminal reflection inserts a missing positive sign.

theorem TauCeti.DynkinType.typeBSpinReflection_eq_erase_of_mem_last {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) {s : Finset (Fin n)} (hi : i ∈ s) : (typeBSpinReflection i) s = s.erase i

The terminal reflection erases an existing positive sign.

theorem TauCeti.DynkinType.typeBSpinReflection_eq_insert_erase_of_not_mem {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) {s : Finset (Fin n)} (hi : i ∉ s) (hj : Order.succ i ∈ s) : (typeBSpinReflection i) s = insert i (s.erase (Order.succ i))

An adjacent reflection moves a positive successor sign to the negative node.

theorem TauCeti.DynkinType.typeBSpinReflection_eq_insert_erase_of_mem {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) {s : Finset (Fin n)} (hi : i ∈ s) (hj : Order.succ i ∉ s) : (typeBSpinReflection i) s = insert (Order.succ i) (s.erase i)

An adjacent reflection moves a positive node sign to its negative successor.

The reflection formula

Coordinates of a reflected spin weight

The formula

theorem TauCeti.DynkinType.typeBSpinWeight_typeBSpinReflection_apply {n : ℕ} (i : Fin n) (s : Finset (Fin n)) (j : Fin n) : typeBSpinWeight ((typeBSpinReflection i) s) j = typeBSpinWeight s j - typeBSpinWeight s i * CartanMatrix.B n i j

The reflection formula for type-Bₙ spin weights. Reflecting a sign set in the i-th simple root subtracts, from its weight, the i-th simple-coroot coordinate of that weight times the i-th simple root. In the fundamental-weight basis the i-th simple root is the i-th row of the Bourbaki-numbered Cartan matrix, so the spin weights are permuted by the Weyl group.

That row is the row of a chain of type B, TauCeti.chainBEntry, whose double edge points at the terminal node: the terminal simple root is the short one, so the root before it pairs to -2 with the long terminal coroot, while the terminal root pairs to -1 with the coroot before it.

Distinct weights and fixed points

theorem TauCeti.DynkinType.typeBSpinWeight_apply_eq_neg_one_or_eq_zero_or_eq_one {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : typeBSpinWeight s i = -1 ∨ typeBSpinWeight s i = 0 ∨ typeBSpinWeight s i = 1

Every simple-coroot coordinate of a type-Bₙ spin weight is -1, 0 or 1: the spin weights are minuscule.

theorem TauCeti.DynkinType.typeBSpinWeight_injective {n : ℕ} : Function.Injective typeBSpinWeight

Distinct sign sets have distinct type-Bₙ spin weights. The last coordinate of the weight recovers the last sign, and the remaining signs follow from the adjacent differences.

@[simp]

theorem TauCeti.DynkinType.typeBSpinReflection_eq_self_iff {n : ℕ} (i : Fin n) (s : Finset (Fin n)) : (typeBSpinReflection i) s = s ↔ typeBSpinWeight s i = 0

A simple reflection fixes a sign set exactly when the matching simple-coroot coordinate of its weight vanishes.

A single Weyl orbit

theorem TauCeti.DynkinType.exists_typeBSpinReflections_eq {n : ℕ} (s : Finset (Fin n)) : ∃ (l : List (Fin n)), List.foldl (fun (t : Finset (Fin n)) (i : Fin n) => (typeBSpinReflection i) t) ∅ l = s

The type-Bₙ spin weights form a single orbit of the simple reflections. Every sign set is reached from the all-negative one by a finite sequence of simple reflections, so the spin module is minuscule with a connected weight graph.

@[simp]

theorem TauCeti.DynkinType.typeBSimplyConnectedRootDatum_reflection_typeBSpinWeight {n : ℕ} (i : Fin n) (s : Finset (Fin n)) : (RootPairing.reflection (typeBSimplyConnectedRootDatum n) (typeBSimpleIndex n i)) (typeBSpinWeight s) = typeBSpinWeight ((typeBSpinReflection i) s)

The sign-set reflection is reflection in the pinned type-Bₙ datum. The weight of a reflected sign set is the Weyl reflection of its weight in the corresponding simple root of TauCeti.DynkinType.typeBSimplyConnectedRootDatum.