The Steinberg map and candidate group of every valid Lie-type index

The thirteen ordinary and graph-twisted families use their existing assembly. The four half-Frobenius families use their explicit Suzuki, Ree, or Tits endomorphism. Every branch retains the validity proof of the input index; no carrier is assigned to an invalid index.

The candidate group is uniformly the derived subgroup of the fixed points modulo its centre. Comparison with the pinned simply connected groups requires isomorphisms preserving the root subgroups and Steinberg maps. No finiteness or simplicity of a candidate is asserted. The construction follows the family modules it imports.

Main definitions

• TauCeti.ValidLieTypeIndex.steinberg: the Steinberg endomorphism on the ambient group of each valid Lie-type index.
• TauCeti.ValidLieTypeIndex.FixedPoints: the fixed subgroup of the Steinberg endomorphism.
• TauCeti.ValidLieTypeIndex.Group: the Lie-type candidate group, the derived subgroup of the fixed points modulo its centre.

Main results

• TauCeti.ValidLieTypeIndex.steinberg_simpleRootSubgroup_of_not_usesHalfFrobenius: on ordinary and graph-twisted indices, the action on simple root subgroups permutes by the diagram automorphism and raises the parameter to the q-th power.
• TauCeti.ValidLieTypeIndex.steinberg_simpleRootSubgroup_of_usesHalfFrobenius: on the Suzuki, Ree and Tits indices, the action on simple root subgroups exchanges root lengths and raises the parameter to the odd half-Frobenius exponent.
• TauCeti.ValidLieTypeIndex.steinberg_steinberg_of_usesHalfFrobenius: on half-Frobenius families, the Steinberg endomorphism squares to the q-power Frobenius.
• TauCeti.ValidLieTypeIndex.Group_eq_of_not_usesHalfFrobenius: on ordinary and graph-twisted families, the candidate group agrees with GraphTwistedIndex.Group.

References

• R. W. Carter, Simple Groups of Lie Type, Wiley, 1972.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968).

noncomputable def TauCeti.ValidLieTypeIndex.steinberg (d : ValidLieTypeIndex) : d.AmbientGroup →* d.AmbientGroup

The actual Steinberg endomorphism on the carrier of each valid Lie-type index.

Equations

• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.suzuki m, hv⟩ = TauCeti.SuzukiLieIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.suzuki m, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.reeG2 m, hv⟩ = TauCeti.ReeG2LieIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.reeG2 m, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.reeF4 m, hv⟩ = TauCeti.ReeF4LieIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.reeF4 m, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.tits, hv⟩ = TauCeti.TitsLieIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.tits, hv⟩, TauCeti.ValidLieTypeIndex.steinberg._proof_4✝⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.A rank q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.A rank q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.twistedA rank q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.twistedA rank q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.B rank q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.B rank q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.C rank q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.C rank q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.D rank q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.D rank q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.twistedD rank q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.twistedD rank q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.E6 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.E6 q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.E7 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.E7 q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.E8 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.E8 q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.F4 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.F4 q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.G2 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.G2 q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.twistedE6 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩
• TauCeti.ValidLieTypeIndex.steinberg ⟨TauCeti.LieTypeIndex.trialityD4 q, hv⟩ = TauCeti.GraphTwistedIndex.steinberg ⟨⟨TauCeti.LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩

theorem TauCeti.ValidLieTypeIndex.steinberg_simpleRootSubgroup_of_not_usesHalfFrobenius (d : ValidLieTypeIndex) (h : ¬(↑d).UsesHalfFrobenius) (i : Fin d.rank) (u : Multiplicative d.Closure) : d.steinberg ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup ((GraphTwistedIndex.diagramPerm ⟨d, h⟩) i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ d.fieldOrder))

On ordinary and graph-twisted indices the assembled map has the recorded diagram action and field-order exponent.

theorem TauCeti.ValidLieTypeIndex.steinberg_simpleRootSubgroup_of_usesHalfFrobenius (d : ValidLieTypeIndex) (h : (↑d).UsesHalfFrobenius) (i : Fin d.rank) (u : Multiplicative d.Closure) : d.steinberg ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup ((SuzukiReeIndex.lengthPerm ⟨d, h⟩) i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (d.characteristic ^ SuzukiReeIndex.halfExponent ⟨d, h⟩ * SuzukiReeIndex.exponent ⟨d, h⟩ i)))

On the Suzuki, Ree and Tits indices the assembled map exchanges root lengths and raises the parameter to the odd half-Frobenius exponent.

theorem TauCeti.ValidLieTypeIndex.steinberg_steinberg_of_usesHalfFrobenius (d : ValidLieTypeIndex) (h : (↑d).UsesHalfFrobenius) (g : d.AmbientGroup) : d.steinberg (d.steinberg g) = d.frobenius g

On a half-Frobenius family, the assembled Steinberg map squares to the indexed field-order Frobenius.

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.FixedPoints (d : ValidLieTypeIndex) : Type

The fixed subgroup of the family's Steinberg endomorphism.

Equations

• d.FixedPoints = ↥(TauCeti.fixedSubgroup d.steinberg)

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.Group (d : ValidLieTypeIndex) : Type

The Lie-type candidate is the derived subgroup of the fixed points modulo its own centre. No finiteness or simplicity instance is assumed or supplied.

Equations

• d.Group = TauCeti.FixedPointCandidate d.steinberg

theorem TauCeti.ValidLieTypeIndex.Group_eq_of_not_usesHalfFrobenius (d : ValidLieTypeIndex) (h : ¬(↑d).UsesHalfFrobenius) : d.Group = GraphTwistedIndex.Group ⟨d, h⟩

On the thirteen ordinary or graph-twisted families, the assembled candidate is the existing graph-twisted assembly's candidate.