The classical integral roots of type Dₙ

This file constructs the classical integral root set of type Dₙ and gives the concrete infrastructure needed to build its pinned integral root datum. The squared-length-two root type and its reflection API are rank-polymorphic. The enumeration and Bourbaki simple-root APIs require 4 ≤ n, the rank range on which TauCeti.DynkinType.Valid admits D n: the smaller ranks name no type of the classification, D 2 being reducible and D 3 being A 3.

The classical roots are the 2 * n * (n - 1) vectors ±e_a ±e_b, a < b. They are first enumerated by a sign and an ordered pair of distinct coordinates: increasing pairs represent e_a - e_b, decreasing pairs represent e_b + e_a. The enumeration puts the chain roots e_i - e_(i+1) first, followed by the fork root e_(n-2) + e_(n-1); the remaining order is explicit but mathematically immaterial.

Every integral vector of even coordinate sum, in particular every root, is expanded explicitly in the Bourbaki-numbered simple roots. Reflections are constructed directly on the set of squared-length-two vectors and proved involutive.

Main definitions and results

• TauCeti.DynkinType.TypeDRoot is the set of integral vectors of squared length two.
• TauCeti.DynkinType.typeDRootEquiv enumerates these roots by Fin (2 * n * (n - 1)).
• TauCeti.DynkinType.typeDSimpleRoot gives the Bourbaki-numbered simple roots, computed by TauCeti.DynkinType.typeDSimpleRoot_of_add_one_lt on the chain and by TauCeti.DynkinType.typeDSimpleRoot_of_not_add_one_lt at the fork.
• TauCeti.DynkinType.sum_smul_typeDSimpleRootCoordinates expands in that basis every integral vector of even coordinate sum, as every root is by TauCeti.DynkinType.even_sum_typeDRoot, and TauCeti.DynkinType.typeDSimpleRootCoordinates_eq_of_sum_smul_eq says the expansion is unique. By TauCeti.DynkinType.typeDSimpleRootCoordinates_nonneg_or_nonpos the coefficients of a root have one sign.
• TauCeti.DynkinType.mem_span_range_typeDSimpleRoot_iff: their integral span is the lattice of integral vectors of even coordinate sum.
• TauCeti.DynkinType.sum_typeDSimpleRoot gives their coordinate sums and TauCeti.DynkinType.typeDSimpleRoot_dotProduct_typeDSimpleRoot their Gram matrix, the Cartan matrix CartanMatrix.D n.
• TauCeti.DynkinType.typeDSimpleRoot_mul_transpose_self packages that Gram identity as a matrix product for determinant and scalar-extension arguments.
• TauCeti.DynkinType.det_typeDSimpleRoot_eq_two: the simple-root matrix has determinant 2.
• TauCeti.DynkinType.linearIndependent_typeDSimpleRoot_cast says that basis stays linearly independent over any ring in which 2 is right-regular; linearIndependent_typeDSimpleRoot is its case ℤ.
• TauCeti.DynkinType.typeDRootReflectionEquiv is reflection in a root, acting on the coordinates by TauCeti.DynkinType.typeDSimpleRootCoordinates_typeDRootReflection.

References

The coordinates and numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV, and Humphreys, Introduction to Lie Algebras and Representation Theory, section 12.1.

Classical roots and their enumeration

@[reducible, inline]

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

The integral vectors of squared length two. For n ≥ 2, these are exactly the classical roots ±e_a ±e_b of type Dₙ.

Equations

