Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.D.Basic

The simply connected root datum of type Dₙ #

This file constructs, uniformly in the rank n ≥ 4, the pinned integral root datum of type Dₙ 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.D n and the i-th simple coroot is the i-th standard basis vector.

The coordinates #

Simple roots and coordinates alike are indexed from zero throughout: the simple root αᵢ is Bourbaki node i + 1, and e_j is the zero-based coordinate j, so what is called α_{n-1} here is Bourbaki's fork root α_n.

The classical model is ℤ ^ n with the dot product: the 2 * n * (n - 1) roots are the vectors ±e_a ± e_b with a ≠ b, which are exactly the integral vectors of squared length two, and the Bourbaki simple roots are αᵢ = eᵢ - eᵢ₊₁ for i + 1 < n together with the fork root α_{n-1} = e_{n-2} + e_{n-1}. That model, its enumeration by Fin (2 * n * (n - 1)) with the simple roots first, the expansion of every root in the simple roots, their linear independence and reflection in a root are all supplied by TauCeti.LinearAlgebra.RootSystem.ClassicalTypeD and are consumed here rather than rebuilt.

Type Dₙ is simply laced, so α^∨ = α under the dot product and both pinned lattices are images of the one classical model:

typeDWeight x = (x ⬝ᵥ αⱼ)ⱼ,      typeDSimpleRootCoordinates x = the coefficients of x in the αᵢ.

The first records a vector by its pairings against the simple coroots, the second by its coordinates in the simple coroots. Because the second family reconstructs the classical vector, the pinned pairing is the classical dot product, typeDWeight_dotProduct_coordinates, and every axiom of the datum reduces to a statement about ⬝ᵥ on ℤ ^ n.

The roots are indexed by Fin (2 * n * (n - 1)) through TauCeti.DynkinType.typeDRootEquiv, whose first n values are the simple roots in Bourbaki order. That index type is the one Layer 6 pins for the type, since (DynkinType.D n).numRoots is 2 * n * (n - 1) by definition.

Only the coroots are asked to span their lattice, and only that half is recorded, in corootSpan_typeDSimplyConnectedRootDatum_eq_top. The roots span the root lattice, which sits inside the weight lattice with index four (Bourbaki, Plate IV), so the datum is a RootDatum carrying no RootPairing.IsRootSystem instance. That asymmetry is what "simply connected" means here.

Main definitions #

Main results #

References #

