The classical model of type Cₙ in the pinned coordinates

This file sets up the coordinates in which TauCeti.DynkinType.typeCSimplyConnectedRootDatum is built, and proves everything about the roots of type Cₙ that can be said before they are indexed: the two coordinate families, the signed classical basis vectors ± e_a out of which every root is a sum of two, and the action of a reflection on those signed basis vectors.

Write e₀, …, e_{n-1} for the standard basis of the classical model ℤ ^ n, in which the roots of type Cₙ are the short roots ± e_a ± e_b with a ≠ b and the long roots ± 2 e_a, with simple roots αᵢ = eᵢ - eᵢ₊₁ for i < n - 1 and α_{n-1} = 2 e_{n-1}. The corresponding simple coroots are αᵢ^∨ = eᵢ - eᵢ₊₁ and α_{n-1}^∨ = e_{n-1}, and they are a basis of the classical lattice, which is what makes Cₙ the classical family whose whole construction stays inside the classical basis vectors: both

weight n a   = (⟨e_a, αₖ^∨⟩)ₖ         = ([a = k] - [a = k + 1])ₖ,
coweight n a = (coefficient of αₖ^∨)ₖ = ([a ≤ k])ₖ

are integral, the second because e_a = ∑ a ≤ k, αₖ^∨. Everything here is a finite calculation with these two families, resting on the single identity TauCeti.DynkinType.TypeC.weight_dotProduct_coweight, which says that the pinned pairing sees the classical pairing ⟨e_a, e_c⟩ = [a = c] exactly.

The reflection in the root p + q acts on signed basis vectors by the involution exchanging p with -q and -p with q; that is TauCeti.DynkinType.TypeC.signedReflection, and its uniformity in the shape of the root is what makes the two reflection axioms one five-case calculation rather than one case per pair of shapes. The long roots are the case p = q, where the coroot is the halved p rather than p + q, and that is the only asymmetry between the two calculations.

The domain of the pair operations

A pair (p, q) of signed basis vectors names a root only when q ≠ signedNeg p. On the excluded diagonal q = -p the sum p + q is zero, which is no root, and there is no reflection in it, so outside that hypothesis TauCeti.DynkinType.TypeC.pairRoot, TauCeti.DynkinType.TypeC.pairCoroot and TauCeti.DynkinType.TypeC.signedReflection are total functions carrying auxiliary data with no root-theoretic meaning. Every substantive lemma below accordingly assumes q ≠ signedNeg p, and the root indices of the datum are built so that the hypothesis always holds.

Main definitions

• TauCeti.DynkinType.TypeC.weight and TauCeti.DynkinType.TypeC.coweight: the character- and cocharacter-lattice coordinates of a classical basis vector.
• TauCeti.DynkinType.TypeC.pairRoot and TauCeti.DynkinType.TypeC.pairCoroot: the root p + q and its coroot, in those coordinates, for q ≠ signedNeg p.
• TauCeti.DynkinType.TypeC.signedReflection: the reflection in p + q, on signed basis vectors, for q ≠ signedNeg p.

Main results

• TauCeti.DynkinType.TypeC.span_range_weight_eq_top: the classical weights span the full character lattice in every rank.
• TauCeti.DynkinType.TypeC.signedWeight_signedReflection and TauCeti.DynkinType.TypeC.signedCoweight_signedReflection: the reflection acts as the reflection formula says it does.
• TauCeti.DynkinType.TypeC.pairRoot_reflection and TauCeti.DynkinType.TypeC.pairCoroot_reflection: the transported form of those two identities, which is what the root datum's reflection axioms consume.

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

The two coordinate families

def TauCeti.DynkinType.TypeC.weight (n a : ℕ) : Fin n → ℤ

The character-lattice coordinates of the classical basis vector e_a of type Cₙ: its pairings ⟨e_a, αₖ^∨⟩ = [a = k] - [a = k + 1] against the simple coroots.

Equations

• TauCeti.DynkinType.TypeC.weight n a k = (if a = ↑k then 1 else 0) - if a = ↑k + 1 then 1 else 0

@[simp]

theorem TauCeti.DynkinType.TypeC.weight_apply (n a : ℕ) (k : Fin n) : weight n a k = (if a = ↑k then 1 else 0) - if a = ↑k + 1 then 1 else 0

def TauCeti.DynkinType.TypeC.coweight (n a : ℕ) : Fin n → ℤ

The cocharacter-lattice coordinates of the classical basis vector e_a of type Cₙ, read off e_a = ∑ a ≤ k, αₖ^∨: the k-th coordinate is [a ≤ k].

Equations

• TauCeti.DynkinType.TypeC.coweight n a k = if a ≤ ↑k then 1 else 0

