Type D 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 Dₙ 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),       e_{n-2} + e_{n-1}  (i + 1 = n).

In those coordinates all spin weights are integral. This file defines the resulting sign-vector family TauCeti.DynkinType.typeDSpinWeight, compares it coordinate by coordinate with TauCeti.spinWeight, and proves that the family spans the full character lattice Fin n → ℤ. Using all spinor weights is essential in even rank: either half-spin family alone reaches only one of the two nonzero spinor cosets of the root lattice.

The type-D graph automorphism changes the sign of the final orthonormal coordinate. On the sign-set indexing the spin basis, this toggles membership of the final index. The resulting permutation exchanges the even and odd half-spin bases and carries each spin weight through the fork-node permutation TauCeti.graphPermD. Thus the full spin module, rather than either half-spin summand by itself, is the weight-stable input for the graph-twisted carrier.

The spanning result is the full-weight input needed to construct the simply connected type D Chevalley carrier from the spin representation. The adjoint representation supplies only the index-four root lattice.

The second half of the file describes how the Weyl group moves the spin basis around, uniformly in the rank. Reflection in a chain simple root eᵢ - eᵢ₊₁ exchanges two adjacent signs; reflection in the fork simple root e_{n-2} + e_{n-1} exchanges the last two signs and reverses both. Both act on the indexing sign sets, giving TauCeti.DynkinType.typeDSpinReflection, and both change the number of positive signs by an even amount. Every pairing of a spin weight with a simple coroot is -1, 0, or 1, and the spin weights are pairwise distinct, so the spin module is multiplicity free, and the orbits of the simple reflections on its basis are exactly the two half-spin parity classes. So the weight basis of the full spin module splits into two Weyl orbits, and its weights alone do not exhibit it as irreducible.

Main declarations

• TauCeti.DynkinType.typeDSpinWeight: a spin weight in fundamental-weight coordinates.
• TauCeti.DynkinType.algebraMap_typeDSpinWeight_apply: comparison with the half-integer orthonormal coordinates of TauCeti.spinWeight.
• TauCeti.DynkinType.typeDSpinWeight_univ_apply, TauCeti.DynkinType.typeDSpinWeight_univ_eq_single, and TauCeti.DynkinType.typeDSpinWeight_univ_erase_last_eq_single: the terminal and penultimate fork fundamental weights.
• TauCeti.DynkinType.span_range_typeDSpinWeight_eq_top: the spin weights generate the full simply connected character lattice.
• TauCeti.DynkinType.typeDSpinGraphPerm: the graph symmetry on the spin basis, with TauCeti.DynkinType.typeDSpinWeight_typeDSpinGraphPerm_apply recording its action on weights, and TauCeti.DynkinType.typeDSpinGraphPerm_of_mem and TauCeti.DynkinType.typeDSpinGraphPerm_of_notMem reading the toggle as an erasure or an insertion.
• TauCeti.DynkinType.typeDSpinReflection: the i-th simple reflection on the sign sets, with TauCeti.DynkinType.mem_typeDSpinReflection_of_add_one_lt and TauCeti.DynkinType.mem_typeDSpinReflection_of_not_add_one_lt for membership and TauCeti.DynkinType.typeDSpinReflection_apply_apply for involutivity.
• TauCeti.DynkinType.typeDSpinWeight_typeDSpinReflection_apply and TauCeti.DynkinType.typeDSimplyConnectedRootDatum_reflection_typeDSpinWeight: the reflection formula against the i-th row of CartanMatrix.D n, and its identification with reflection in the pinned datum.
• TauCeti.DynkinType.typeDSpinWeight_apply_eq_neg_one_or_eq_zero_or_eq_one and TauCeti.DynkinType.typeDSpinWeight_injective: every pairing of a spin weight with a simple coroot is -1, 0, or 1, and the spin weights are pairwise distinct.
• TauCeti.DynkinType.typeDSpinReflection_eq_self_iff: a simple reflection fixes a sign set exactly where the corresponding weight coordinate vanishes.
• TauCeti.DynkinType.typeDSpinReflection_typeDSpinReflection_fork: the two fork reflections compose to the toggle of the last two signs.
• TauCeti.DynkinType.even_card_typeDSpinReflection_iff and TauCeti.DynkinType.exists_typeDSpinReflections_eq_iff: the simple reflections preserve the parity of a sign set, and two sign sets lie in one reflection orbit exactly when their parities agree.

