Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Suzuki.Candidate

The Suzuki candidate group is the group generated by the standard matrices #

Two constructions of the Suzuki group Sz(2^(2m+1)) sit side by side in Tau Ceti. One is TauCeti.SuzukiLieIndex.Group, the derived subgroup of the fixed points of the Steinberg endomorphism ฯ„ ^ (2m+1) of the rank-two symplectic carrier over an algebraic closure of ๐”ฝโ‚‚, modulo the centre of that derived subgroup. The other is TauCeti.suzukiGroup m, the subgroup of GLโ‚„(๐”ฝ_(2^(2m+1))) generated by the standard unipotent matrices u(a, b) and the Weyl matrix w. This file proves that the two are isomorphic, for every valid Suzuki index.

The fixed points are already known to be the generated group: scalar extension along the generator embedding identifies TauCeti.suzukiGroup m with TauCeti.SuzukiLieIndex.FixedPoints. What remains is that the two further steps of the fixed-point recipe do nothing here. The generated group is perfect once m โ‰  0, which validity of the index forces, and its centre is trivial at every parameter; both properties transport to the fixed points along that identification, and a perfect group with trivial centre is its own derived subgroup modulo the centre of that derived subgroup.

So the recipe returns the Steinberg fixed points unchanged on the Suzuki family, and the candidate group of a valid Suzuki index is the generated Suzuki group. On underlying matrices the resulting isomorphism is inverse to the generator embedding.

Neither group is asserted here to be finite or simple, and no order is computed: the statement is an isomorphism between the two constructions and nothing more.

Main definitions #

Main results #

References #

The fixed points are perfect and centreless #

source
instance TauCeti.SuzukiLieIndex.instIsPerfectFixedPoints {m : โ„•} {hvalid : (LieTypeIndex.suzuki m).Valid} :
Group.IsPerfect (of m hvalid).FixedPoints

The Steinberg fixed points of a valid Suzuki index are perfect. Validity of the index forces 1 โ‰ค m, which is what the corresponding statement about the generated group needs: at m = 0 that group is the solvable Frobenius group Sz(2) of order twenty.

source
@[simp]
theorem TauCeti.SuzukiLieIndex.center_fixedPoints_eq_bot {m : โ„•} {hvalid : (LieTypeIndex.suzuki m).Valid} :
Subgroup.center (of m hvalid).FixedPoints = โŠฅ

The Steinberg fixed points of a valid Suzuki index have trivial centre, the centre of the generated Suzuki group being trivial at every parameter.

The candidate group #

source
noncomputable def TauCeti.SuzukiLieIndex.groupEquivFixedPoints (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) :
(of m hvalid).Group โ‰ƒ* (of m hvalid).FixedPoints

The fixed-point recipe is the identity on the Suzuki family: the candidate group of a valid Suzuki index is its Steinberg fixed-point group, which is perfect with trivial centre and so is its own derived subgroup modulo the centre of that derived subgroup.

Instances For
    source
    @[simp]
    theorem TauCeti.SuzukiLieIndex.groupEquivFixedPoints_mk (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) (x : โ†ฅ(commutator (of m hvalid).FixedPoints)) :
    (groupEquivFixedPoints m hvalid) โ†‘x = โ†‘x

    The fixed-point equivalence sends the class represented by an element of the commutator subgroup to that element of the fixed-point group.

    source
    @[simp]
    theorem TauCeti.SuzukiLieIndex.groupEquivFixedPoints_symm_apply (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) (x : (of m hvalid).FixedPoints) :
    (groupEquivFixedPoints m hvalid).symm x = โ†‘โŸจx, โ‹ฏโŸฉ

    Read backwards, the fixed-point equivalence sends a fixed point to its class in the candidate group; every fixed point lies in the derived subgroup, the fixed points being perfect.

    source
    noncomputable def TauCeti.SuzukiLieIndex.groupEquivSuzukiGroup (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) :
    (of m hvalid).Group โ‰ƒ* โ†ฅ(suzukiGroup m)

    The candidate group of a valid Suzuki index is the generated Suzuki group: the derived subgroup of the Steinberg fixed points of ยฒBโ‚‚(2^(2m+1)), modulo the centre of that derived subgroup, is the subgroup of GLโ‚„(๐”ฝ_(2^(2m+1))) generated by the standard unipotent matrices and the Weyl matrix.

    Neither side is asserted to be finite or simple.

    Instances For
      source
      @[simp]
      theorem TauCeti.SuzukiLieIndex.groupEquivSuzukiGroup_mk (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) (x : โ†ฅ(commutator (of m hvalid).FixedPoints)) :
      (groupEquivSuzukiGroup m hvalid) โ†‘x = (suzukiGroupEquivFixedPoints m hvalid).symm โ†‘x

      The Suzuki-group equivalence sends the class represented by an element of the commutator subgroup to the corresponding element of the generated Suzuki group.

      source
      @[simp]
      theorem TauCeti.SuzukiLieIndex.groupEquivSuzukiGroup_symm_apply (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : โ†ฅ(suzukiGroup m)) :
      (groupEquivSuzukiGroup m hvalid).symm g = โ†‘โŸจ(suzukiGroupEquivFixedPoints m hvalid) g, โ‹ฏโŸฉ

      Read backwards, the identification sends an element of the generated Suzuki group to the class of the Steinberg fixed point it scalar-extends to; every fixed point lies in the derived subgroup, the fixed points being perfect.

      source
      theorem TauCeti.SuzukiLieIndex.generatorEmbedding_groupEquivSuzukiGroup_mk (m : โ„•) (hvalid : (LieTypeIndex.suzuki m).Valid) (x : โ†ฅ(commutator (of m hvalid).FixedPoints)) :
      (generatorEmbedding m hvalid) โ†‘((groupEquivSuzukiGroup m hvalid) โ†‘x) = โ†‘โ†‘โ†‘x

      The identification with the generated group is inverse to the generator embedding: the class of a Steinberg fixed point x goes to the element of the generated Suzuki group whose coordinate change and scalar extension is x.