Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.B.SpecialMap

The special length-exchanging map of the pinned type B₂ root datum #

In characteristic two, the Suzuki construction uses a special isogeny of the simply connected group of type B₂. At the root-datum level its character-lattice map exchanges the two Bourbaki nodes and multiplies in the long-root direction. In the fundamental-weight coordinates of TauCeti.DynkinType.b2Root, that map is

A = !![0, 1; 2, 0].

This file computes the action of A on every root and of Aᵀ on every coroot. The induced root permutation exchanges the two simple roots, the two other positive roots, and their negatives. The rescaling exponent is the existing squared-length table TauCeti.DynkinType.b2Length: it is 1 on short roots and 2 on long roots. Applying the data twice multiplies both lattices by 2, and the two exponents along each orbit multiply to 2.

These equations are the explicit B₂ input for the root-datum special-isogeny construction. They do not yet construct a group-scheme morphism; Layer 9 of the reductive-groups roadmap requires that later lift, together with its action on root subgroups, before the Suzuki--Ree lane can use it.

Main definitions #

Main results #

References #

The node numbering and coordinates follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II. The special-isogeny equations follow R. Steinberg, Endomorphisms of Linear Algebraic Groups, §11; the Suzuki convention is also described in R. W. Carter, Simple Groups of Lie Type, §§12.3--12.4. The exponent is 1 on long root subgroups and the characteristic on short root subgroups when the group-scheme map is read contravariantly on its root datum. Here the lattice map consequently rescales a root by its own squared length before exchanging its index.

The lattice map and the root permutation #

source
def TauCeti.DynkinType.b2SpecialIsogenyMatrix :
Matrix (Fin 2) (Fin 2) ℤ

The character-lattice matrix of the special length-exchanging map of the pinned B₂ root datum, in the fundamental-weight basis.

