Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Suzuki.FieldDescent

Descent of Suzuki fixed points to the finite field #

The Steinberg fixed-point construction of the Suzuki groups lives in a general linear group over an algebraic closure, whereas the standard generators live over GaloisField 2 (2 * m + 1). This file proves that the embedding chosen for the generators has exactly the Frobenius-fixed field as its image. Consequently every Steinberg fixed point has finite-field coordinates for that same embedding.

The subgroup finiteFixedSubgroup is the exact finite-field preimage of the Steinberg fixed points. Scalar extension identifies it with the fixed-point subgroup in the ambient general linear group. Equality with Suzuki.suzukiGroup is the finite-field generation theorem that identifies the two constructions; it is not asserted here.

Main results #

References #

source
@[simp]
theorem TauCeti.SuzukiLieIndex.fieldRange_generatorFieldEmbedding (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
(generatorFieldEmbedding m hvalid).fieldRange = (↑(of m hvalid)).fixedField

The field embedding chosen for the standard Suzuki generators has image exactly the fixed field of the field Frobenius.

source
@[simp]
theorem TauCeti.SuzukiLieIndex.mem_range_generatorFieldEmbedding_iff (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) {x : (↑(of m hvalid)).Closure} :
(∃ (y : GaloisField 2 (2 * m + 1)), (generatorFieldEmbedding m hvalid) y = x) ↔ x ^ (↑(of m hvalid)).fieldOrder = x

An element of the algebraic closure lies in the range of the field embedding used for the Suzuki generators exactly when the field Frobenius fixes it.

source
@[simp]
theorem TauCeti.SuzukiLieIndex.mem_range_generatorEmbedding_iff (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : GL (Fin 4) (↑(of m hvalid)).Closure) :
(∃ (g₀ : GL (Fin 4) (GaloisField 2 (2 * m + 1))), (generatorEmbedding m hvalid) g₀ = g) ↔ ∀ (i j : Fin 4), ↑g i j ^ (↑(of m hvalid)).fieldOrder = ↑g i j

Scalar extension after the Suzuki coordinate change has exactly the invertible matrices whose entries are fixed by the field Frobenius.

source
theorem TauCeti.SuzukiLieIndex.map_fixedSubgroup_le_range_generatorEmbedding (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg) ≤ (generatorEmbedding m hvalid).range

Every Suzuki Steinberg fixed point in the ambient general linear group has coordinates over the finite field used by the standard generators.

source
noncomputable def TauCeti.SuzukiLieIndex.finiteFixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
Subgroup (GL (Fin 4) (GaloisField 2 (2 * m + 1)))

The exact finite-field preimage of the Suzuki Steinberg fixed-point subgroup. Equality with Suzuki.suzukiGroup is the associated finite-field generation theorem.

Instances For
    source
    @[simp]
    theorem TauCeti.SuzukiLieIndex.mem_finiteFixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} :
    g ∈ finiteFixedSubgroup m hvalid ↔ (generatorEmbedding m hvalid) g ∈ Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg)

    Membership in the finite-field preimage is detected by scalar extension to the Suzuki Steinberg fixed-point subgroup.

    source
    theorem TauCeti.SuzukiLieIndex.mem_finiteFixedSubgroup_iff (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} :
    g ∈ finiteFixedSubgroup m hvalid ↔ ↑((Suzuki.coordinateEquiv (GaloisField 2 (2 * m + 1))) g) * JFin 2 (GaloisField 2 (2 * m + 1)) * (↑((Suzuki.coordinateEquiv (GaloisField 2 (2 * m + 1))) g)).transpose = JFin 2 (GaloisField 2 (2 * m + 1)) ∧ (↑((Suzuki.coordinateEquiv (GaloisField 2 (2 * m + 1))) g)).symplecticSpecialIsogeny = (↑((Suzuki.coordinateEquiv (GaloisField 2 (2 * m + 1))) g)).map fun (x : GaloisField 2 (2 * m + 1)) => x ^ 2 ^ (m + 1)

    Over the generator field, a matrix is a Steinberg fixed point exactly when its coordinate change preserves the alternating form and has special isogeny equal to its entrywise 2^(m+1)-st power.

    source
    theorem TauCeti.SuzukiLieIndex.suzukiGroup_le_finiteFixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
    suzukiGroup m ≤ finiteFixedSubgroup m hvalid

    The standard generated Suzuki group lies in the exact finite-field preimage of the Steinberg fixed points. Equality is the finite-field generation theorem identifying the two constructions.

    source
    theorem TauCeti.SuzukiLieIndex.map_finiteFixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
    Subgroup.map (generatorEmbedding m hvalid) (finiteFixedSubgroup m hvalid) = Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg)

    Scalar extension maps the finite-field preimage onto the full Suzuki Steinberg fixed-point subgroup.

    source
    noncomputable def TauCeti.SuzukiLieIndex.finiteFixedSubgroupEquiv (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
    ↥(finiteFixedSubgroup m hvalid) ≃* ↥(Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg))

    Scalar extension is an isomorphism from the finite-field preimage onto the Suzuki Steinberg fixed-point subgroup in the algebraic-closure model.

    Instances For
      source
      @[simp]
      theorem TauCeti.SuzukiLieIndex.coe_finiteFixedSubgroupEquiv_apply (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : ↥(finiteFixedSubgroup m hvalid)) :
      ↑((finiteFixedSubgroupEquiv m hvalid) g) = (generatorEmbedding m hvalid) ↑g
      source
      @[simp]
      theorem TauCeti.SuzukiLieIndex.generatorEmbedding_finiteFixedSubgroupEquiv_symm_apply (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : ↥(Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg))) :
      (generatorEmbedding m hvalid) ↑((finiteFixedSubgroupEquiv m hvalid).symm g) = ↑g

      Descending an ambient fixed point and extending scalars again recovers that fixed point.