@[simp]

theorem TauCeti.DynkinType.TypeC.coweight_apply (n a : ℕ) (k : Fin n) : coweight n a k = if a ≤ ↑k then 1 else 0

theorem TauCeti.DynkinType.TypeC.coweight_eq_zero_of_le {n a : ℕ} (ha : n ≤ a) : coweight n a = 0

theorem TauCeti.DynkinType.TypeC.weight_dotProduct_coweight {n a c : ℕ} (ha : a < n) : weight n a ⬝ᵥ coweight n c = if a = c then 1 else 0

The fundamental pairing identity of type Cₙ: the two pinned lattices see the classical pairing ⟨e_a, e_c⟩ = [a = c] exactly, with no correction term, because the simple coroots of Cₙ are a basis of the classical lattice.

Generation of the character lattice

theorem TauCeti.DynkinType.TypeC.span_range_weight_eq_top (n : ℕ) : Submodule.span ℤ (Set.range fun (a : Fin n) => weight n ↑a) = ⊤

The classical type-Cₙ weights generate the full character lattice. Each standard coordinate character is the partial sum of the weights through that coordinate.

Signed basis vectors

@[reducible, inline]

abbrev TauCeti.DynkinType.TypeC.Signed (n : ℕ) : Type

A signed classical basis vector ± e_a, the atom out of which every root of type Cₙ is built as a sum of two.

Equations

• TauCeti.DynkinType.TypeC.Signed n = (Fin n × Bool)

def TauCeti.DynkinType.TypeC.signedNeg {n : ℕ} (x : Signed n) : Signed n

The opposite ∓ e_a of a signed basis vector.

Equations

• TauCeti.DynkinType.TypeC.signedNeg x = (x.1, !x.2)

@[simp]

theorem TauCeti.DynkinType.TypeC.signedNeg_mk {n : ℕ} (a : Fin n) (s : Bool) : signedNeg (a, s) = (a, !s)

@[simp]

theorem TauCeti.DynkinType.TypeC.signedNeg_signedNeg {n : ℕ} (x : Signed n) : signedNeg (signedNeg x) = x

theorem TauCeti.DynkinType.TypeC.signedNeg_ne {n : ℕ} (x : Signed n) : signedNeg x ≠ x

theorem TauCeti.DynkinType.TypeC.ne_signedNeg_of_ne_signedNeg {n : ℕ} {x y : Signed n} (h : y ≠ signedNeg x) : x ≠ signedNeg y

def TauCeti.DynkinType.TypeC.signedWeight {n : ℕ} (x : Signed n) : Fin n → ℤ

The character-lattice coordinates of a signed basis vector.

Equations

• TauCeti.DynkinType.TypeC.signedWeight x = if x.2 = true then -TauCeti.DynkinType.TypeC.weight n ↑x.1 else TauCeti.DynkinType.TypeC.weight n ↑x.1

def TauCeti.DynkinType.TypeC.signedCoweight {n : ℕ} (x : Signed n) : Fin n → ℤ

The cocharacter-lattice coordinates of a signed basis vector.

Equations

• TauCeti.DynkinType.TypeC.signedCoweight x = if x.2 = true then -TauCeti.DynkinType.TypeC.coweight n ↑x.1 else TauCeti.DynkinType.TypeC.coweight n ↑x.1

@[simp]

theorem TauCeti.DynkinType.TypeC.signedWeight_false {n : ℕ} (a : Fin n) : signedWeight (a, false) = weight n ↑a

@[simp]

theorem TauCeti.DynkinType.TypeC.signedWeight_true {n : ℕ} (a : Fin n) : signedWeight (a, true) = -weight n ↑a

@[simp]

theorem TauCeti.DynkinType.TypeC.signedCoweight_false {n : ℕ} (a : Fin n) : signedCoweight (a, false) = coweight n ↑a

@[simp]

theorem TauCeti.DynkinType.TypeC.signedCoweight_true {n : ℕ} (a : Fin n) : signedCoweight (a, true) = -coweight n ↑a

@[simp]

theorem TauCeti.DynkinType.TypeC.signedWeight_signedNeg {n : ℕ} (x : Signed n) : signedWeight (signedNeg x) = -signedWeight x

@[simp]

theorem TauCeti.DynkinType.TypeC.signedCoweight_signedNeg {n : ℕ} (x : Signed n) : signedCoweight (signedNeg x) = -signedCoweight x

theorem TauCeti.DynkinType.TypeC.signedWeight_dotProduct_signedCoweight {n : ℕ} (x y : Signed n) : signedWeight x ⬝ᵥ signedCoweight y = if x = y then 1 else if x = signedNeg y then -1 else 0

