The simply connected root datum of type Bₙ

This file assembles the coordinate model of TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.B.Model into the pinned integral root datum of type Bₙ, uniformly in the rank n, on the character and cocharacter lattices Fin n → ℤ. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis, so the i-th simple root is the i-th row of the Bourbaki-numbered Cartan matrix CartanMatrix.B n and the i-th simple coroot is the i-th standard basis vector.

The enumeration

The roots are indexed by Fin (2 * n ^ 2), which is TauCeti.DynkinType.numRoots (.B n). The model names a root by a signed basis vector u together with a cyclic offset d, so the raw index type is Fin (2 * n) × Fin n; the enumeration rotates the first coordinate and reverses the second so that the Bourbaki simple roots come first. All but the last simple root are long and the last one is short, so they cannot occupy a single block of a product enumeration: the rotation puts α₀, …, α_{n-2} at indices 0, …, n - 2 and sends the short α_{n-1} elsewhere, and a single transposition then brings that one to index n - 1.

Only the coroots are asked to span their lattice, and only that half is recorded, in TauCeti.DynkinType.corootSpan_typeBSimplyConnectedRootDatum_eq_top. The roots span the root lattice, which for 0 < n sits inside the weight lattice with index 2 (Bourbaki, Plate II); at n = 0 both lattices are trivial and the two coincide. So the datum is a RootDatum carrying no RootPairing.IsRootSystem instance. That asymmetry is what "simply connected" means here.

Main definitions

• TauCeti.DynkinType.typeBSimplyConnectedRootDatum: the pinned root datum of type Bₙ.
• TauCeti.DynkinType.typeBSimpleIndex: the first n root indices, the Bourbaki-numbered simple roots.
• TauCeti.DynkinType.typeBSimplyConnectedBase: the base they form.

Nothing here is @[expose]d: the datum, its enumeration and its base are used through the lemmas below, not by unfolding.

Main results

• TauCeti.DynkinType.root_typeBSimpleIndex and TauCeti.DynkinType.coroot_typeBSimpleIndex: the i-th simple root is the i-th row of CartanMatrix.B n and the i-th simple coroot is Pi.single i 1, which is what pins the two lattices as the weight and coroot lattices.
• TauCeti.DynkinType.hasCartanType_typeBSimplyConnectedRootDatum: the pinned base has Cartan type B n.
• TauCeti.DynkinType.corootSpan_typeBSimplyConnectedRootDatum_eq_top: the coroots span the cocharacter lattice, the simply connected condition.

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 the Bₙ branch of the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.

Reading off the coordinates of an explicit signed basis vector

The reflection permutation on the raw index type

The enumeration of the roots

def TauCeti.DynkinType.typeBSimpleIndex (n : ℕ) (i : Fin n) : Fin (2 * n ^ 2)

The i-th simple root of type Bₙ sits at root index i, the Bourbaki node i + 1.

Equations

• TauCeti.DynkinType.typeBSimpleIndex n i = Fin.castLE ⋯ i

@[simp]

theorem TauCeti.DynkinType.typeBSimpleIndex_val {n : ℕ} (i : Fin n) : ↑(typeBSimpleIndex n i) = ↑i

theorem TauCeti.DynkinType.typeBSimpleIndex_injective {n : ℕ} : Function.Injective (typeBSimpleIndex n)

The root datum

def TauCeti.DynkinType.typeBSimplyConnectedRootDatum (n : ℕ) : RootDatum (Fin (2 * n ^ 2)) (Fin n → ℤ) (Fin n → ℤ)

The pinned simply connected root datum of type Bₙ.

Both lattices are Fin n → ℤ: the character lattice in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. The 2 * n ^ 2 roots are the classical ± e_a ± e_b and ± e_a, enumerated with the simple roots first; see TauCeti.DynkinType.root_typeBSimpleIndex.

Equations

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

@[simp]

theorem TauCeti.DynkinType.toLinearMap_typeBSimplyConnectedRootDatum {n : ℕ} (x y : Fin n → ℤ) : ((typeBSimplyConnectedRootDatum n).toLinearMap x) y = x ⬝ᵥ y

The pinned pairing is the classical dot product, in both the fundamental-weight and the simple-coroot coordinates.

