The simply connected root datum of type Cₙ

This file constructs, uniformly in the rank n, the pinned integral root datum of type Cₙ 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.C n and the i-th simple coroot is the i-th standard basis vector. The coordinates themselves, and the action of a reflection on the signed classical basis vectors ± e_a out of which every root of type Cₙ is a sum of two, are TauCeti.DynkinType.TypeC in the imported model file.

The roots and their enumeration

A root index (a, b, s) : Fin n × Fin n × Bool denotes the pair of signed basis vectors p = (a, s) and q = (b, s) with the sign of q flipped exactly when a < b; equivalently the root is (-1) ^ s * (e_a + e_b) when b ≤ a, including the long root when b = a, and (-1) ^ s * (e_a - e_b) when a < b. Every root arises from exactly one index, and typeCMk names the index belonging to a given pair, which is how the reflected pair is turned back into an index. typeCIndexEquiv encodes a root index as an index of the datum, and root_typeCIndexEquiv_of_lt and its companions read off the root and the coroot there.

The roots are enumerated by Fin (2 * n ^ 2) by the first index a fastest, so that the first n indices are the simple roots α₀, …, α_{n-1} in Bourbaki order, as root_typeCSimpleIndex records. The b of the a-th simple root is the clamped successor Order.succ a, that is min (a + 1) (n - 1), which is a + 1 except at the last node, where the simple root is the long root 2 e_{n-1}; Equiv.swap moves that successor to the first slot of the enumeration.

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

Main definitions

• TauCeti.DynkinType.typeCSimplyConnectedRootDatum: the pinned root datum of type Cₙ.
• TauCeti.DynkinType.TypeCIndex and TauCeti.DynkinType.typeCIndexEquiv: the root index (a, b, s) and its pinned encoding as an index of the datum.
• TauCeti.DynkinType.typeCSimpleIndex: the first n root indices, the Bourbaki-numbered simple roots.
• TauCeti.DynkinType.typeCSimplyConnectedBase: the base they form.

Main results

• TauCeti.DynkinType.root_typeCIndexEquiv_of_lt and its four companions: which classical vector the root and the coroot of the datum at an encoded index are.
• TauCeti.DynkinType.root_typeCSimpleIndex and TauCeti.DynkinType.coroot_typeCSimpleIndex: the i-th simple root is the i-th row of CartanMatrix.C 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.mem_support_typeCSimplyConnectedBase: the support of the pinned base is the set of the first n root indices.
• TauCeti.DynkinType.hasCartanType_typeCSimplyConnectedRootDatum: the pinned base has Cartan type C n.
• TauCeti.DynkinType.corootSpan_typeCSimplyConnectedRootDatum_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 III, and Humphreys, Introduction to Lie Algebras and Representation Theory, section 12.1. This is the Cₙ branch of the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.

The root index type

@[reducible, inline]

abbrev TauCeti.DynkinType.TypeCIndex (n : ℕ) : Type

A root index (a, b, s) of type Cₙ: it denotes the pair of signed basis vectors (a, s) and (b, s), the sign of the second being flipped exactly when a < b. Thus the root is (-1) ^ s * (e_a + e_b) when b ≤ a, including the long root (-1) ^ s * 2 e_a when b = a, and (-1) ^ s * (e_a - e_b) when a < b.

Equations

• TauCeti.DynkinType.TypeCIndex n = (Fin n × Fin n × Bool)

Injectivity of the roots and of the coroots

The reflection on root indices

The Bourbaki enumeration of the roots

def TauCeti.DynkinType.typeCIndexEquiv (n : ℕ) : TypeCIndex n ≃ Fin (2 * n ^ 2)

The pinned enumeration of the roots of type Cₙ by Fin (2 * n ^ 2).

Equations

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

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

The pinned simply connected root datum of type Cₙ.

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 ± 2 e_a, enumerated with the simple roots first; see TauCeti.DynkinType.root_typeCSimpleIndex.

Equations

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

@[simp]

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

The pinned pairing of type Cₙ is the dot product of the two lattices.

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

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

The root and the coroot at an arbitrary index

Away from the simple indices, a root of the datum is named by encoding a root index with typeCIndexEquiv, and the five lemmas below say which vector the encoded index denotes. Together they cover every index, since typeCIndexEquiv is a bijection.

@[simp]

