Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.Assembly

The pinned simply connected root datum of a Dynkin type #

This file assembles the explicit simply connected root data for the nine irreducible crystallographic Dynkin families into one construction indexed by a valid TauCeti.DynkinType. Both lattices are Fin t.rank → ℤ: the character lattice uses the fundamental-weight basis and the cocharacter lattice uses the simple-coroot basis. Roots are indexed by Fin t.numRoots, with the first t.rank indices the Bourbaki-numbered simple roots.

The construction dispatches directly to the coordinate data in the family modules imported above. It does not choose a root datum from a realization theorem. The branch equations below make this explicit data available without requiring downstream users to unfold the dispatcher.

Main definitions #

Main results #

References #

The family data and numbering follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates I--IX, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter 11. This assembles the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md for its consumer, CFSGStatement milestone L0.

The uniform pinned datum #

source
noncomputable def TauCeti.DynkinType.simplyConnectedRootDatum (t : DynkinType) (ht : t.Valid) :
RootDatum (Fin t.numRoots) (Fin t.rank → ℤ) (Fin t.rank → ℤ)

The pinned simply connected root datum attached to a valid Dynkin type.

This is a definition by cases into the nine explicit family data. The validity proof is used only by the type D construction, whose coordinate model requires 4 ≤ n; the other family models are defined at every rank, while validity controls which of them enter the classification list.