The coordinates and the node 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. The layout of the file follows its sibling TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.A (#2594), whose type-agnostic scaffolding — the perfect pairing, the pinned support, the Cartan-type criterion and the coroot span — now lives in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.Basic and is shared with this file. This is the Dₙ branch of the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.

The two pinned coordinate families #

Reflections #

The pinned root datum #

source
noncomputable def TauCeti.DynkinType.typeDSimplyConnectedRootDatum (n : ℕ) (hn : 4 ≤ n) :
RootDatum (Fin (2 * n * (n - 1))) (Fin n → ℤ) (Fin n → ℤ)

The pinned simply connected root datum of type Dₙ, for n ≥ 4.

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 * (n - 1) roots are the classical ±e_a ± e_b with a ≠ b, enumerated with the simple roots first; see TauCeti.DynkinType.root_typeDSimpleIndex.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.DynkinType.toLinearMap_typeDSimplyConnectedRootDatum {n : ℕ} (hn : 4 ≤ n) (x y : Fin n → ℤ) :
    ((typeDSimplyConnectedRootDatum n hn).toLinearMap x) y = x ⬝ᵥ y

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

    source
    @[simp]
    theorem TauCeti.DynkinType.toLinearMap_typeDSimplyConnectedRootDatum_single_single {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) :
    ((typeDSimplyConnectedRootDatum n hn).toLinearMap (Pi.single i 1)) (Pi.single j 1) = if i = j then 1 else 0

    The standard basis of the character lattice is the family of fundamental weights. By TauCeti.DynkinType.coroot_typeDSimpleIndex the j-th simple coroot is Pi.single j 1, so this says ⟨ωᵢ, αⱼ^∨⟩ = δᵢⱼ.

    source
    theorem TauCeti.DynkinType.root_typeDSimplyConnectedRootDatum {n : ℕ} (hn : 4 ≤ n) (k : Fin (2 * n * (n - 1))) (j : Fin n) :
    (typeDSimplyConnectedRootDatum n hn).root k j = ↑((typeDRootEquiv n hn) k) ⬝ᵥ typeDSimpleRoot n hn j

    The k-th root of the pinned datum, in the fundamental-weight basis: its j-th coordinate is the pairing of the k-th classical root with the j-th simple root.

    source
    theorem TauCeti.DynkinType.coroot_typeDSimplyConnectedRootDatum {n : ℕ} (hn : 4 ≤ n) (k : Fin (2 * n * (n - 1))) :
    (typeDSimplyConnectedRootDatum n hn).coroot k = typeDSimpleRootCoordinates n hn ↑((typeDRootEquiv n hn) k)

    The k-th coroot of the pinned datum, in the simple-coroot basis: type Dₙ is simply laced, so it is the family of coefficients of the k-th classical root in the simple roots.

    source
    theorem TauCeti.DynkinType.pairing_typeDSimplyConnectedRootDatum_comm {n : ℕ} (hn : 4 ≤ n) (k l : Fin (2 * n * (n - 1))) :
    RootPairing.pairing (typeDSimplyConnectedRootDatum n hn) k l = RootPairing.pairing (typeDSimplyConnectedRootDatum n hn) l k

    The root--coroot pairing of the pinned type D datum is symmetric.

    source
    @[simp]
    theorem TauCeti.DynkinType.root_typeDSimpleIndex {n : ℕ} (hn : 4 ≤ n) (i : Fin n) :
    (typeDSimplyConnectedRootDatum n hn).root (typeDSimpleIndex n hn i) = fun (k : Fin n) => CartanMatrix.D 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 Dₙ datum is the i-th row of CartanMatrix.D n, which is what pins the character lattice as the weight lattice.

    source
    @[simp]
    theorem TauCeti.DynkinType.coroot_typeDSimpleIndex {n : ℕ} (hn : 4 ≤ n) (i : Fin n) :
    (typeDSimplyConnectedRootDatum n hn).coroot (typeDSimpleIndex n hn 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.

    source
    @[simp]
    theorem TauCeti.DynkinType.pairing_typeDSimpleIndex {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) :
    RootPairing.pairing (typeDSimplyConnectedRootDatum n hn) (typeDSimpleIndex n hn i) (typeDSimpleIndex n hn j) = CartanMatrix.D n i j

    The pairing of two simple roots of the pinned datum is the corresponding entry of the Bourbaki-numbered Cartan matrix.

    The pinned base #

    source
    noncomputable def TauCeti.DynkinType.typeDSimplyConnectedBase (n : ℕ) (hn : 4 ≤ n) :
    RootPairing.Base (typeDSimplyConnectedRootDatum n hn)

    The Bourbaki-numbered base of the pinned simply connected root datum of type Dₙ. 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.
    Instances For
      source
      @[simp]
      theorem TauCeti.DynkinType.mem_typeDSimplyConnectedBase_support {n : ℕ} (hn : 4 ≤ n) {k : Fin (2 * n * (n - 1))} :
      k ∈ (typeDSimplyConnectedBase n hn).support ↔ ↑k < n

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

      Positive roots in the pinned coordinates #

      source
      theorem TauCeti.DynkinType.mem_posRoots_typeDSimplyConnectedBase_iff_nonneg {n : ℕ} (hn : 4 ≤ n) (k : Fin (2 * n * (n - 1))) :
      k ∈ posRoots (typeDSimplyConnectedRootDatum n hn) (typeDSimplyConnectedBase n hn) ↔ ∀ (i : Fin n), 0 ≤ typeDSimpleRootCoordinates n hn (↑((typeDRootEquiv n hn) k)) i

      Positive roots of the pinned type Dₙ datum are exactly those whose classical simple-root coordinates are nonnegative. This sign criterion is the orientation input for the compatible Borel and its positive nilradical; it does not itself construct that nilradical.

      source
      theorem TauCeti.DynkinType.hasCartanType_typeDSimplyConnectedRootDatum (n : ℕ) (hn : 4 ≤ n) :
      HasCartanType (typeDSimplyConnectedRootDatum n hn) (typeDSimplyConnectedBase n hn) (D n)

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

      source
      theorem TauCeti.DynkinType.corootSpan_typeDSimplyConnectedRootDatum_eq_top (n : ℕ) (hn : 4 ≤ n) :
      RootPairing.corootSpan (typeDSimplyConnectedRootDatum n hn) ℤ = ⊤

      The coroots of the pinned type Dₙ 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 four (Bourbaki, Plate IV).