Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Suzuki.Torus

The torus of the Suzuki group #

The standard generators of TauCeti.suzukiGroup m are the lower unitriangular matrices u(a, b) and the antidiagonal Weyl element w. This file adds the diagonal torus

h(κ) = diag (κ, κ^θ / κ, κ / κ^θ, κ⁻¹),      θ = 2^(m+1),

as a homomorphism TauCeti.Suzuki.torus from the multiplicative group of the generator field, computes its conjugation action on the unipotent generators, and proves that its image lies in the generated group. The torus is not a generator, so its membership is a computation: the rank-one Bruhat relation

w u(0, b) w = u(b^(1-θ), b⁻¹) · h(b^θ) · w · u(b^(1-θ), 0)      (b ≠ 0)

exhibits h(b^θ) w as a product of generators, and since x ↦ x^θ is a bijection of the finite generator field every torus element is some h(b^θ). The Bruhat decomposition of the Suzuki group with respect to the point at infinity, and the identification of the group with the Steinberg fixed points, consume the torus in TauCeti.GroupTheory.SpecificGroups.CFSG.Suzuki.Generation.

Main definitions #

Main results #

References #

The torus #

source
noncomputable def TauCeti.Suzuki.torusMatrix (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) :
Matrix (Fin 4) (Fin 4) (GaloisField 2 (2 * m + 1))

The torus matrix of the Suzuki group at the parameter κ, diag (κ, κ^θ / κ, κ / κ^θ, κ⁻¹) with θ = 2^(m+1). Writing κ = λ^(2^m + 1), which is possible since 2^m + 1 is prime to 2^(2m+1) - 1, this is the usual diagonal matrix diag (λ^(2^m+1), λ^(2^m), λ^(-2^m), λ^(-2^m-1)) of the literature.