• TauCeti.DynkinType.TypeDRoot n = { x : Fin n → ℤ // x ⬝ᵥ x = 2 }

theorem TauCeti.DynkinType.TypeDRoot.exists_eq_single_sub_or_add_or_neg_add {n : ℕ} (x : TypeDRoot n) : ∃ (i : Fin n) (j : Fin n), i ≠ j ∧ (↑x = Pi.single i 1 - Pi.single j 1 ∨ ↑x = Pi.single i 1 + Pi.single j 1 ∨ ↑x = -(Pi.single i 1 + Pi.single j 1))

Every classical type-D root has one of the three coordinate shapes eᵢ - eⱼ, eᵢ + eⱼ, or -eᵢ - eⱼ, for distinct coordinates i and j.

The fourth apparent sign choice is a difference root with the two coordinates exchanged.

The Bourbaki order

noncomputable def TauCeti.DynkinType.typeDRootEquiv (n : ℕ) (hn : 4 ≤ n) : Fin (2 * n * (n - 1)) ≃ TypeDRoot n

Enumerate the 2 * n * (n - 1) roots of type Dₙ, with the Bourbaki simple roots first.

Equations

• TauCeti.DynkinType.typeDRootEquiv n hn = (TauCeti.DynkinType.typeDRawFinEquiv✝ n ⋯).symm.trans (TauCeti.DynkinType.typeDRawRootEquiv✝ n)

def TauCeti.DynkinType.typeDSimpleIndex (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : Fin (2 * n * (n - 1))

The i-th simple root occupies root index i.

Equations

• TauCeti.DynkinType.typeDSimpleIndex n hn i = Fin.castLE ⋯ i

@[simp]

theorem TauCeti.DynkinType.typeDSimpleIndex_val {n : ℕ} (hn : 4 ≤ n) (i : Fin n) : ↑(typeDSimpleIndex n hn i) = ↑i

The root index of the i-th simple root has value i.

theorem TauCeti.DynkinType.typeDSimpleIndex_injective {n : ℕ} (hn : 4 ≤ n) : Function.Injective (typeDSimpleIndex n hn)

Distinct simple roots occupy distinct root indices.

The Bourbaki simple roots

def TauCeti.DynkinType.typeDSimpleRoot (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : Fin n → ℤ

The Bourbaki-numbered simple roots of type Dₙ in classical orthogonal coordinates.

Equations

• TauCeti.DynkinType.typeDSimpleRoot n hn i = if h : ↑i + 1 < n then Pi.single i 1 - Pi.single ⟨↑i + 1, h⟩ 1 else Pi.single ⟨n - 2, ⋯⟩ 1 + Pi.single ⟨n - 1, ⋯⟩ 1

@[simp]

theorem TauCeti.DynkinType.typeDSimpleRoot_of_add_one_lt {n : ℕ} (hn : 4 ≤ n) {i : Fin n} (hi : ↑i + 1 < n) : typeDSimpleRoot n hn i = Pi.single i 1 - Pi.single ⟨↑i + 1, hi⟩ 1

The chain simple roots of type Dₙ, the Fin-indices 0 to n - 2: the i-th one is e_i - e_{i+1}. Here and below both the simple roots and the coordinates e_j are indexed from zero, so Fin-index i is Bourbaki node i + 1.

@[simp]

theorem TauCeti.DynkinType.typeDSimpleRoot_of_not_add_one_lt {n : ℕ} (hn : 4 ≤ n) {i : Fin n} (hi : ¬↑i + 1 < n) : typeDSimpleRoot n hn i = Pi.single ⟨n - 2, ⋯⟩ 1 + Pi.single ⟨n - 1, ⋯⟩ 1

The fork simple root of type Dₙ, the Fin-index n - 1 and so Bourbaki node n: in the zero-based coordinates it is e_{n-2} + e_{n-1}, the only simple root that is not a difference of two coordinates.

@[simp]

theorem TauCeti.DynkinType.sum_typeDSimpleRoot {n : ℕ} (hn : 4 ≤ n) (i : Fin n) : ∑ j : Fin n, typeDSimpleRoot n hn i j = if ↑i + 1 < n then 0 else 2

The coordinate sum of a Bourbaki simple root of type Dₙ: a chain root eᵢ - eᵢ₊₁ has sum zero and the fork root e_{n-2} + e_{n-1} has sum two. In particular every simple root has even coordinate sum.

theorem TauCeti.DynkinType.even_sum_typeDSimpleRoot {n : ℕ} (hn : 4 ≤ n) (i : Fin n) : Even (∑ j : Fin n, typeDSimpleRoot n hn i j)

Every simple root has even coordinate sum.

theorem TauCeti.DynkinType.even_sum_sum_smul_typeDSimpleRoot {n : ℕ} (hn : 4 ≤ n) (c : Fin n → ℤ) : Even (∑ j : Fin n, (∑ i : Fin n, c i • typeDSimpleRoot n hn i) j)

Every integral combination of the simple roots has even coordinate sum.

The Gram matrix of the Bourbaki simple roots

@[simp]

theorem TauCeti.DynkinType.typeDSimpleRoot_dotProduct_typeDSimpleRoot {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) : typeDSimpleRoot n hn i ⬝ᵥ typeDSimpleRoot n hn j = CartanMatrix.D n i j

The simple roots of type Dₙ have the Cartan matrix as Gram matrix. Type Dₙ is simply laced and its roots have squared length two, so the coroot of a root is the root itself and the Cartan integer ⟨αᵢ, αⱼ^∨⟩ is the classical dot product.

The simple-root Gram matrix is the type-D Cartan matrix.

theorem TauCeti.DynkinType.typeDSimpleRoot_mul_transpose_self {n : ℕ} (hn : 4 ≤ n) : Matrix.of (typeDSimpleRoot n hn) * (Matrix.of (typeDSimpleRoot n hn)).transpose = CartanMatrix.D n

The matrix of type-D simple roots times its transpose is the type-D Cartan matrix: the Gram identity whose determinant gives the type-D determinant-square calculation.

theorem TauCeti.DynkinType.det_cartanMatrixD_eq_det_typeDSimpleRoot_sq {n : ℕ} (hn : 4 ≤ n) : (CartanMatrix.D n).det = (Matrix.of (typeDSimpleRoot n hn)).det ^ 2

The determinant of the type-D Cartan matrix is the square of the simple-root determinant.

@[simp]

theorem TauCeti.DynkinType.det_typeDSimpleRoot_eq_two {n : ℕ} (hn : 4 ≤ n) : (Matrix.of (typeDSimpleRoot n hn)).det = 2

The simple-root matrix of type Dₙ has determinant 2.

@[simp]

theorem TauCeti.DynkinType.typeDRootEquiv_apply_typeDSimpleIndex {n : ℕ} (hn : 4 ≤ n) (i : Fin n) : ↑((typeDRootEquiv n hn) (typeDSimpleIndex n hn i)) = typeDSimpleRoot n hn i

The first n entries of typeDRootEquiv are the Bourbaki-numbered simple roots.

Coordinates in the simple-root basis

theorem TauCeti.DynkinType.even_sum_typeDRoot {n : ℕ} (x : TypeDRoot n) : Even (∑ i : Fin n, ↑x i)

The coordinate sum of a squared-length-two integral vector is even: it differs from x ⬝ᵥ x = 2 by a sum of products of consecutive integers.

def TauCeti.DynkinType.typeDSimpleRootCoordinates (n : ℕ) (hn : 4 ≤ n) (v : Fin n → ℤ) : Fin n → ℤ

The coefficients of an integral vector in the Bourbaki simple-root basis of type Dₙ. They expand the vector in that basis whenever its coordinate sum is even (TauCeti.DynkinType.sum_smul_typeDSimpleRootCoordinates), in particular for every root; for a vector of odd coordinate sum they are meaningless.

Equations

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

The doubled fundamental coweights

The coefficients of a root in the Bourbaki simple-root basis are read off the classical vector by pairing it against an explicit integral family, twice the fundamental coweights. Halving is unavoidable — the last two fundamental coweights of type Dₙ are not integral vectors — and doubling is harmless, since ℤ is torsion free. That one family does two jobs: it is a dual family for the simple roots up to the factor two, which gives their linear independence, and it exhibits twice the coefficient map as the restriction of a linear map, which shows that the coefficients expand every vector of even coordinate sum.

theorem TauCeti.DynkinType.linearIndependent_typeDSimpleRoot_cast {n : ℕ} {R : Type u_1} [Ring R] (h2 : IsRightRegular 2) (hn : 4 ≤ n) : LinearIndependent R fun (i j : Fin n) => ↑(typeDSimpleRoot n hn i j)

The Bourbaki simple roots of type Dₙ are linearly independent over any ring in which 2 is right-regular. The doubled fundamental coweights pair with them diagonally, by 2.

theorem TauCeti.DynkinType.linearIndependent_typeDSimpleRoot {n : ℕ} (hn : 4 ≤ n) : LinearIndependent ℤ (typeDSimpleRoot n hn)

The Bourbaki simple roots of type Dₙ are linearly independent over ℤ.

theorem TauCeti.DynkinType.sum_smul_typeDSimpleRootCoordinates {n : ℕ} (hn : 4 ≤ n) {v : Fin n → ℤ} (hv : Even (∑ i : Fin n, v i)) : ∑ i : Fin n, typeDSimpleRootCoordinates n hn v i • typeDSimpleRoot n hn i = v

Every integral vector of even coordinate sum, in particular every type Dₙ root, is the indicated integral combination of the Bourbaki simple roots.

theorem TauCeti.DynkinType.typeDSimpleRootCoordinates_eq_of_sum_smul_eq {n : ℕ} (hn : 4 ≤ n) {v c : Fin n → ℤ} (h : ∑ i : Fin n, c i • typeDSimpleRoot n hn i = v) : typeDSimpleRootCoordinates n hn v = c

The coefficients in the Bourbaki simple-root basis are unique: any integral expansion of a vector in the simple roots has the coefficients typeDSimpleRootCoordinates.

theorem TauCeti.DynkinType.mem_span_range_typeDSimpleRoot_iff {n : ℕ} (hn : 4 ≤ n) {v : Fin n → ℤ} : v ∈ Submodule.span ℤ (Set.range (typeDSimpleRoot n hn)) ↔ Even (∑ i : Fin n, v i)

The integral span of the simple roots is the lattice of integral vectors of even coordinate sum.

@[simp]

theorem TauCeti.DynkinType.typeDSimpleRootCoordinates_typeDSimpleRoot {n : ℕ} (hn : 4 ≤ n) (i : Fin n) : typeDSimpleRootCoordinates n hn (typeDSimpleRoot n hn i) = Pi.single i 1

The coordinates of the i-th simple root are the i-th standard basis vector.

Reflections of the concrete roots

def TauCeti.DynkinType.typeDRootReflection {n : ℕ} (u v : TypeDRoot n) : TypeDRoot n

Reflection of a type Dₙ root v in the root u.

Equations

• TauCeti.DynkinType.typeDRootReflection u v = ⟨(TauCeti.DynkinType.typeDAmbientReflection✝ u) ↑v, ⋯⟩

@[simp]

theorem TauCeti.DynkinType.typeDRootReflection_val {n : ℕ} (u v : TypeDRoot n) : ↑(typeDRootReflection u v) = ↑v - (↑v ⬝ᵥ ↑u) • ↑u

Reflection in a root acts by the classical formula on coordinates.

theorem TauCeti.DynkinType.typeDRootReflection_involutive {n : ℕ} (u : TypeDRoot n) : Function.Involutive (typeDRootReflection u)

Reflection in a type Dₙ root is involutive.

def TauCeti.DynkinType.typeDRootReflectionEquiv {n : ℕ} (u : TypeDRoot n) : TypeDRoot n ≃ TypeDRoot n

Reflection in a type Dₙ root, as an involutive permutation of all roots.

Equations

• TauCeti.DynkinType.typeDRootReflectionEquiv u = Function.Involutive.toPerm (TauCeti.DynkinType.typeDRootReflection u) ⋯

@[simp]

theorem TauCeti.DynkinType.typeDRootReflectionEquiv_apply {n : ℕ} (u v : TypeDRoot n) : (typeDRootReflectionEquiv u) v = typeDRootReflection u v

The reflection equivalence acts by typeDRootReflection.

Positivity of the coordinates

Every classical root is a nonnegative or a nonpositive integral combination of the Bourbaki simple roots. The four positive coordinate patterns are read off the two shapes of a positive root, e_a - e_b and e_a + e_b, and the negative roots follow by negating.

theorem TauCeti.DynkinType.typeDSimpleRootCoordinates_nonneg_or_nonpos {n : ℕ} (hn : 4 ≤ n) (x : TypeDRoot n) : (∀ (k : Fin n), 0 ≤ typeDSimpleRootCoordinates n hn (↑x) k) ∨ ∀ (k : Fin n), typeDSimpleRootCoordinates n hn (↑x) k ≤ 0

Every classical type Dₙ root is positive or negative. Its coefficients in the Bourbaki simple-root basis are either all nonnegative or all nonpositive, which is what makes the first n root indices a base of the pinned root datum.

theorem TauCeti.DynkinType.typeDSimpleRootCoordinates_typeDRootReflection {n : ℕ} (hn : 4 ≤ n) (u v : TypeDRoot n) : typeDSimpleRootCoordinates n hn ↑(typeDRootReflection u v) = typeDSimpleRootCoordinates n hn ↑v - (↑v ⬝ᵥ ↑u) • typeDSimpleRootCoordinates n hn ↑u

Reflection acts on the simple-root coordinates by the classical formula.