Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.B.RankTwo

The rank-two type B root datum in explicit coordinates #

TauCeti.DynkinType.typeBSimplyConnectedRootDatum is built uniformly in the rank, out of signed basis vectors and a rotated product enumeration, so its public interface reads off the simple roots and the simple coroots and nothing else. A consumer that has to check an equation on every root of a fixed small rank cannot work with that: it needs a coordinate table, in the same shape as the ones TauCeti.DynkinType.g2Root and TauCeti.DynkinType.f4Root carry for the two exceptional types built directly from coordinates.

This file supplies the missing rank-two table. It names the eight roots of B₂ by reflection words in the two Bourbaki simple indices, and identifies their character and cocharacter coordinates.

Coordinates #

The character lattice is the weight lattice in the fundamental-weight basis and the cocharacter lattice is the coroot lattice in the simple-coroot basis, so the coordinates of a root are its Cartan integers against the two simple coroots and the coordinates of a coroot are its coefficients on the two simple coroots. With α₀ the long simple root and α₁ the short one, the Cartan matrix being !![2, -2; -1, 2] (TauCeti.DynkinType.cartanMatrix_B_two_eq), the enumeration is

α₀,  α₁,  α₀ + α₁,  α₀ + 2 α₁,  -α₀,  -α₁,  -α₀ - α₁,  -α₀ - 2 α₁,

so that index k + 4 is the negative of index k. The four positive roots come first, the two simple ones first among them, matching the convention of TauCeti.DynkinType.typeBSimpleIndex.

Main definitions #

Main results #

References #

The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II. The table is the rank-two input asked for by the "special isogenies in characteristics two and three" bullet of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, whose B₂ case is the one the pinned type B datum could not be computed against.

source
def TauCeti.DynkinType.b2Root :
Fin 8 → Fin 2 → ℤ

The eight roots of the pinned rank-two type B datum, in the fundamental-weight basis of the character lattice, with the four positive roots first and the two simple ones first among them.

