Matrix equations for the Suzuki fixed points

For a validated Suzuki index with field order q = 2^(2m+1), the fixed points of the Steinberg map τ^(2m+1) are exactly the symplectic matrices satisfying

τ(g) = g^[2^(m+1)],

where the right side raises each matrix entry to the indicated power. On the left, τ(g) is the matrix of two-by-two minors on the four coordinate pairs (0,1), (0,3), (2,3), (1,2). Thus the criterion gives explicit polynomial equations, without expanding the odd iterate of the special isogeny. Every solution has entries in the recorded copy of 𝔽_q inside the algebraic closure.

mem_map_fixedSubgroup_steinberg_iff reads this criterion in the general linear group, including the symplectic equation. It supplies a matrix description with which a generator-based construction can be compared: after identifying the coefficient fields and coordinates, one must show that the generators satisfy these equations and exhaust their solutions. The fixed-field coefficient theorem supplies the field-membership step for that comparison. No generation theorem, derived-subgroup calculation, or identification with another construction of the Suzuki group is asserted.

The explicit carrier is not identified with the pinned simply connected group scheme of its diagram. Constructions on it transfer to that pinned group only along such an identification, once one is proved.

The calculation uses the special-isogeny square relation already proved in TauCeti.Algebra.Lie.Symplectic.StandardCarrier.SpecialIsogeny and the odd-power construction in TauCeti.GroupTheory.SpecificGroups.CFSG.Suzuki.Basic.

theorem TauCeti.SuzukiLieIndex.mem_fixedSubgroup_steinberg_iff (d : SuzukiLieIndex) (g : d.toRankTwoBLieIndex.AmbientGroup) : g ∈ fixedSubgroup d.steinberg ↔ ∀ (i j : Fin 4), (↑↑g).symplecticSpecialIsogeny i j = ↑↑g i j ^ 2 ^ (d.toSuzukiReeIndex.halfExponent + 1)

A carrier point is fixed by the Suzuki Steinberg map exactly when the matrix of its special isogeny equals its entrywise 2^(m+1)-st power.

theorem TauCeti.SuzukiLieIndex.mem_map_fixedSubgroup_steinberg_iff (d : SuzukiLieIndex) (g : GL (Fin 4) (↑d).Closure) : g ∈ Subgroup.map (SpStd.points 1 (↑d).Closure).subtype (fixedSubgroup d.steinberg) ↔ ↑g * JFin 2 (↑d).Closure * (↑g).transpose = JFin 2 (↑d).Closure ∧ ∀ (i j : Fin 4), (↑g).symplecticSpecialIsogeny i j = ↑g i j ^ 2 ^ (d.toSuzukiReeIndex.halfExponent + 1)

The image of the Suzuki fixed subgroup in GL₄ is cut out by the symplectic equation and the special-isogeny minor equations. The alternating form uses the coordinate pairs (0,2) and (1,3), as in JFin 2.

theorem TauCeti.SuzukiLieIndex.coe_mem_fixedField_of_mem_fixedSubgroup_steinberg (d : SuzukiLieIndex) (g : d.toRankTwoBLieIndex.AmbientGroup) (hg : g ∈ fixedSubgroup d.steinberg) (i j : Fin 4) : ↑↑g i j ∈ (↑d).fixedField

Every matrix entry of a Suzuki Steinberg fixed point belongs to the recorded field of order 2^(2m+1).