Standard generators inside the Suzuki fixed points

The generator presentation of Sz(2^(2m+1)) and its Steinberg fixed-point construction use different coefficient fields. This file chooses an embedding of the generator field into the algebraic closure of a valid Suzuki index and proves that the standard generators belong to the Steinberg fixed subgroup. Consequently scalar extension maps the generated Suzuki group into that fixed subgroup.

This is the inclusion half of the comparison. It does not assert that the standard generators exhaust the fixed points, nor identify the derived central quotient with the generated group.

References

• M. Suzuki, On a class of doubly transitive groups, Annals of Mathematics 75 (1962), 105--145.

def TauCeti.Suzuki.coordinateSwap : Fin 4 ≃ Fin 4

The coordinate change from the standard generator model to the standard symplectic carrier. It exchanges the final two basis vectors.

theorem TauCeti.Suzuki.coordinateSwap_def : coordinateSwap = Equiv.swap 2 3

The coordinate change is the transposition of the final two basis vectors.

@[reducible, inline]

abbrev TauCeti.Suzuki.coordinateEquiv (R : Type u_1) [CommSemiring R] : GL (Fin 4) R ≃* GL (Fin 4) R

Simultaneous row and column reindexing from the standard generator coordinates to the coordinates used by SpStd.

theorem TauCeti.Suzuki.coordinateEquiv_unipotent_mul_jFin_mul_transpose (m : ℕ) (a b : GaloisField 2 (2 * m + 1)) : ↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (unipotent m a b)) * JFin 2 (GaloisField 2 (2 * m + 1)) * (↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (unipotent m a b))).transpose = JFin 2 (GaloisField 2 (2 * m + 1))

After the standard coordinate change, every unipotent Suzuki generator preserves the alternating form used by SpStd.

theorem TauCeti.Suzuki.coordinateEquiv_weyl_mul_jFin_mul_transpose (m : ℕ) : ↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (weyl m)) * JFin 2 (GaloisField 2 (2 * m + 1)) * (↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (weyl m))).transpose = JFin 2 (GaloisField 2 (2 * m + 1))

After the standard coordinate change, the Weyl generator preserves the alternating form used by SpStd.

theorem TauCeti.Suzuki.symplecticSpecialIsogeny_coordinateEquiv_unipotent (m : ℕ) (a b : GaloisField 2 (2 * m + 1)) : (↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (unipotent m a b))).symplecticSpecialIsogeny = (↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (unipotent m a b))).map fun (x : GaloisField 2 (2 * m + 1)) => x ^ 2 ^ (m + 1)

After the standard coordinate change, the special isogeny sends a unipotent generator to its entrywise 2^(m+1)-st power.

theorem TauCeti.Suzuki.symplecticSpecialIsogeny_coordinateEquiv_weyl (m : ℕ) : (↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (weyl m))).symplecticSpecialIsogeny = (↑((coordinateEquiv (GaloisField 2 (2 * m + 1))) (weyl m))).map fun (x : GaloisField 2 (2 * m + 1)) => x ^ 2 ^ (m + 1)

After the standard coordinate change, the special isogeny fixes the Weyl generator.

noncomputable def TauCeti.SuzukiLieIndex.generatorFieldEmbedding (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : GaloisField 2 (2 * m + 1) →+* (↑(of m hvalid)).Closure

A finite-field embedding from the coefficient field of the standard generators into the algebraic closure used by a valid Suzuki index.

noncomputable def TauCeti.SuzukiLieIndex.generatorEmbedding (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : GL (Fin 4) (GaloisField 2 (2 * m + 1)) →* GL (Fin 4) (↑(of m hvalid)).Closure

Scalar extension of the coordinate-changed generator model into the algebraic closure of a valid Suzuki index.

@[simp]

theorem TauCeti.SuzukiLieIndex.generatorEmbedding_apply (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : GL (Fin 4) (GaloisField 2 (2 * m + 1))) (i j : Fin 4) : ↑((generatorEmbedding m hvalid) g) i j = (generatorFieldEmbedding m hvalid) (↑((Suzuki.coordinateEquiv (GaloisField 2 (2 * m + 1))) g) i j)

Scalar extension acts entrywise after the coordinate change.

theorem TauCeti.SuzukiLieIndex.generatorEmbedding_injective (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : Function.Injective ⇑(generatorEmbedding m hvalid)

The scalar extension and coordinate change used for the generator model are injective.

theorem TauCeti.SuzukiLieIndex.coe_generatorEmbedding (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : GL (Fin 4) (GaloisField 2 (2 * m + 1))) : ↑((generatorEmbedding m hvalid) g) = (↑((Suzuki.coordinateEquiv (GaloisField 2 (2 * m + 1))) g)).map ⇑(generatorFieldEmbedding m hvalid)

The underlying matrix of a scalar-extended generator is the coordinate-changed matrix with the field embedding applied entrywise.

theorem TauCeti.SuzukiLieIndex.generatorEmbedding_mem_map_fixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : GL (Fin 4) (GaloisField 2 (2 * m + 1))) (hsymp : ↑((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))) (hiso : (↑((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)) : (generatorEmbedding m hvalid) g ∈ Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg)

A generator whose coordinate change preserves the alternating form and satisfies the special-isogeny equation over the generator field is, after scalar extension, a Steinberg fixed point.

theorem TauCeti.SuzukiLieIndex.generatorEmbedding_unipotent_mem_map_fixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (a b : GaloisField 2 (2 * m + 1)) : (generatorEmbedding m hvalid) (Suzuki.unipotent m a b) ∈ Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg)

Every coordinate-changed unipotent generator, extended to the algebraic closure, is a Steinberg fixed point.

theorem TauCeti.SuzukiLieIndex.generatorEmbedding_weyl_mem_map_fixedSubgroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : (generatorEmbedding m hvalid) (Suzuki.weyl m) ∈ Subgroup.map (SpStd.points 1 (↑(of m hvalid)).Closure).subtype (fixedSubgroup (of m hvalid).steinberg)

The coordinate-changed Weyl generator, extended to the algebraic closure, is a Steinberg fixed point.

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

The coordinate-changed standard generator model embeds into the image in GL₄ of the Suzuki Steinberg fixed subgroup.