References

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

The integral-coordinate and spanning API follows the parallel type B construction in Tau Ceti PR #4847. The fork coordinate and the use of both half-spin parities are the type D changes. The shape of the reflection interface, from the involution on basis indices through the coordinate equation to the orbit statement, follows the fixed-rank type-E₆ one in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E6.MinusculeWeight.

Integral spin weights

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

The weight of a type Dₙ 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 fork node it is the half-sum of the last two signs.

Equations

• TauCeti.DynkinType.typeDSpinWeight s i = if h : ↑i + 1 < n then (if i ∈ s then 1 else 0) - if ⟨↑i + 1, h⟩ ∈ s then 1 else 0 else ((if ⟨↑i - 1, ⋯⟩ ∈ s then 1 else 0) + if i ∈ s then 1 else 0) - 1

@[simp]

theorem TauCeti.DynkinType.typeDSpinWeight_apply {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : typeDSpinWeight s i = if h : ↑i + 1 < n then (if i ∈ s then 1 else 0) - if ⟨↑i + 1, h⟩ ∈ s then 1 else 0 else ((if ⟨↑i - 1, ⋯⟩ ∈ s then 1 else 0) + if i ∈ s then 1 else 0) - 1

The coordinate formula for a type D spin weight.

theorem TauCeti.DynkinType.algebraMap_typeDSpinWeight_apply {K : Type u_1} [CommRing K] [Invertible 2] {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : (algebraMap ℤ K) (typeDSpinWeight s i) = if h : ↑i + 1 < n then spinWeight K s i - spinWeight K s ⟨↑i + 1, h⟩ else spinWeight K s ⟨↑i - 1, ⋯⟩ + spinWeight K s i

After mapping to any coefficient ring in which 2 is invertible, typeDSpinWeight is obtained from the orthonormal sign weight by pairing with the simple coroot: take an adjacent difference away from the terminal node and the sum of the last two coordinates at the terminal fork node.

theorem TauCeti.DynkinType.algebraMap_typeDSpinWeight {K : Type u_1} [CommRing K] [Invertible 2] {n : ℕ} (s : Finset (Fin n)) : (fun (i : Fin n) => (algebraMap ℤ K) (typeDSpinWeight s i)) = fun (i : Fin n) => if h : ↑i + 1 < n then spinWeight K s i - spinWeight K s ⟨↑i + 1, h⟩ else spinWeight K s ⟨↑i - 1, ⋯⟩ + spinWeight K s i

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

theorem TauCeti.DynkinType.algebraMap_typeDSpinWeight_eq_dotProduct {K : Type u_1} [CommRing K] [Invertible 2] {n : ℕ} (hn : 4 ≤ n) (s : Finset (Fin n)) (i : Fin n) : (algebraMap ℤ K) (typeDSpinWeight s i) = spinWeight K s ⬝ᵥ fun (j : Fin n) => (algebraMap ℤ K) (typeDSimpleRoot n hn i j)

For a valid type Dₙ, the integral coordinate of a spin weight is its pairing with the corresponding Bourbaki simple coroot in orthonormal coordinates. Type D is simply laced, so the simple coroot is typeDSimpleRoot n hn i.

The graph automorphism on spin weights

def TauCeti.DynkinType.typeDSpinGraphPerm (n : ℕ) (hn : 1 ≤ n) : Equiv.Perm (Finset (Fin n))

The permutation of the type-D spin basis induced by the graph automorphism: toggle the sign of the final orthonormal coordinate. A sign is encoded by membership in the indexing finset, so this takes the symmetric difference with the singleton containing the final index.

Equations

• TauCeti.DynkinType.typeDSpinGraphPerm n hn = Function.Involutive.toPerm (fun (x : Finset (Fin n)) => symmDiff x {⟨n - 1, ⋯⟩}) ⋯

theorem TauCeti.DynkinType.typeDSpinGraphPerm_apply (n : ℕ) (hn : 1 ≤ n) (s : Finset (Fin n)) : (typeDSpinGraphPerm n hn) s = symmDiff s {⟨n - 1, ⋯⟩}

The type-D spin graph permutation acts by symmetric difference with the final index.

@[simp]

theorem TauCeti.DynkinType.typeDSpinGraphPerm_of_mem (n : ℕ) (hn : 1 ≤ n) {s : Finset (Fin n)} (hs : ⟨n - 1, ⋯⟩ ∈ s) : (typeDSpinGraphPerm n hn) s = s.erase ⟨n - 1, ⋯⟩

Toggling the final sign of a sign set that carries the final index erases it.

@[simp]

theorem TauCeti.DynkinType.typeDSpinGraphPerm_of_notMem (n : ℕ) (hn : 1 ≤ n) {s : Finset (Fin n)} (hs : ⟨n - 1, ⋯⟩ ∉ s) : (typeDSpinGraphPerm n hn) s = insert ⟨n - 1, ⋯⟩ s

Toggling the final sign of a sign set that lacks the final index inserts it.

@[simp]

theorem TauCeti.DynkinType.mem_typeDSpinGraphPerm_iff (n : ℕ) (hn : 1 ≤ n) (s : Finset (Fin n)) (i : Fin n) : i ∈ (typeDSpinGraphPerm n hn) s ↔ (i ∈ s ↔ ↑i + 1 ≠ n)

An index belongs to the graph-transformed sign set precisely when its old membership agrees with not being the final index. Thus membership is unchanged away from the final coordinate and reversed there.

@[simp]

theorem TauCeti.DynkinType.typeDSpinGraphPerm_apply_apply (n : ℕ) (hn : 1 ≤ n) (s : Finset (Fin n)) : (typeDSpinGraphPerm n hn) ((typeDSpinGraphPerm n hn) s) = s

Toggling the final sign twice is the identity.

@[simp]

theorem TauCeti.DynkinType.typeDSpinGraphPerm_symm (n : ℕ) (hn : 1 ≤ n) : Equiv.symm (typeDSpinGraphPerm n hn) = typeDSpinGraphPerm n hn

The permutation which toggles the final sign is an involution.

@[simp]

theorem TauCeti.DynkinType.even_card_typeDSpinGraphPerm_iff (n : ℕ) (hn : 1 ≤ n) (s : Finset (Fin n)) : Even ((typeDSpinGraphPerm n hn) s).card ↔ Odd s.card

The graph permutation exchanges the two half-spin parities: an even sign set is sent to an odd one and conversely.

@[simp]

theorem TauCeti.DynkinType.odd_card_typeDSpinGraphPerm_iff (n : ℕ) (hn : 1 ≤ n) (s : Finset (Fin n)) : Odd ((typeDSpinGraphPerm n hn) s).card ↔ Even s.card

Equivalently, the graph permutation sends odd sign sets to even ones.

theorem TauCeti.DynkinType.typeDSpinWeight_typeDSpinGraphPerm_apply {n : ℕ} (hn : 2 ≤ n) (s : Finset (Fin n)) (i : Fin n) : typeDSpinWeight ((typeDSpinGraphPerm n ⋯) s) i = typeDSpinWeight s ((graphPermD n hn) i)

The final-sign toggle realizes the type-D graph automorphism on spin weights. Applying the fork-node permutation to the fundamental-weight coordinates of a spin weight gives the weight indexed by the sign set with its final membership toggled.

theorem TauCeti.DynkinType.image_comp_graphPermD_range_typeDSpinWeight {n : ℕ} (hn : 2 ≤ n) : (fun (wt : Fin n → ℤ) => wt ∘ ⇑(graphPermD n hn)) '' Set.range typeDSpinWeight = Set.range typeDSpinWeight

The type-D graph permutation preserves the full family of spin weights as a set.

A spanning family

@[simp]

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

The all-positive type-D spin weight, evaluated at an arbitrary fundamental-weight coordinate.

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

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

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

Erasing the final sign from the all-positive type-D spin weight gives the penultimate fundamental weight. This pins the order of the two fork weights under the diagram symmetry.

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

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

The all-positive sign sequence has weight ω_{n-1}. A sign sequence positive through a node strictly before the fork has weight ωᵢ - ω_{n-1}; at the penultimate node it has weight ω_{n-2}. Thus the weights from both half-spin parities contain enough differences to generate every fundamental-weight basis vector.

Simple reflections on the spin basis

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

The i-th simple reflection of type Dₙ, acting on the sign sets that index the spin basis.

A sign is recorded by membership in the finset. At a chain node i, whose simple root is eᵢ - eᵢ₊₁, the reflection exchanges the signs at i and i + 1. At the terminal fork node, whose simple root is e_{n-2} + e_{n-1}, it exchanges the last two signs and reverses both.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DynkinType.typeDSpinReflection_of_add_one_lt {n : ℕ} {i : Fin n} (hi : ↑i + 1 < n) (s : Finset (Fin n)) : typeDSpinReflection i s = Finset.map (Equiv.toEmbedding (Equiv.swap i ⟨↑i + 1, hi⟩)) s

At a chain node the simple reflection is the transposition of the two adjacent signs.

theorem TauCeti.DynkinType.typeDSpinReflection_of_not_add_one_lt {n : ℕ} {i : Fin n} (hi : ¬↑i + 1 < n) (s : Finset (Fin n)) : typeDSpinReflection i s = symmDiff (Finset.map (Equiv.toEmbedding (Equiv.swap ⟨↑i - 1, ⋯⟩ i)) s) {⟨↑i - 1, ⋯⟩, i}

At the terminal fork node the simple reflection transposes the last two signs and reverses both.

theorem TauCeti.DynkinType.mem_typeDSpinReflection_of_add_one_lt {n : ℕ} {i : Fin n} (hi : ↑i + 1 < n) (s : Finset (Fin n)) (x : Fin n) : x ∈ typeDSpinReflection i s ↔ (Equiv.swap i ⟨↑i + 1, hi⟩) x ∈ s

Membership in a chain-node reflection of a sign set, read through the transposition.

theorem TauCeti.DynkinType.mem_typeDSpinReflection_of_not_add_one_lt {n : ℕ} {i : Fin n} (hi : ¬↑i + 1 < n) (s : Finset (Fin n)) (x : Fin n) : x ∈ typeDSpinReflection i s ↔ ((Equiv.swap ⟨↑i - 1, ⋯⟩ i) x ∈ s ↔ x ≠ ⟨↑i - 1, ⋯⟩ ∧ x ≠ i)

Membership in the fork-node reflection of a sign set: away from the last two indices it is unchanged, and at those two it is the transposed membership, reversed.

@[simp]

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

Each simple reflection of the spin basis is an involution.

theorem TauCeti.DynkinType.typeDSpinReflection_involutive {n : ℕ} (i : Fin n) : Function.Involutive (typeDSpinReflection i)

The involution underlying each simple reflection of the spin basis.

The reflection formula

theorem TauCeti.DynkinType.typeDSpinWeight_typeDSpinReflection_apply {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) (s : Finset (Fin n)) : typeDSpinWeight (typeDSpinReflection i s) j = typeDSpinWeight s j - typeDSpinWeight s i * CartanMatrix.D n i j

The coordinate equation for a simple reflection on the type-Dₙ spin weights. Reflection in the i-th simple root subtracts the pairing with the i-th simple coroot, which is the i-th coordinate of the weight, times that root; in the fundamental-weight basis the root is the i-th row of the Bourbaki-numbered Cartan matrix.

theorem TauCeti.DynkinType.typeDSpinWeight_typeDSpinReflection {n : ℕ} (hn : 4 ≤ n) (i : Fin n) (s : Finset (Fin n)) : typeDSpinWeight (typeDSpinReflection i s) = typeDSpinWeight s - typeDSpinWeight s i • fun (j : Fin n) => CartanMatrix.D n i j

The functional form of TauCeti.DynkinType.typeDSpinWeight_typeDSpinReflection_apply.

@[simp]

theorem TauCeti.DynkinType.typeDSimplyConnectedRootDatum_reflection_typeDSpinWeight {n : ℕ} (hn : 4 ≤ n) (i : Fin n) (s : Finset (Fin n)) : (RootPairing.reflection (typeDSimplyConnectedRootDatum n hn) (typeDSimpleIndex n hn i)) (typeDSpinWeight s) = typeDSpinWeight (typeDSpinReflection i s)

The simple reflections of the spin basis realize reflection in the pinned type-Dₙ datum.

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

Every pairing of a type-Dₙ spin weight with a simple coroot is -1, 0, or 1, that is, every coordinate in the fundamental-weight basis is one of the three. The corresponding bound over all coroots, which is what minusculeity asks for, is not proved here.

theorem TauCeti.DynkinType.typeDSpinWeight_injective {n : ℕ} : Function.Injective typeDSpinWeight

The type-Dₙ spin weights are pairwise distinct, so the spin module is multiplicity free.

@[simp]

theorem TauCeti.DynkinType.typeDSpinReflection_eq_self_iff {n : ℕ} (i : Fin n) (s : Finset (Fin n)) : typeDSpinReflection i s = s ↔ typeDSpinWeight s i = 0

A simple reflection fixes a sign set exactly when the corresponding coordinate of its spin weight vanishes.

@[simp]

theorem TauCeti.DynkinType.even_card_typeDSpinReflection_iff {n : ℕ} (hn : 2 ≤ n) (i : Fin n) (s : Finset (Fin n)) : Even (typeDSpinReflection i s).card ↔ Even s.card

The simple reflections preserve the parity of a sign set, so each of the two half-spin families of weights is stable under all of them. The graph automorphism behaves the other way round and exchanges the two parities, by TauCeti.DynkinType.even_card_typeDSpinGraphPerm_iff.

The two Weyl orbits

theorem TauCeti.DynkinType.typeDSpinReflection_typeDSpinReflection_fork {n : ℕ} {p q : Fin n} (hp : ↑p + 2 = n) (hq : ↑q + 1 = n) (s : Finset (Fin n)) : typeDSpinReflection p (typeDSpinReflection q s) = symmDiff s {p, q}

The two fork reflections compose to the toggle of the last two signs. Their composite reverses both fork signs and leaves every other sign alone, so the reflections move a sign set inside its parity class by an arbitrary even number of sign changes.

theorem TauCeti.DynkinType.exists_typeDSpinReflections_eq_iff {n : ℕ} (hn : 2 ≤ n) (s t : Finset (Fin n)) : (∃ (l : List (Fin n)), List.foldl (fun (u : Finset (Fin n)) (j : Fin n) => typeDSpinReflection j u) s l = t) ↔ (Even s.card ↔ Even t.card)

The orbits of the simple reflections on the type-Dₙ spin basis are exactly the two half-spin parity classes. Each reflection preserves the parity of the sign set, and any two sign sets of equal parity are joined by a word of reflections. So the two half-spin families of weights are the connected components of the reflection graph on the spin weights.