The pinned coordinate model of the roots of type Bₙ #
This file records the roots of type Bₙ in the two lattices pinned by the Bourbaki numbering: the
character lattice Fin n → ℤ written in the fundamental-weight basis, and the cocharacter lattice
Fin n → ℤ written in the simple-coroot basis. It stops just short of assembling a RootDatum,
which is done in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.B.Datum once the roots
have been enumerated by Fin (2 * n ^ 2).
The coordinates #
Write e₀, …, e_{n-1} for the standard basis of the classical model ℤ ^ n, in which the roots of
type Bₙ are the 2 * n ^ 2 vectors ± e_a ± e_b (a ≠ b) and ± e_a, the simple roots are
αᵢ = eᵢ - eᵢ₊₁ for i + 1 < n and α_{n-1} = e_{n-1}, and the coroot of a root α is
2 α / (α, α), so the long roots are self-dual while (± e_a)^∨ = ± 2 e_a. Everything below is the
image of that model in the two pinned lattices:
weight n a = (⟨e_a, αₖ^∨⟩)ₖ, the character coordinates of `e_a`,
coweight n b = the simple-coroot coordinates of `2 e_b`.
The doubling in coweight is not a normalisation: e_b itself is a half-integral combination of
the simple coroots, because α_{n-1}^∨ = 2 e_{n-1}, while 2 e_b is integral. The single identity
TauCeti.DynkinType.TypeB.weight_dotProduct_coweight, that the two families pair to 2 * [a = b],
is what the rest of the file computes with.
Signed basis vectors and the pairs naming a root #
A root is a sum of one or two signed basis vectors on distinct axes, so Fin (2 * n) indexes the
signed basis vectors, u < n standing for e_u and u ≥ n for -e_{u-n}, and a root is named by
an unordered pair {u, v}, with u = v for a short root. Two devices make this uniform.
The cyclic offset TauCeti.DynkinType.TypeB.shift turns the unordered pair into the ordered datum
(u, d) : Fin (2 * n) × Fin n. For a distinct admissible pair, exactly one of the two orders has
its offset in the range Fin n; a short root uses the coincident order with offset zero. This is
the index type the datum is built on, and TauCeti.DynkinType.TypeB.index is the inverse
normalisation.
The coroot is uniform in the pair while the root is not:
TauCeti.DynkinType.TypeB.corootOfPair computes
the simple-coroot coordinates of the coroot from the pair, and specialises to the short coroot when
the two entries agree, since (e_a)^∨ = 2 e_a = e_a + e_a. It is a genuine half, and the integral
identity TauCeti.DynkinType.TypeB.corootOfPair_add_self is how the reflection identity for
coroots is proved.
Main definitions #
TauCeti.DynkinType.TypeB.signedWeightandTauCeti.DynkinType.TypeB.signedCoweight: the coordinates of a signed basis vector and of its double.TauCeti.DynkinType.TypeB.rootOfPairandTauCeti.DynkinType.TypeB.corootOfPair: the root and coroot named by a pair of signed basis vectors.TauCeti.DynkinType.TypeB.reflMap: the signed permutation realising the reflection in a root.
The coordinate definitions are used through their defining and case-characterization lemmas below; their bodies are not exposed to importing modules.
Main results #
TauCeti.DynkinType.TypeB.signedWeight_reflMapandTauCeti.DynkinType.TypeB.signedCoweight_reflMap: the reflection formulas on a single signed basis vector, from which the root-datum axioms follow additively.TauCeti.DynkinType.TypeB.index_eq_of_pair_mem_iff: an index is recovered from its unordered signed-vector pair.
References #
The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters
4--6, Plate II, and Humphreys, Introduction to Lie Algebras and Representation Theory, section
12.1. This is part of the Bₙ branch of the target "a named datum per valid type" in Layer 6 of
TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.
The two coordinate families #
The character-lattice coordinates of the classical basis vector e_a of type Bₙ, namely its
pairings ⟨e_a, αₖ^∨⟩ against the simple coroots. The last simple coroot is 2 e_{n-1}, which is
why the diagonal entry doubles there. The value is 0 for n ≤ a, where there is no basis
vector.
Equations
Instances For
The cocharacter-lattice coordinates of 2 e_b, that is, its coordinates in the simple coroots
αₖ^∨ = e_k - e_{k+1} and α_{n-1}^∨ = 2 e_{n-1}. The vector e_b alone is half-integral in that
basis, so it is its double that is recorded.
Equations
Instances For
Signed basis vectors #
The character coordinates of the signed basis vector indexed by u.
Equations
Instances For
The cocharacter coordinates of twice the signed basis vector indexed by u.
Equations
Instances For
The pairing of two signed basis vectors: 2 on the diagonal, -2 on opposite vectors, and 0
on different axes.
The coroot attached to a pair of signed basis vectors #
The simple-coroot coordinates of the coroot named by the pair {u, v}: the half of
signedCoweight u + signedCoweight v, which is integral. When u = v this is the short coroot
signedCoweight u, and otherwise it is the long coroot ± e_a ± e_b itself.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integral form of the halving.
Cyclic offsets and the index of a pair #
A pair of signed basis vectors naming a root: either equal, for a short root, or on distinct axes, for a long root.
Equations
Instances For
The canonical index in Fin (2 * n) × Fin n of the root named by a pair of signed basis
vectors. For a distinct admissible pair it uses the unique order whose cyclic offset lies in
Fin n; a short pair uses the coincident order with offset zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Roots and coroots #
The character coordinates of the root named by a pair of signed basis vectors.
Equations
Instances For
The reflection in a root #
The signed permutation of the basis vectors realising the reflection in the root named by the
pair {p, q}. On a long root it exchanges p with -q and q with -p; on a short root, where
p = q, it is the sign change on the axis of p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The reflection formula on a single signed basis vector.
The reflection formula on the double of a single signed basis vector.