The pinned pairing of two signed basis vectors: 1 on the diagonal, -1 on opposites, and 0 otherwise.

theorem TauCeti.DynkinType.TypeC.signedWeight_dotProduct_self {n : ℕ} (x : Signed n) : signedWeight x ⬝ᵥ signedCoweight x = 1

theorem TauCeti.DynkinType.TypeC.signedWeight_dotProduct_nonpos {n : ℕ} {x y : Signed n} (h : x ≠ y) : signedWeight x ⬝ᵥ signedCoweight y ≤ 0

theorem TauCeti.DynkinType.TypeC.signedWeight_dotProduct_nonneg {n : ℕ} {x y : Signed n} (h : x ≠ signedNeg y) : 0 ≤ signedWeight x ⬝ᵥ signedCoweight y

theorem TauCeti.DynkinType.TypeC.signedWeight_dotProduct_eq_zero {n : ℕ} {x y : Signed n} (h : x ≠ y) (h' : x ≠ signedNeg y) : signedWeight x ⬝ᵥ signedCoweight y = 0

theorem TauCeti.DynkinType.TypeC.eq_of_signedWeight_dotProduct_eq_one {n : ℕ} {x y : Signed n} (h : signedWeight x ⬝ᵥ signedCoweight y = 1) : x = y

theorem TauCeti.DynkinType.TypeC.signedWeight_injective {n : ℕ} : Function.Injective signedWeight

Roots and coroots of a pair of signed basis vectors

def TauCeti.DynkinType.TypeC.pairRoot {n : ℕ} (x y : Signed n) : Fin n → ℤ

The root p + q attached to a pair of signed basis vectors, in fundamental-weight coordinates.

This is a root only under y ≠ signedNeg x; on the excluded diagonal y = -x the value is 0, which is no root.

Equations

• TauCeti.DynkinType.TypeC.pairRoot x y = TauCeti.DynkinType.TypeC.signedWeight x + TauCeti.DynkinType.TypeC.signedWeight y

theorem TauCeti.DynkinType.TypeC.pairRoot_def {n : ℕ} (x y : Signed n) : pairRoot x y = signedWeight x + signedWeight y

def TauCeti.DynkinType.TypeC.pairCoroot {n : ℕ} (x y : Signed n) : Fin n → ℤ

The coroot of the root p + q, in simple-coroot coordinates. It is p + q again for the short roots p ≠ q, and the halved p for the long roots p = q.

This is the coroot of a root only under y ≠ signedNeg x; on the excluded diagonal y = -x there is no root x + y and the value here is auxiliary data.

Equations

• TauCeti.DynkinType.TypeC.pairCoroot x y = if x = y then TauCeti.DynkinType.TypeC.signedCoweight x else TauCeti.DynkinType.TypeC.signedCoweight x + TauCeti.DynkinType.TypeC.signedCoweight y

@[simp]

theorem TauCeti.DynkinType.TypeC.pairCoroot_self {n : ℕ} (x : Signed n) : pairCoroot x x = signedCoweight x

@[simp]

theorem TauCeti.DynkinType.TypeC.pairCoroot_of_ne {n : ℕ} {x y : Signed n} (h : x ≠ y) : pairCoroot x y = signedCoweight x + signedCoweight y

theorem TauCeti.DynkinType.TypeC.pairRoot_comm {n : ℕ} (x y : Signed n) : pairRoot x y = pairRoot y x

theorem TauCeti.DynkinType.TypeC.pairCoroot_comm {n : ℕ} (x y : Signed n) : pairCoroot x y = pairCoroot y x

theorem TauCeti.DynkinType.TypeC.pairRoot_dotProduct_pairCoroot_self {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : pairRoot p q ⬝ᵥ pairCoroot p q = 2

theorem TauCeti.DynkinType.TypeC.abs_pairRoot_dotProduct_pairCoroot_le_two {n : ℕ} {x y p q : Signed n} (hpq : q ≠ signedNeg p) : |pairRoot x y ⬝ᵥ pairCoroot p q| ≤ 2

Cartan integers between roots in the classical type C model have absolute value at most two.

theorem TauCeti.DynkinType.TypeC.one_le_dotProduct_pairCoroot_iff {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (z : Signed n) : 1 ≤ signedWeight z ⬝ᵥ pairCoroot p q ↔ z = p ∨ z = q

A signed basis vector pairs to at least 1 with the coroot of p + q exactly when it is p or q. This is the recognition principle behind injectivity of the roots and coroots.

theorem TauCeti.DynkinType.TypeC.one_le_pairRoot_dotProduct_iff {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (z : Signed n) : 1 ≤ pairRoot p q ⬝ᵥ signedCoweight z ↔ z = p ∨ z = q

The root half of TauCeti.DynkinType.TypeC.one_le_dotProduct_pairCoroot_iff.

The reflection on signed basis vectors

def TauCeti.DynkinType.TypeC.signedReflection {n : ℕ} (p q z : Signed n) : Signed n

Reflection in the root p + q, acting on signed basis vectors: it exchanges p with -q and -p with q, and fixes everything else. On a long root p = q the two exchanges coincide and this is the sign change at the index of p.

This is the reflection in a root only under q ≠ signedNeg p, the hypothesis of every lemma below; on the excluded diagonal q = -p there is no root p + q to reflect in and the value here is auxiliary data.

Equations

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

@[simp]

theorem TauCeti.DynkinType.TypeC.signedReflection_left {n : ℕ} (p q : Signed n) : signedReflection p q p = signedNeg q

@[simp]

theorem TauCeti.DynkinType.TypeC.signedReflection_signedNeg_right {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : signedReflection p q (signedNeg q) = p

@[simp]

theorem TauCeti.DynkinType.TypeC.signedReflection_signedNeg_left {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : signedReflection p q (signedNeg p) = q

@[simp]

theorem TauCeti.DynkinType.TypeC.signedReflection_right {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : signedReflection p q q = signedNeg p

@[simp]

theorem TauCeti.DynkinType.TypeC.signedReflection_of_ne {n : ℕ} {p q z : Signed n} (h1 : z ≠ p) (h2 : z ≠ q) (h3 : z ≠ signedNeg p) (h4 : z ≠ signedNeg q) : signedReflection p q z = z

The pairings of a root and its coroot against a signed basis vector

theorem TauCeti.DynkinType.TypeC.dotProduct_pairCoroot_left {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : signedWeight p ⬝ᵥ pairCoroot p q = 1

theorem TauCeti.DynkinType.TypeC.dotProduct_pairCoroot_right {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : signedWeight q ⬝ᵥ pairCoroot p q = 1

theorem TauCeti.DynkinType.TypeC.dotProduct_pairCoroot_of_ne {n : ℕ} {p q z : Signed n} (h1 : z ≠ p) (h2 : z ≠ q) (h3 : z ≠ signedNeg p) (h4 : z ≠ signedNeg q) : signedWeight z ⬝ᵥ pairCoroot p q = 0

theorem TauCeti.DynkinType.TypeC.pairRoot_dotProduct_of_ne {n : ℕ} {p q z : Signed n} (h1 : z ≠ p) (h2 : z ≠ q) (h3 : z ≠ signedNeg p) (h4 : z ≠ signedNeg q) : pairRoot p q ⬝ᵥ signedCoweight z = 0

theorem TauCeti.DynkinType.TypeC.signedWeight_signedReflection {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (z : Signed n) : signedWeight (signedReflection p q z) = signedWeight z - (signedWeight z ⬝ᵥ pairCoroot p q) • pairRoot p q

The reflection in a root acts on signed basis vectors. This is the whole content of the reflection axiom for the roots, and it is uniform in the shapes of both roots involved: the same five-case calculation covers the short and the long reflecting root.

theorem TauCeti.DynkinType.TypeC.signedCoweight_signedReflection {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (z : Signed n) : signedCoweight (signedReflection p q z) = signedCoweight z - (pairRoot p q ⬝ᵥ signedCoweight z) • pairCoroot p q

The coroot half of TauCeti.DynkinType.TypeC.signedWeight_signedReflection. The long reflecting root is a genuine second case here, its coroot being the halved one.

theorem TauCeti.DynkinType.TypeC.signedReflection_injective {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) : Function.Injective (signedReflection p q)

theorem TauCeti.DynkinType.TypeC.signedReflection_signedNeg {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (z : Signed n) : signedReflection p q (signedNeg z) = signedNeg (signedReflection p q z)

theorem TauCeti.DynkinType.TypeC.pairRoot_reflection {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (x y : Signed n) : pairRoot x y - (pairRoot x y ⬝ᵥ pairCoroot p q) • pairRoot p q = pairRoot (signedReflection p q x) (signedReflection p q y)

Reflection in the root p + q transports the root of a pair to the root of the reflected pair.

theorem TauCeti.DynkinType.TypeC.pairCoroot_reflection {n : ℕ} {p q : Signed n} (h : q ≠ signedNeg p) (x y : Signed n) : pairCoroot x y - (pairRoot p q ⬝ᵥ pairCoroot x y) • pairCoroot p q = pairCoroot (signedReflection p q x) (signedReflection p q y)

The coroot half of TauCeti.DynkinType.TypeC.pairRoot_reflection.