The type-A families in the CFSG list #
The full-weight type-A_r Chevalley carrier, its Frobenius endomorphism, and its pinned graph
automorphism are already available in Tau Ceti. This file connects that construction to the
validated indices for the two type-A families in the classification list:
A_r(q), ²A_r(q).
TauCeti.TypeALieIndex, the subtype of TauCeti.ValidLieTypeIndex consisting of exactly these two
constructors, is supplied by CFSG/Index.lean. Thus every group-valued definition below still
takes a validated Lie-type index: excluded ranks and duplicate representatives cannot reach a
carrier or Steinberg map.
For an index d, TauCeti.TypeALieIndex.AmbientGroup d is the group of
d.Closure-valued points of the explicit type-A carrier. Its positive simple-root subgroup at
the Bourbaki node i is TauCeti.TypeALieIndex.simpleRootSubgroup d i. The Steinberg map is the
entrywise q-power Frobenius on A_r(q) and the graph automorphism composed with that Frobenius
on ²A_r(q). The uniform pinned equation is
F (x_i(u)) = x_{γ i}(u ^ q),
where γ is the diagram permutation already attached to the index: the identity on A_r(q), and
on ²A_r(q) the reversal i ↦ i.rev of the zero-based Bourbaki numbering. Finally,
TauCeti.TypeALieIndex.Group d applies the roadmap's fixed-points, derived-subgroup, and
central-quotient recipe to this endomorphism.
The Steinberg map is also split back into its two factors. TauCeti.TypeALieIndex.frobenius is the
q-power Frobenius, which is the same map on both families, and
TauCeti.TypeALieIndex.graphAut is the pinned graph automorphism realizing the index's diagram
permutation: the identity on A_r(q) and signed reverse inverse transpose on ²A_r(q). Their
pinned equations are Frob_q (x_i(u)) = x_i(u ^ q) and the sign-free γ (x_i(u)) = x_{γ i}(u),
and the two factorizations
F = γ ∘ Frob_q = Frob_q ∘ γ
carry the relations that milestone L1 asks of a graph-twisted Steinberg map: the twist order of the
diagram permutation γ realizes annihilates γ, that is γ = 1 on A_r(q) and γ ^ 2 = 1 on
²A_r(q), and γ commutes with the Frobenius. Its exact order is not proved here.
The branch equations steinberg_ofA and steinberg_ofTwistedA name the Steinberg map of each
family as TauCeti.SlStd.frobenius and TauCeti.SlStd.twistedFrobenius outright, so the upstream
results about those maps apply to d.steinberg directly and are not restated here. The upstream
lemmas include the commutation TauCeti.SlStd.graphAutomorphismPoints_comp_frobenius and the
involution equation TauCeti.SlStd.graphAutomorphismPoints_graphAutomorphismPoints required by
milestone L1. Separately, TauCeti.SlStd.twistedFrobenius_comp_self supplies the square relation
for the composite Steinberg map. The fixed-point identification
TauCeti.SlStd.map_subtype_fixedSubgroup_frobenius_eq and the containment
TauCeti.SlStd.map_subtype_fixedSubgroup_twistedFrobenius_le are available in the same way. The
lemma simpleRootSubgroup_def plays this role for the root subgroups.
The definitions in this file are specific to TypeALieIndex. Their uniform
ValidLieTypeIndex.AmbientGroup and ValidLieTypeIndex.frobenius counterparts are assembled from
the family constructions in TauCeti.GroupTheory.SpecificGroups.CFSG.Assembly.AmbientGroup. The
uniform GraphTwistedIndex.graphAut is assembled from the family graph automorphisms in
TauCeti.GroupTheory.SpecificGroups.CFSG.Assembly.GraphTwisted. Nothing here asserts that a
constructed group is finite or simple.
Main declarations #
TauCeti.TypeALieIndex.AmbientGroup: the algebraic-closure-valued points of the full-weight type-A carrier.TauCeti.TypeALieIndex.simpleRootSubgroupandTauCeti.TypeALieIndex.simpleRootSubgroup_def: the positive simple-root subgroup at a Bourbaki node, and its identification with the carrier's numbered root subgroup.TauCeti.TypeALieIndex.steinberg, withTauCeti.TypeALieIndex.steinberg_ofAandTauCeti.TypeALieIndex.steinberg_ofTwistedA: Frobenius onA_r(q)and graph-twisted Frobenius on²A_r(q).TauCeti.TypeALieIndex.steinberg_simpleRootSubgroup: the pinned simple-root-subgroup equation.TauCeti.TypeALieIndex.frobeniusandTauCeti.TypeALieIndex.frobenius_simpleRootSubgroup: theq-power Frobenius factor and its pinned equation.TauCeti.TypeALieIndex.graphAut, withTauCeti.TypeALieIndex.graphAut_ofAandTauCeti.TypeALieIndex.graphAut_ofTwistedA: the pinned graph automorphism factor.TauCeti.TypeALieIndex.graphAut_simpleRootSubgroup: its pinned simple-root-subgroup equationγ (x_i(u)) = x_{γ i}(u), with no field power and no sign.TauCeti.TypeALieIndex.graphAut_pow_twistOrderandTauCeti.TypeALieIndex.graphAut_comp_frobenius: the order relation on the graph factor, and its commutation with the Frobenius.TauCeti.TypeALieIndex.steinberg_eq_graphAut_comp_frobeniusandTauCeti.TypeALieIndex.steinberg_eq_frobenius_comp_graphAut: the Steinberg map is the composite of the two factors, in either order.TauCeti.TypeALieIndex.FixedPointsandTauCeti.TypeALieIndex.Group: the fixed group and its derived central quotient.TauCeti.TypeALieIndex.primeFrobenius, withTauCeti.TypeALieIndex.primeFrobenius_simpleRootSubgroupandTauCeti.TypeALieIndex.frobenius_eq_primeFrobenius_pow: the prime-field Frobenius, its pinned equationFrob_p (x_i(u)) = x_i(u ^ p), and theq-power Frobenius as itse-th power.
References #
- R. W. Carter, Simple Groups of Lie Type, Chapters 2 and 14.
- R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
- R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
- The target signatures realized here follow the human-authored formal skeleton
TauCetiRoadmap/CFSGStatement/Suggested.lean: the ambient group, the numbered simple root subgroup, the Steinberg map and its pinned equationx_i(u) ↦ x_{γ i}(u ^ q), the fixed points, and the derived central quotient, all taken on a validated-index subtype.
The algebraic-closure-valued points of the explicit full-weight type-A Chevalley carrier.
Equations
- d.AmbientGroup = ↥(TauCeti.SlStd.points (↑d).rank (↑d).Closure)
Instances For
The positive simple-root subgroup at the Bourbaki-numbered node i of a type-A carrier.
Equations
- d.simpleRootSubgroup i = TauCeti.SlStd.rootSubgroupPoints (↑d).rank (Sum.inl i) (↑d).Closure
Instances For
The simple-root subgroup is the carrier's numbered root subgroup at the positive simple root
i. This is the equation through which the upstream root-subgroup API reaches
simpleRootSubgroup. It is not a simp lemma: steinberg_simpleRootSubgroup is the normal form
the pinned equations of this file are stated against, and unfolding to
TauCeti.SlStd.rootSubgroupPoints would keep it from firing.
The Steinberg endomorphism of a validated type-A index. It is the q-power Frobenius on
A_r(q) and the reversal graph automorphism composed with that Frobenius on ²A_r(q).
The two branch equations steinberg_ofA and steinberg_ofTwistedA name the selected upstream map
on each family, so no consumer needs this body.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On A_r(q) the Steinberg map is the q-power Frobenius of the standard carrier.
On ²A_r(q) the Steinberg map is the graph-twisted q-power Frobenius of the standard
carrier, that is, the pinned reversal graph automorphism composed with the Frobenius.
The Steinberg map has the pinned action on every positive simple-root subgroup. It sends
x_i(u) to x_{γ i}(u ^ q), where γ is the diagram permutation of the index and q is its
recorded field order.
The two factors of the Steinberg map #
The q-power Frobenius endomorphism of a type-A ambient group, for q the Frobenius
parameter recorded by the index. It is the same map on both type-A families: what distinguishes
²A_r(q) from A_r(q) is the graph automorphism TauCeti.TypeALieIndex.graphAut its Steinberg
map composes with this one.
Equations
- d.frobenius = TauCeti.SlStd.frobenius (↑d).rank (↑d).characteristic (↑d).fieldExponent (↑d).Closure
Instances For
The type-A Frobenius is the standard carrier's Frobenius at the characteristic and field exponent recorded by the index.
The Frobenius fixes the Bourbaki numbering of a positive simple-root subgroup and raises its
parameter to the q-th power, that is, Frob_q (x_i(u)) = x_i(u ^ q).
The prime-field Frobenius endomorphism of a type-A ambient group, the p-power map for p
the defining characteristic. The q-power Frobenius TauCeti.TypeALieIndex.frobenius is its
e-th power, for e the field exponent the index records, by frobenius_eq_primeFrobenius_pow.
The two agree when the index has prime field order.
Equations
- d.primeFrobenius = TauCeti.SlStd.frobenius (↑d).rank (↑d).characteristic 1 (↑d).Closure
Instances For
The prime-field Frobenius is the standard carrier's Frobenius at exponent one.
The prime-field Frobenius fixes the Bourbaki numbering of a positive simple-root subgroup and
raises its parameter to the p-th power, that is, Frob_p (x_i(u)) = x_i(u ^ p).
The q-power Frobenius is the e-th power of the prime-field Frobenius, for e the field
exponent the index records.
The pinned graph automorphism of a validated type-A index. It realizes on the ambient group
the diagram permutation TauCeti.GraphTwistedIndex.diagramPerm already attached to the index: it is
the identity on A_r(q), whose diagram permutation is trivial, and signed reverse inverse transpose
on ²A_r(q), which reverses the Bourbaki numbering.
The two branch equations graphAut_ofA and graphAut_ofTwistedA name the selected map on each
family, so no consumer needs this body.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On A_r(q) the graph automorphism is trivial: the A_r diagram symmetry is not used by the
untwisted family.
On ²A_r(q) the graph automorphism is the standard carrier's pinned graph automorphism, signed
reverse inverse transpose.
The graph automorphism has the pinned action on every positive simple-root subgroup: it
sends x_i(u) to x_{γ i}(u), where γ is the diagram permutation of the index. The parameter is
carried across unchanged, with neither a field power nor a sign; on a general root the equation
would acquire a sign forced by the Chevalley structure constants.
The graph automorphism of a type-A index is an involution.
The graph automorphism of a type-A index squares to the identity in the automorphism group.
The twist order of a type-A index annihilates its graph automorphism, so γ = 1 on
A_r(q) and γ ^ 2 = 1 on ²A_r(q). This is the order relation milestone L1 asks of the graph
factor of a Steinberg map, and it matches TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder on
the diagram permutation that γ realizes.
The graph automorphism commutes with the Frobenius.
The graph automorphism commutes with the Frobenius, as an identity of endomorphisms. This is
the relation γ ∘ Frob_q = Frob_q ∘ γ required of the graph-twisted families by milestone L1.
The Steinberg map of a type-A index is its graph automorphism composed with its Frobenius,
uniformly on both families. On A_r(q) the graph factor is trivial, so the composite is the
Frobenius itself.
The Steinberg map may equally be read with its Frobenius factor last, the two factors commuting.
The finite-group candidate #
The fixed subgroup of the Steinberg endomorphism attached to a type-A index.
Equations
Instances For
The finite-simple-group candidate attached to a type-A index: the derived subgroup of the Steinberg fixed points, modulo the centre of that derived subgroup. No finiteness or simplicity assertion is part of this definition.