Equations
Instances For
    source
    noncomputable def TauCeti.DynkinType.simplyConnectedBase (t : DynkinType) (ht : t.Valid) :
    RootPairing.Base (t.simplyConnectedRootDatum ht)

    The Bourbaki-numbered base of simplyConnectedRootDatum, supported on its first t.rank root indices.

    Equations
    Instances For

      Branch equations #

      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_A (n : ℕ) (ht : (A n).Valid) :
      (A n).simplyConnectedRootDatum ht = typeASimplyConnectedRootDatum n
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_B (n : ℕ) (ht : (B n).Valid) :
      (B n).simplyConnectedRootDatum ht = typeBSimplyConnectedRootDatum n
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_C (n : ℕ) (ht : (C n).Valid) :
      (C n).simplyConnectedRootDatum ht = typeCSimplyConnectedRootDatum n
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_D (n : ℕ) (ht : (D n).Valid) :
      (D n).simplyConnectedRootDatum ht = typeDSimplyConnectedRootDatum n ⋯
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_E6 (ht : E6.Valid) :
      E6.simplyConnectedRootDatum ht = e6SimplyConnectedRootDatum
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_E7 (ht : E7.Valid) :
      E7.simplyConnectedRootDatum ht = e7SimplyConnectedRootDatum
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_E8 (ht : E8.Valid) :
      E8.simplyConnectedRootDatum ht = e8SimplyConnectedRootDatum
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_F4 (ht : F4.Valid) :
      F4.simplyConnectedRootDatum ht = f4SimplyConnectedRootDatum
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedRootDatum_G2 (ht : G2.Valid) :
      G2.simplyConnectedRootDatum ht = g2SimplyConnectedRootDatum
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_A (n : ℕ) (ht : (A n).Valid) :
      ⋯.mp ((A n).simplyConnectedBase ht) = typeASimplyConnectedBase n
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_B (n : ℕ) (ht : (B n).Valid) :
      ⋯.mp ((B n).simplyConnectedBase ht) = typeBSimplyConnectedBase n
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_C (n : ℕ) (ht : (C n).Valid) :
      ⋯.mp ((C n).simplyConnectedBase ht) = typeCSimplyConnectedBase n
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_D (n : ℕ) (ht : (D n).Valid) :
      ⋯.mp ((D n).simplyConnectedBase ht) = typeDSimplyConnectedBase n ⋯
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_E6 (ht : E6.Valid) :
      ⋯.mp (E6.simplyConnectedBase ht) = e6SimplyConnectedBase
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_E7 (ht : E7.Valid) :
      ⋯.mp (E7.simplyConnectedBase ht) = e7SimplyConnectedBase
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_E8 (ht : E8.Valid) :
      ⋯.mp (E8.simplyConnectedBase ht) = e8SimplyConnectedBase
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_F4 (ht : F4.Valid) :
      ⋯.mp (F4.simplyConnectedBase ht) = f4SimplyConnectedBase
      source
      @[simp]
      theorem TauCeti.DynkinType.simplyConnectedBase_G2 (ht : G2.Valid) :
      ⋯.mp (G2.simplyConnectedBase ht) = g2SimplyConnectedBase

      The uniform Bourbaki pinning #

      source
      def TauCeti.DynkinType.simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      Fin t.numRoots

      The index of the i-th Bourbaki simple root in the pinned root enumeration.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.DynkinType.simpleIndex_val (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
        ↑(t.simpleIndex ht i) = ↑i

        The root enumeration index of a simple root has the same zero-based value as its node.

        Each family module enumerates its own roots and names its own simple-root index. The equations below identify the dispatcher with those names, so a statement proved for one family about its own index transfers to the uniform one. They are stated by Fin.ext against simpleIndex_val rather than by unfolding either side.

        source
        @[simp]
        theorem TauCeti.DynkinType.simpleIndex_B (n : ℕ) (ht : (B n).Valid) (i : Fin n) :
        (B n).simpleIndex ht i = typeBSimpleIndex n i

        The simple-root index of the dispatcher at type B n is type B's own simple-root index.

        source
        @[simp]
        theorem TauCeti.DynkinType.simpleIndex_F4 (ht : F4.Valid) (i : Fin 4) :
        F4.simpleIndex ht i = Fin.castAdd 44 i

        The simple-root index of the dispatcher at type F₄ is type F₄'s own simple-root index.

        source
        @[simp]
        theorem TauCeti.DynkinType.simpleIndex_G2 (ht : G2.Valid) (i : Fin 2) :
        G2.simpleIndex ht i = Fin.castAdd 10 i

        The simple-root index of the dispatcher at type G₂ is type G₂'s own simple-root index.

        source
        @[simp]
        theorem TauCeti.DynkinType.coroot_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
        (t.simplyConnectedRootDatum ht).coroot (t.simpleIndex ht i) = Pi.single i 1

        The simple coroots of the pinned datum are the standard basis of the cocharacter lattice.

        source
        @[simp]
        theorem TauCeti.DynkinType.root_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
        (t.simplyConnectedRootDatum ht).root (t.simpleIndex ht i) = fun (k : Fin t.rank) => t.cartanMatrix i k

        The simple roots of the pinned datum are the rows of its Bourbaki-numbered Cartan matrix.

        source
        @[simp]
        theorem TauCeti.DynkinType.mem_support_simplyConnectedBase (t : DynkinType) (ht : t.Valid) {k : Fin t.numRoots} :
        k ∈ (t.simplyConnectedBase ht).support ↔ ↑k < t.rank

        The pinned base is supported exactly on the first t.rank root indices.

        source
        def TauCeti.DynkinType.simpleSupportEquivSimplyConnectedBase (t : DynkinType) (ht : t.Valid) :
        Fin t.rank ≃ ↥(t.simplyConnectedBase ht).support

        The Bourbaki numbering identifies the nodes with the support of the pinned integral base.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.DynkinType.coe_simpleSupportEquivSimplyConnectedBase (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
          ↑((t.simpleSupportEquivSimplyConnectedBase ht) i) = t.simpleIndex ht i
          source
          theorem TauCeti.DynkinType.card_support_simplyConnectedBase (t : DynkinType) (ht : t.Valid) :
          (t.simplyConnectedBase ht).support.card = t.rank

          The pinned base has one simple root per Bourbaki node.

          source
          theorem TauCeti.DynkinType.toLinearMap_simplyConnectedRootDatum (t : DynkinType) (ht : t.Valid) (x y : Fin t.rank → ℤ) :
          ((t.simplyConnectedRootDatum ht).toLinearMap x) y = x ⬝ᵥ y

          The pinned pairing is the dot product of the fundamental-weight and simple-coroot coordinates, uniformly in the Dynkin type.

          source
          theorem TauCeti.DynkinType.coroot'_simpleIndex_apply (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (mu : Fin t.rank → ℤ) :
          (RootPairing.coroot' (t.simplyConnectedRootDatum ht) (t.simpleIndex ht i)) mu = mu i

          Evaluation at the i-th simple coroot extracts the i-th fundamental-weight coordinate.

          Not a simp lemma: RootPairing.coroot' is an abbreviation for a LinearMap.flip, so simp rewrites the left-hand side with LinearMap.flip_apply before this could fire.

          source
          @[simp]
          theorem TauCeti.DynkinType.pairing_simpleIndex (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) :
          RootPairing.pairing (t.simplyConnectedRootDatum ht) (t.simpleIndex ht i) (t.simpleIndex ht j) = t.cartanMatrix i j

          The Cartan integers of the pinned datum at the simple indices are the entries of its Bourbaki-numbered Cartan matrix. The simple root is a row of the Cartan matrix and the simple coroot is a standard basis vector, so the dot product picks out one entry.

          source
          @[simp]
          theorem TauCeti.DynkinType.pairingIn_simpleIndex (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) :
          RootPairing.pairingIn (t.simplyConnectedRootDatum ht) ℤ (t.simpleIndex ht i) (t.simpleIndex ht j) = t.cartanMatrix i j

          The integral form of TauCeti.DynkinType.pairing_simpleIndex.

          Uniform acceptance theorems #

          source
          theorem TauCeti.DynkinType.hasCartanType_simplyConnectedRootDatum (t : DynkinType) (ht : t.Valid) :
          HasCartanType (t.simplyConnectedRootDatum ht) (t.simplyConnectedBase ht) t

          The pinned datum has Cartan type t: its base Cartan matrix agrees with the standard one after a relabelling of the support. The entrywise Bourbaki pinning is given by root_simpleIndex and coroot_simpleIndex.

          source
          theorem TauCeti.DynkinType.span_coroot_simplyConnectedRootDatum (t : DynkinType) (ht : t.Valid) :
          Submodule.span ℤ (Set.range ⇑(t.simplyConnectedRootDatum ht).coroot) = ⊤

          The coroots of the pinned datum span the cocharacter lattice. This is the simply connected lattice condition consumed by the pinned Chevalley--Demazure construction.