Equations
Instances For
    source
    theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_def :
    b2SpecialIsogenyMatrix = !![0, 1; 2, 0]

    The explicit entries of the character-lattice special-isogeny matrix.

    source
    def TauCeti.DynkinType.b2SpecialIsogenyTableIndex :
    Fin 8 → Fin 8

    The permutation of the eight B₂ roots induced by TauCeti.DynkinType.b2SpecialIsogenyMatrix. It exchanges long roots with short roots and commutes with root negation.

    Equations
    Instances For
      source
      theorem TauCeti.DynkinType.b2SpecialIsogenyTableIndex_def :
      b2SpecialIsogenyTableIndex = ![1, 0, 3, 2, 5, 4, 7, 6]

      The explicit values of the special permutation on the coordinate-table indices.

      source
      @[simp]
      theorem TauCeti.DynkinType.b2SpecialIsogenyTableIndex_add_four (i : Fin 8) :
      b2SpecialIsogenyTableIndex (i + 4) = b2SpecialIsogenyTableIndex i + 4

      The special root permutation commutes with passing to the negative root.

      source
      noncomputable def TauCeti.DynkinType.b2SpecialIsogenyIndexEquiv :
      Equiv.Perm (Fin (2 * 2 ^ 2))

      The special permutation on the native root indices of the pinned type B₂ datum. It is the coordinate-table permutation conjugated by TauCeti.DynkinType.b2IndexEquiv.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.DynkinType.b2SpecialIsogenyIndexEquiv_b2Index (i : Fin 8) :
        b2SpecialIsogenyIndexEquiv (b2Index i) = b2Index (b2SpecialIsogenyTableIndex i)

        On a tabulated root, the native special permutation is the tabulated permutation.

        source
        @[simp]
        theorem TauCeti.DynkinType.b2SpecialIsogenyIndexEquiv_apply_apply (i : Fin (2 * 2 ^ 2)) :
        b2SpecialIsogenyIndexEquiv (b2SpecialIsogenyIndexEquiv i) = i

        Applying the special permutation twice fixes every native root index.

        source
        @[simp]
        theorem TauCeti.DynkinType.b2SpecialIsogenyIndexEquiv_typeBSimpleIndex (i : Fin 2) :
        b2SpecialIsogenyIndexEquiv (typeBSimpleIndex 2 i) = typeBSimpleIndex 2 (lengthPermRankTwo i)

        On the pinned simple-root indices, the special permutation is the rank-two length permutation.

        source
        noncomputable def TauCeti.DynkinType.b2SpecialIsogenyExponent (i : Fin (2 * 2 ^ 2)) :
        ℤ

        The exponent of the special map on the native root indices of the pinned type B₂ datum.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_b2Index (i : Fin 8) :
          b2SpecialIsogenyExponent (b2Index i) = b2Length i

          On a tabulated root, the special exponent is its squared length.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_pos (i : Fin (2 * 2 ^ 2)) :
          0 < b2SpecialIsogenyExponent i

          Every exponent of the special map is positive.

          Action on the pinned root datum #

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_mulVec_root (i : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyMatrix.mulVec ((typeBSimplyConnectedRootDatum 2).root i) = b2SpecialIsogenyExponent i • (typeBSimplyConnectedRootDatum 2).root (b2SpecialIsogenyIndexEquiv i)

          The special matrix carries every root of the pinned datum to its indexed image with the prescribed exponent.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_transpose_mulVec_coroot (i : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyMatrix.transpose.mulVec ((typeBSimplyConnectedRootDatum 2).coroot (b2SpecialIsogenyIndexEquiv i)) = b2SpecialIsogenyExponent i • (typeBSimplyConnectedRootDatum 2).coroot i

          The transposed special matrix satisfies the contragredient equation on every coroot of the pinned datum.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_mul_self :
          b2SpecialIsogenyMatrix * b2SpecialIsogenyMatrix = 2 • 1

          The square of the character-lattice special matrix is twice the identity matrix.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_transpose_mul_self :
          b2SpecialIsogenyMatrix.transpose * b2SpecialIsogenyMatrix.transpose = 2 • 1

          The square of the cocharacter-lattice special matrix is twice the identity matrix.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_mulVec_self (x : Fin 2 → ℤ) :
          b2SpecialIsogenyMatrix.mulVec (b2SpecialIsogenyMatrix.mulVec x) = 2 • x

          Applying the character-lattice special map twice is multiplication by the characteristic 2. This is not a simp lemma: on Fin 2 the simp set unfolds *ᵥ entrywise through Matrix.mulVec_fin_two, so the left-hand side is not in normal form.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_transpose_mulVec_self (x : Fin 2 → ℤ) :
          b2SpecialIsogenyMatrix.transpose.mulVec (b2SpecialIsogenyMatrix.transpose.mulVec x) = 2 • x

          Applying the cocharacter-lattice special map twice is multiplication by the characteristic 2. As for the character-lattice statement, this is not a simp lemma.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_mulVecLin_comp_self :
          b2SpecialIsogenyMatrix.mulVecLin ∘ₗ b2SpecialIsogenyMatrix.mulVecLin = 2 • LinearMap.id

          The square relation for the character-lattice map, as an equality of linear maps.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyMatrix_transpose_mulVecLin_comp_self :
          b2SpecialIsogenyMatrix.transpose.mulVecLin ∘ₗ b2SpecialIsogenyMatrix.transpose.mulVecLin = 2 • LinearMap.id

          The square relation for the cocharacter-lattice map, as an equality of linear maps.

          source
          @[simp]
          theorem TauCeti.DynkinType.det_b2SpecialIsogenyMatrix :
          b2SpecialIsogenyMatrix.det = -2

          The special map is an isogeny and not an automorphism of the character lattice: its determinant is -2, of absolute value the characteristic.

          Length and exponent conventions #

          source
          @[simp]
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_mul_exponent (i : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyExponent i * b2SpecialIsogenyExponent (b2SpecialIsogenyIndexEquiv i) = 2

          The exponents at a native root index and its image multiply to the characteristic 2.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_eq_one_or_eq_two (i : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyExponent i = 1 ∨ b2SpecialIsogenyExponent i = 2

          Every rescaling exponent of the special map is either 1 or the characteristic 2.

          source
          @[simp]
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_indexEquiv_eq_one_iff (i : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyExponent (b2SpecialIsogenyIndexEquiv i) = 1 ↔ b2SpecialIsogenyExponent i = 2

          The special permutation exchanges long roots with short ones.

          source
          @[simp]
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_indexEquiv_eq_two_iff (i : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyExponent (b2SpecialIsogenyIndexEquiv i) = 2 ↔ b2SpecialIsogenyExponent i = 1

          The special permutation sends a short root to a long root.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_mul_pairing (i j : Fin (2 * 2 ^ 2)) :
          b2SpecialIsogenyExponent i * RootPairing.pairing (typeBSimplyConnectedRootDatum 2) (b2SpecialIsogenyIndexEquiv i) (b2SpecialIsogenyIndexEquiv j) = b2SpecialIsogenyExponent j * RootPairing.pairing (typeBSimplyConnectedRootDatum 2) i j

          The Cartan integers transform by the rule a special isogeny forces. Writing α' for the image of a root α under the special permutation, pairing the root equation against the coroot equation gives ℓ(α) ⟨α', β'∨⟩ = ℓ(β) ⟨α, β∨⟩.

          source
          @[simp]
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_typeBSimpleIndex (i : Fin 2) :
          b2SpecialIsogenyExponent (typeBSimpleIndex 2 i) = (B 2).rootLength i

          On a pinned simple-root index, the special exponent is its normalised squared length.

          source
          theorem TauCeti.DynkinType.b2SpecialIsogenyExponent_typeBSimpleIndex_eq_one_iff (i : Fin 2) :
          b2SpecialIsogenyExponent (typeBSimpleIndex 2 i) = 1 ↔ ¬(B 2).IsLongSimpleRoot i

          At a pinned simple-root index, the special exponent is 1 exactly on a short node.