Instances For
    source
    @[simp]
    theorem TauCeti.Suzuki.torusMatrix_apply (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) (i j : Fin 4) :
    torusMatrix m κ i j = Matrix.diagonal ![↑κ, ↑κ ^ 2 ^ (m + 1) * (↑κ)⁻¹, ↑κ * (↑κ ^ 2 ^ (m + 1))⁻¹, (↑κ)⁻¹] i j

    An entry of the torus matrix.

    source
    @[simp]
    theorem TauCeti.Suzuki.det_torusMatrix (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) :
    (torusMatrix m κ).det = 1

    The torus matrix has determinant one.

    source
    @[simp]
    theorem TauCeti.Suzuki.torusMatrix_one (m : ℕ) :
    torusMatrix m 1 = 1

    The torus matrix at 1 is the identity.

    source
    theorem TauCeti.Suzuki.torusMatrix_mul (m : ℕ) (κ μ : (GaloisField 2 (2 * m + 1))ˣ) :
    torusMatrix m (κ * μ) = torusMatrix m κ * torusMatrix m μ

    The torus matrices multiply through their parameters.

    source
    noncomputable def TauCeti.Suzuki.torus (m : ℕ) :
    (GaloisField 2 (2 * m + 1))ˣ →* GL (Fin 4) (GaloisField 2 (2 * m + 1))

    The torus of the Suzuki group: the homomorphism κ ↦ h(κ) from the multiplicative group of the generator field into the general linear group, with h(κ) the matrix torusMatrix m κ.

    Instances For
      source
      @[simp]
      theorem TauCeti.Suzuki.coe_torus (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) :
      ↑((torus m) κ) = torusMatrix m κ

      The underlying matrix of torus m κ is torusMatrix m κ.

      The action of the torus on the unipotent generators #

      source
      @[simp]
      theorem TauCeti.Suzuki.torus_mul_unipotent_mul_torus_inv (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) (a b : GaloisField 2 (2 * m + 1)) :
      (torus m) κ * unipotent m a b * ((torus m) κ)⁻¹ = unipotent m (↑κ ^ 2 ^ (m + 1) / ↑κ ^ 2 * a) (b / ↑κ ^ 2 ^ (m + 1))

      The torus normalizes the unipotent generators: h(κ) u(a, b) h(κ)⁻¹ = u(κ^θ κ⁻² a, κ^(-θ) b), with θ = 2^(m+1).

      source
      @[simp]
      theorem TauCeti.Suzuki.commutatorElement_torus_unipotent (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) (a b : GaloisField 2 (2 * m + 1)) :
      ⁅(torus m) κ, unipotent m a b⁆ = unipotent m ((↑κ ^ 2 ^ (m + 1) / ↑κ ^ 2 + 1) * a) (((↑κ ^ 2 ^ (m + 1))⁻¹ + 1) * b + (↑κ ^ 2 ^ (m + 1) / ↑κ ^ 2 + 1) * a * a ^ 2 ^ (m + 1))

      The commutator of a torus element with a unipotent generator is again a unipotent generator: writing λ = κ^θ κ⁻² and μ = κ^(-θ), [h(κ), u(a, b)] = u((λ + 1) a, (μ + 1) b + (λ + 1) a^(1+θ)).

      The rank-one Bruhat relation and the torus #

      source
      theorem TauCeti.Suzuki.weyl_mul_unipotent_zero_mul_weyl (m : ℕ) (b : GaloisField 2 (2 * m + 1)) (hb : b ≠ 0) :
      weyl m * unipotent m 0 b * weyl m = unipotent m (b / b ^ 2 ^ (m + 1)) b⁻¹ * (torus m) (Units.mk0 (b ^ 2 ^ (m + 1)) ⋯) * weyl m * unipotent m (b / b ^ 2 ^ (m + 1)) 0

      The rank-one Bruhat relation of the Suzuki group: conjugating the long-root generator u(0, b) by the Weyl element lands in the big cell, w u(0, b) w = u' h(b^θ) w u'' with u' = u(b^(1-θ), b⁻¹) and u'' = u(b^(1-θ), 0).

      source
      theorem TauCeti.Suzuki.torus_mem_suzukiGroup (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) :
      (torus m) κ ∈ suzukiGroup m

      Every torus element of the Suzuki group is a product of the standard generators: it is read off the rank-one Bruhat relation at a θ-th root of its parameter.

      The Borel subgroup #

      source
      theorem TauCeti.Suzuki.torus_mul_mul_inv_mem_unipotentSubgroup (m : ℕ) (κ : (GaloisField 2 (2 * m + 1))ˣ) {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ unipotentSubgroup m) :
      (torus m) κ * g * ((torus m) κ)⁻¹ ∈ unipotentSubgroup m

      The torus normalizes the unipotent subgroup.

      source
      theorem TauCeti.Suzuki.range_torus_le_normalizer (m : ℕ) :
      (torus m).range ≤ Subgroup.normalizer ↑(unipotentSubgroup m)

      The range of the torus normalizes the unipotent subgroup.

      source
      noncomputable def TauCeti.Suzuki.borelSubgroup (m : ℕ) :
      Subgroup (GL (Fin 4) (GaloisField 2 (2 * m + 1)))

      The Borel subgroup B = H U of GL₄(𝔽_(2^(2m+1))), the join of the range of the torus and the unipotent subgroup. Since the torus normalizes the unipotent subgroup, it consists of the products h(κ) u(a, b) (TauCeti.Suzuki.mem_borelSubgroup).

      Instances For
        source
        @[simp]
        theorem TauCeti.Suzuki.mem_borelSubgroup {m : ℕ} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} :
        g ∈ borelSubgroup m ↔ ∃ (κ : (GaloisField 2 (2 * m + 1))ˣ) (a : GaloisField 2 (2 * m + 1)) (b : GaloisField 2 (2 * m + 1)), (torus m) κ * unipotent m a b = g

        The Borel subgroup consists of the products of a torus element and a standard unipotent generator.

        source
        theorem TauCeti.Suzuki.unipotentSubgroup_le_borelSubgroup (m : ℕ) :
        unipotentSubgroup m ≤ borelSubgroup m

        The unipotent subgroup lies in the Borel subgroup.

        source
        theorem TauCeti.Suzuki.borelSubgroup_le_suzukiGroup (m : ℕ) :
        borelSubgroup m ≤ suzukiGroup m

        The Borel subgroup lies in the Suzuki group.

        source
        theorem TauCeti.Suzuki.borelSubgroup_le_normalizer (m : ℕ) :
        borelSubgroup m ≤ Subgroup.normalizer ↑(unipotentSubgroup m)

        The Borel subgroup normalizes the unipotent subgroup.

        source
        theorem TauCeti.Suzuki.weyl_mul_unipotent_mul_weyl_mem_borelSubgroup_iff (m : ℕ) {a b : GaloisField 2 (2 * m + 1)} :
        weyl m * unipotent m a b * weyl m ∈ borelSubgroup m ↔ a = 0 ∧ b = 0

        The Weyl element conjugates u(a, b) into the Borel subgroup only when u(a, b) = 1.

        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.Suzuki.borelSubgroupOf (m : ℕ) :
        Subgroup ↥(suzukiGroup m)

        The Borel subgroup B = H U, inside the Suzuki group.

        Instances For
          source
          theorem TauCeti.Suzuki.borelSubgroupOf_le_normalizer (m : ℕ) :
          borelSubgroupOf m ≤ Subgroup.normalizer ↑(unipotentSubgroupOf m)

          The Borel subgroup normalizes the unipotent subgroup, inside the Suzuki group.

          source
          theorem TauCeti.Suzuki.normalClosure_unipotentSubgroupOf (m : ℕ) :
          Subgroup.normalClosure ↑(unipotentSubgroupOf m) = ⊤

          The conjugates of the unipotent subgroup generate the Suzuki group. The Weyl element is u(1, 1)⁻¹ (w u(0, 1) w⁻¹) u(1, 0)⁻¹, by the rank-one Bruhat relation at the parameter 1.