Equations
Instances For
    source
    def TauCeti.DynkinType.b2Coroot :
    Fin 8 → Fin 2 → ℤ

    The eight coroots of the pinned rank-two type B datum, in the simple-coroot basis of the cocharacter lattice, ordered compatibly with TauCeti.DynkinType.b2Root.

    Equations
    Instances For
      source
      theorem TauCeti.DynkinType.b2Root_injective :
      Function.Injective b2Root

      The eight tabulated roots are pairwise distinct.

      source
      theorem TauCeti.DynkinType.b2Coroot_injective :
      Function.Injective b2Coroot

      The eight tabulated coroots are pairwise distinct.

      source
      theorem TauCeti.DynkinType.b2Root_dotProduct_b2Coroot_self (k : Fin 8) :
      b2Root k ⬝ᵥ b2Coroot k = 2

      A root and the coroot listed beside it pair to 2, as a root datum asks.

      source
      @[simp]
      theorem TauCeti.DynkinType.b2Root_add_four (k : Fin 8) :
      b2Root (k + 4) = -b2Root k

      The last four roots are the negatives of the first four.

      source
      @[simp]
      theorem TauCeti.DynkinType.b2Coroot_add_four (k : Fin 8) :
      b2Coroot (k + 4) = -b2Coroot k

      The last four coroots are the negatives of the first four.

      source
      def TauCeti.DynkinType.b2Index :
      Fin 8 → Fin (2 * 2 ^ 2)

      The eight root indices of the pinned rank-two type B datum, named by reflection words in the two Bourbaki simple indices and ordered as TauCeti.DynkinType.b2Root is.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.DynkinType.b2Index_zero :
        b2Index 0 = typeBSimpleIndex 2 0

        The first named index is the first Bourbaki simple root.

        source
        @[simp]
        theorem TauCeti.DynkinType.b2Index_one :
        b2Index 1 = typeBSimpleIndex 2 1

        The second named index is the second Bourbaki simple root.

        Computing the table #

        The table is the datum #

        source
        @[simp]
        theorem TauCeti.DynkinType.root_b2Index (k : Fin 8) :
        (typeBSimplyConnectedRootDatum 2).root (b2Index k) = b2Root k

        The eight named indices carry the tabulated roots.

        source
        @[simp]
        theorem TauCeti.DynkinType.coroot_b2Index (k : Fin 8) :
        (typeBSimplyConnectedRootDatum 2).coroot (b2Index k) = b2Coroot k

        The eight named indices carry the tabulated coroots.

        source
        theorem TauCeti.DynkinType.b2Index_injective :
        Function.Injective b2Index

        The eight reflection words name eight distinct root indices.

        source
        theorem TauCeti.DynkinType.b2Index_bijective :
        Function.Bijective b2Index

        The eight reflection words exhaust the root indices. The pinned rank-two type B datum has 2 * 2 ^ 2 = 8 roots, so the injective list TauCeti.DynkinType.b2Index is all of them.

        source
        noncomputable def TauCeti.DynkinType.b2IndexEquiv :
        Fin 8 ≃ Fin (2 * 2 ^ 2)

        The reindexing of the roots of the pinned rank-two type B datum by the coordinate table.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.DynkinType.b2IndexEquiv_apply (k : Fin 8) :
          b2IndexEquiv k = b2Index k

          The reindexing is the named list of indices.

          source
          theorem TauCeti.DynkinType.range_root_typeBSimplyConnectedRootDatum_two :
          Set.range ⇑(typeBSimplyConnectedRootDatum 2).root = Set.range b2Root

          The tabulated roots are all the roots.

          source
          theorem TauCeti.DynkinType.range_coroot_typeBSimplyConnectedRootDatum_two :
          Set.range ⇑(typeBSimplyConnectedRootDatum 2).coroot = Set.range b2Coroot

          The tabulated coroots are all the coroots.

          source
          @[simp]
          theorem TauCeti.DynkinType.pairing_b2Index (k l : Fin 8) :
          RootPairing.pairing (typeBSimplyConnectedRootDatum 2) (b2Index k) (b2Index l) = b2Root k ⬝ᵥ b2Coroot l

          Every Cartan integer of the pinned rank-two type B datum is a dot product of table entries, hence a decidable computation.

          Simple-root coordinates and lengths #

          source
          def TauCeti.DynkinType.b2Coeff :
          Fin 8 → Fin 2 → ℤ

          The simple-root coordinates of the eight roots of the pinned rank-two type B datum: the pair (c₀, c₁) with β = c₀ α₀ + c₁ α₁.

          Equations
          Instances For
            source
            theorem TauCeti.DynkinType.b2Root_eq_smul_add_smul (k : Fin 8) :
            b2Root k = b2Coeff k 0 • b2Root 0 + b2Coeff k 1 • b2Root 1

            The coefficient table expands each root on the two simple roots.

            source
            theorem TauCeti.DynkinType.eq_b2Coeff_of_root_eq {k : Fin 8} {c : Fin 2 → ℤ} (h : b2Root k = c 0 • b2Root 0 + c 1 • b2Root 1) :
            c = b2Coeff k

            The two simple roots are linearly independent, so the expansion above determines the coefficients.

            source
            theorem TauCeti.DynkinType.b2Coeff_nonneg (k : Fin 8) (hk : ↑k < 4) (i : Fin 2) :
            0 ≤ b2Coeff k i

            The four positive roots come first: their simple-root coordinates are nonnegative.

            source
            theorem TauCeti.DynkinType.b2Coeff_nonpos (k : Fin 8) (hk : 4 ≤ ↑k) (i : Fin 2) :
            b2Coeff k i ≤ 0

            The four negative roots come last: their simple-root coordinates are nonpositive.

            source
            def TauCeti.DynkinType.b2Length :
            Fin 8 → ℤ

            The squared lengths of the eight roots of the pinned rank-two type B datum, normalised as TauCeti.DynkinType.rootLength normalises the simple ones: 1 on the four short roots ± α₁, ± (α₀ + α₁) and 2 on the four long ones ± α₀, ± (α₀ + 2 α₁).

            Equations
            Instances For
              source
              theorem TauCeti.DynkinType.b2Length_mul_b2Coroot (k : Fin 8) (i : Fin 2) :
              b2Length k * b2Coroot k i = b2Coeff k i * (B 2).rootLength i

              The length table is the one forced by the simple lengths. Writing β = Σ cᵢ αᵢ and β∨ = Σ dᵢ αᵢ∨, the identity β∨ = 2 β / (β, β) reads ℓ(β) dᵢ = cᵢ ℓ(αᵢ) once both sides are expanded on the simple coroots.

              source
              theorem TauCeti.DynkinType.eq_b2Length_of_mul_b2Coroot {k : Fin 8} {c : ℤ} (h : ∀ (i : Fin 2), c * b2Coroot k i = b2Coeff k i * (B 2).rootLength i) :
              c = b2Length k

              No coroot vanishes, so TauCeti.DynkinType.b2Length_mul_b2Coroot determines the length table.

              source
              @[simp]
              theorem TauCeti.DynkinType.b2Length_castLE (i : Fin 2) :
              b2Length (Fin.castLE b2Length_castLE._proof_1 i) = (B 2).rootLength i

              On the two simple roots the length table is TauCeti.DynkinType.rootLength.

              source
              @[simp]
              theorem TauCeti.DynkinType.b2Length_add_four (k : Fin 8) :
              b2Length (k + 4) = b2Length k

              A root and its negative have the same length.

              source
              theorem TauCeti.DynkinType.isLongSimpleRoot_iff_b2Length_eq_two (i : Fin 2) :
              (B 2).IsLongSimpleRoot i ↔ b2Length (Fin.castLE b2Length_castLE._proof_1 i) = 2

              The long simple roots are the ones of length two, which is the convention TauCeti.DynkinType.rootLength fixes and the one a length-exchanging map is pinned against.