theorem TauCeti.DynkinType.abs_pairing_typeBSimplyConnectedRootDatum_le_two {n : ℕ} (k l : Fin (2 * n ^ 2)) : |RootPairing.pairing (typeBSimplyConnectedRootDatum n) k l| ≤ 2

Every Cartan integer between roots of the pinned type B datum has absolute value at most two.

theorem TauCeti.DynkinType.mem_range_root_typeBSimplyConnectedRootDatum_iff {n : ℕ} {x : Fin n → ℤ} : x ∈ Set.range ⇑(typeBSimplyConnectedRootDatum n).root ↔ ∃ (u : Fin (2 * n)) (v : Fin (2 * n)), TypeB.IsPair u v ∧ x = TypeB.rootOfPair u v

The roots of the pinned type Bₙ datum are exactly the roots constructed from admissible unordered pairs of signed basis vectors.

theorem TauCeti.DynkinType.mem_range_coroot_typeBSimplyConnectedRootDatum_iff {n : ℕ} {x : Fin n → ℤ} : x ∈ Set.range ⇑(typeBSimplyConnectedRootDatum n).coroot ↔ ∃ (u : Fin (2 * n)) (v : Fin (2 * n)), TypeB.IsPair u v ∧ x = TypeB.corootOfPair u v

The coroots of the pinned type Bₙ datum are exactly the coroots constructed from admissible unordered pairs of signed basis vectors.

The simple roots and coroots

@[simp]

theorem TauCeti.DynkinType.root_typeBSimpleIndex {n : ℕ} (i : Fin n) : (typeBSimplyConnectedRootDatum n).root (typeBSimpleIndex n i) = fun (k : Fin n) => CartanMatrix.B n i k

The simple roots are the rows of the Cartan matrix. In the fundamental-weight basis the i-th simple root of the pinned type Bₙ datum is the i-th row of CartanMatrix.B n, which is what pins the character lattice as the weight lattice.

@[simp]

theorem TauCeti.DynkinType.coroot_typeBSimpleIndex {n : ℕ} (i : Fin n) : (typeBSimplyConnectedRootDatum n).coroot (typeBSimpleIndex n i) = Pi.single i 1

The simple coroots are the standard basis. This is what pins the cocharacter lattice as the coroot lattice, so that the datum is the simply connected one.

The pinned base

def TauCeti.DynkinType.typeBSimplyConnectedBase (n : ℕ) : RootPairing.Base (typeBSimplyConnectedRootDatum n)

The Bourbaki-numbered base of the pinned simply connected root datum of type Bₙ. Its support is the set of the first n root indices, carrying the simple roots in Bourbaki order.

Equations

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

@[simp]

theorem TauCeti.DynkinType.mem_typeBSimplyConnectedBase_support {n : ℕ} {k : Fin (2 * n ^ 2)} : k ∈ (typeBSimplyConnectedBase n).support ↔ ↑k < n

Membership in the pinned base support is exactly membership among the first n root indices.

@[simp]

theorem TauCeti.DynkinType.pairing_typeBSimpleIndex {n : ℕ} (i j : Fin n) : RootPairing.pairing (typeBSimplyConnectedRootDatum n) (typeBSimpleIndex n i) (typeBSimpleIndex n j) = CartanMatrix.B n i j

The pairing of two Bourbaki-indexed simple roots and coroots is the corresponding entry of the type-B Cartan matrix.

theorem TauCeti.DynkinType.hasCartanType_typeBSimplyConnectedRootDatum (n : ℕ) : HasCartanType (typeBSimplyConnectedRootDatum n) (typeBSimplyConnectedBase n) (B n)

The pinned datum of type Bₙ has Cartan type B n. Its Bourbaki-numbered base realizes the standard Cartan matrix CartanMatrix.B n, with the node numbering of TauCeti.DynkinType.

theorem TauCeti.DynkinType.corootSpan_typeBSimplyConnectedRootDatum_eq_top (n : ℕ) : RootPairing.corootSpan (typeBSimplyConnectedRootDatum n) ℤ = ⊤

The coroots of the pinned type Bₙ datum span the cocharacter lattice. This is the simply connected lattice condition required by the pinned Chevalley--Demazure construction. Its counterpart for the roots is deliberately absent: they span the root lattice, which for 0 < n sits inside the weight lattice with index 2 (Bourbaki, Plate II), the degenerate rank n = 0 being the only case where the two lattices agree.