theorem TauCeti.DynkinType.root_typeCIndexEquiv_of_lt {n : ℕ} {a b : Fin n} (h : a < b) (s : Bool) : (typeCSimplyConnectedRootDatum n).root ((typeCIndexEquiv n) (a, b, s)) = TypeC.signedWeight (a, s) - TypeC.signedWeight (b, s)

The root at the encoded index (a, b, s) with a < b: the short root ± (e_a - e_b).

@[simp]

theorem TauCeti.DynkinType.root_typeCIndexEquiv_of_not_lt {n : ℕ} {a b : Fin n} (h : ¬a < b) (s : Bool) : (typeCSimplyConnectedRootDatum n).root ((typeCIndexEquiv n) (a, b, s)) = TypeC.signedWeight (a, s) + TypeC.signedWeight (b, s)

The root at the encoded index (a, b, s) with b ≤ a: the short root ± (e_a + e_b), and the long root ± 2 e_a on the diagonal b = a.

@[simp]

theorem TauCeti.DynkinType.coroot_typeCIndexEquiv_of_lt {n : ℕ} {a b : Fin n} (h : a < b) (s : Bool) : (typeCSimplyConnectedRootDatum n).coroot ((typeCIndexEquiv n) (a, b, s)) = TypeC.signedCoweight (a, s) - TypeC.signedCoweight (b, s)

The coroot at the encoded index (a, b, s) with a < b, that of a short root: the root itself, in the cocharacter coordinates.

@[simp]

theorem TauCeti.DynkinType.coroot_typeCIndexEquiv_of_gt {n : ℕ} {a b : Fin n} (h : b < a) (s : Bool) : (typeCSimplyConnectedRootDatum n).coroot ((typeCIndexEquiv n) (a, b, s)) = TypeC.signedCoweight (a, s) + TypeC.signedCoweight (b, s)

The coroot at the encoded index (a, b, s) with b < a, that of a short root: the root itself, in the cocharacter coordinates.

@[simp]

theorem TauCeti.DynkinType.coroot_typeCIndexEquiv_diag {n : ℕ} (a : Fin n) (s : Bool) : (typeCSimplyConnectedRootDatum n).coroot ((typeCIndexEquiv n) (a, a, s)) = TypeC.signedCoweight (a, s)

The coroot at the encoded diagonal index (a, a, s), that of the long root ± 2 e_a: the halved ± e_a.

The simple roots and coroots

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

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

Equations

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

@[simp]

theorem TauCeti.DynkinType.typeCSimpleIndex_val {n : ℕ} (i : Fin n) : ↑(typeCSimpleIndex n i) = ↑i

theorem TauCeti.DynkinType.typeCSimpleIndex_injective {n : ℕ} : Function.Injective (typeCSimpleIndex n)

@[simp]

theorem TauCeti.DynkinType.root_typeCSimpleIndex {n : ℕ} (i : Fin n) : (typeCSimplyConnectedRootDatum n).root (typeCSimpleIndex n i) = fun (k : Fin n) => CartanMatrix.C 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 Cₙ datum is the i-th row of CartanMatrix.C n, which is what pins the character lattice as the weight lattice.

@[simp]

theorem TauCeti.DynkinType.coroot_typeCSimpleIndex {n : ℕ} (i : Fin n) : (typeCSimplyConnectedRootDatum n).coroot (typeCSimpleIndex 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.typeCSimplyConnectedBase (n : ℕ) : RootPairing.Base (typeCSimplyConnectedRootDatum n)

The Bourbaki-numbered base of the pinned simply connected root datum of type Cₙ. 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_support_typeCSimplyConnectedBase {n : ℕ} {k : Fin (2 * n ^ 2)} : k ∈ (typeCSimplyConnectedBase n).support ↔ ↑k < n

The support of the pinned base of type Cₙ is the set of the first n root indices, which by TauCeti.DynkinType.root_typeCSimpleIndex carry the simple roots in Bourbaki order.

theorem TauCeti.DynkinType.hasCartanType_typeCSimplyConnectedRootDatum (n : ℕ) : HasCartanType (typeCSimplyConnectedRootDatum n) (typeCSimplyConnectedBase n) (C n)

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

theorem TauCeti.DynkinType.corootSpan_typeCSimplyConnectedRootDatum_eq_top (n : ℕ) : RootPairing.corootSpan (typeCSimplyConnectedRootDatum n) ℤ = ⊤

The coroots of the pinned type Cₙ 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 sits inside the weight lattice with index 2 whenever 0 < n (Bourbaki, Plate III; at n = 0 both lattices are trivial).