The standard symplectic carrier and the candidate group of a validated type-C index #
The type-C branch of the classification list is built on the type-C diagram of rank n, and
Tau Ceti's explicit full-weight Chevalley carrier for that diagram is TauCeti.SpStd.groupScheme,
the Kostant toral closure of the standard representation of sp_(2n) inside GL_(2n) over ℤ.
This file attaches that carrier to a validated type-C index: the group of algebraic-closure-valued
points of the carrier at the index's rank, its Bourbaki-numbered simple root subgroups, and the
reading of their root characters in the type-C root datum the index names.
The carrier also has a q-power Frobenius, where q is the field order recorded by the index: the
endomorphism of its point group raising every matrix entry to the q-th power. This file records
that entrywise action, the equations it satisfies on the numbered simple-root subgroups and on the
split weight torus, where it raises the subgroup parameter and every torus coordinate to the q-th
power, and the description of its fixed points as the carrier points all of whose matrix entries lie
in the field of q elements inside the closure.
The carrier is indexed by n in the spelling C (n + 1), so a validated index of rank r uses
the carrier at TauCeti.TypeCLieIndex.carrierRank, which is r - 1. That subtraction is harmless
because TauCeti.TypeCLieIndex.three_le_rank bounds the rank below by three:
TauCeti.TypeCLieIndex.carrierRank_add_one recovers r, and every numbered object below is indexed
by Fin d.1.rank, the upstream Bourbaki index type of the index's own Dynkin type, rather than by a
node of the carrier. The two numberings agree node for node, so
TauCeti.TypeCLieIndex.carrierNode is the rank identification and nothing more; that is what
TauCeti.TypeCLieIndex.rootGeneratorWeight_carrierNode_eq_root_simpleIndex records, reading the
character of the i-th raising subgroup as the i-th simple root of the type-C root datum the
index names.
The rank-two member of the same carrier family is not reached from here. TauCeti.DynkinType.C 2
is not a valid Dynkin type, the rank-two root system being carried by B 2, and correspondingly a
validated type-C index has rank at least three. The rank-two carrier serves the Suzuki family
instead, in TauCeti/GroupTheory/SpecificGroups/CFSG/TypeB/Two/Basic.lean, where the node
correspondence
acquires the swap of the two Bourbaki nodes.
The family is untwisted, so its Steinberg endomorphism is that Frobenius outright:
TauCeti.TypeCLieIndex.diagramPerm_eq_one records that the diagram permutation attached to the
index is trivial, and TauCeti.TypeCLieIndex.steinberg is the Frobenius read as the Steinberg map.
The candidate group of the family is then the derived subgroup of the Steinberg fixed points modulo
the centre of that derived subgroup,
H_d = fixedSubgroup d.steinberg, d.Group = [H_d, H_d] / Z([H_d, H_d]).
Nothing here asserts that the carrier is reductive, that its weight torus is maximal, or that its
point group or any group formed from it is finite, perfect, or simple. The identification of its
points with the points of the symplectic group scheme over ℤ, matching the numbered simple-root
subgroups and intertwining the Steinberg endomorphism with entrywise Frobenius, is
TauCeti.TypeCLieIndex.carrierEquivPinned in
TauCeti.GroupTheory.SpecificGroups.CFSG.TypeC.Agreement.
Main declarations #
TauCeti.TypeCLieIndex.AmbientGroup: the algebraic-closure-valued points of the standard symplectic carrier at the index's rank.TauCeti.TypeCLieIndex.simpleRootSubgroup: its positive simple-root subgroup at a Bourbaki-numbered node, withTauCeti.TypeCLieIndex.rootGeneratorWeight_carrierNode_eq_root_simpleIndexidentifying the character of that subgroup with the corresponding simple root of the type-Croot datum.TauCeti.TypeCLieIndex.frobenius: the carrier'sq-power Frobenius, withTauCeti.TypeCLieIndex.frobenius_simpleRootSubgroupandTauCeti.TypeCLieIndex.frobenius_weightTorusPointsrecording its action on the numbered simple-root subgroups and split weight torus.TauCeti.TypeCLieIndex.mem_fixedSubgroup_frobenius_iff: its fixed points are the carrier points whose matrix entries all lie in the field ofqelements inside the closure.TauCeti.TypeCLieIndex.steinberg,TauCeti.TypeCLieIndex.steinberg_simpleRootSubgroupandTauCeti.TypeCLieIndex.mem_fixedSubgroup_steinberg_iff: the Steinberg endomorphism of the untwisted family, its simple-root-subgroup action formula, and the description of the group it fixes.TauCeti.TypeCLieIndex.FixedPointsandTauCeti.TypeCLieIndex.Group: that fixed group and the candidate group ofCₙ(q), its derived central quotient.TauCeti.TypeCLieIndex.primeFrobenius, withTauCeti.TypeCLieIndex.primeFrobenius_simpleRootSubgroup,TauCeti.TypeCLieIndex.primeFrobenius_weightTorusPointsandTauCeti.TypeCLieIndex.frobenius_eq_primeFrobenius_pow: the prime-field Frobenius, its pinned equationFrob_p (x_i(u)) = x_i(u ^ p), its action on the split weight torus, and theq-power Frobenius as itse-th power.
References #
- R. W. Carter, Simple Groups of Lie Type, §§4.4 and 11.3.
- R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17, for the entrywise Frobenius action.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III, for the numbering of the
type-
Cdiagram that the root subgroups below are indexed by.
The carrier rank and the node correspondence #
The rank parameter of the standard symplectic carrier serving a validated type-C index.
TauCeti.SpStd.groupScheme n is the carrier of type C (n + 1), so the carrier serving an index
of rank r is the one at r - 1. The subtraction never truncates, r being at least three by
TauCeti.TypeCLieIndex.three_le_rank; TauCeti.TypeCLieIndex.carrierRank_add_one is the
identification that recovers r.
Equations
- d.carrierRank = (↑d).rank - 1
Instances For
The carrier rank of a validated type-C index is one less than its rank. It is oriented
towards TauCeti.ValidLieTypeIndex.rank, so that simp normalizes the successor of the carrier
rank to the rank the index's own Bourbaki index type is built on.
The carrier node numbered by a Bourbaki node of the index's diagram. Unlike the rank-two
correspondence of the Suzuki family, this is the rank identification and nothing else: the standard
symplectic carrier at TauCeti.TypeCLieIndex.carrierRank numbers its generators by the Bourbaki
numbering of the type-C diagram that the index names, node for node.
Equations
- d.carrierNode i = Fin.cast ⋯ i
Instances For
The node correspondence transports the type-C Cartan matrix. The entry at a pair of
carrier nodes is the entry at the pair of Bourbaki nodes they number: carrierNode moves no node
value, only the rank its index type is built on, and TauCeti.TypeCLieIndex.carrierRank_add_one
identifies the two ranks.
The ambient group and its simple root subgroups #
The ambient group this file attaches to a validated type-C index: the points of the
explicit full-weight standard symplectic Chevalley carrier at the index's rank, over the algebraic
closure of its prime field. No finiteness, reductivity, pinning or maximality statement is attached
to it; its identification with the points of the symplectic group scheme over ℤ is
TauCeti.TypeCLieIndex.carrierEquivPinned.
Equations
- d.AmbientGroup = ↥(TauCeti.SpStd.points d.carrierRank (↑d).Closure)
Instances For
The positive simple-root subgroup at the Bourbaki-numbered node i of the type-C diagram. It
is the carrier's numbered raising subgroup at the node that carrierNode names.
Equations
- d.simpleRootSubgroup i = TauCeti.SpStd.rootSubgroupPoints d.carrierRank (Sum.inl (d.carrierNode i)) (↑d).Closure
Instances For
The simple-root subgroup is the carrier's numbered raising subgroup at the corresponding carrier node.
The simple-root subgroups sit at the simple roots of the type-C root datum. The character
by which the carrier's split torus rescales the parameter of simpleRootSubgroup i, read in the
same node correspondence, is the i-th simple root of
TauCeti.DynkinType.simplyConnectedRootDatum at the Dynkin type the index names. This is the sense
in which the standard symplectic carrier serves that diagram; it is not a claim that the carrier is
the pinned group of the diagram, no pinning being constructed for it.
Frobenius on the carrier #
The q-power Frobenius of the standard symplectic carrier attached to a validated type-C
index, where q is the field order recorded by the index. It is the endomorphism of the point
group raising every matrix entry to the q-th power.
Equations
- d.frobenius = TauCeti.SpStd.frobenius d.carrierRank (↑d).characteristic (↑d).fieldExponent (↑d).Closure
Instances For
The Frobenius is the standard carrier's Frobenius at the characteristic and field exponent recorded by the index.
The Frobenius raises every matrix entry to the field order recorded by the index.
The Frobenius fixes the numbering of a 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 of the standard symplectic carrier attached to a validated type-C
index, the p-power map for p the defining characteristic. The q-power Frobenius is its
e-th power, for e the field exponent the index records, by
frobenius_eq_primeFrobenius_pow.
Equations
- d.primeFrobenius = TauCeti.SpStd.frobenius d.carrierRank (↑d).characteristic 1 (↑d).Closure
Instances For
The prime-field Frobenius is the standard carrier's Frobenius at exponent one.
The prime-field Frobenius acts on the ambient group by raising every matrix entry to the
p-th power, for p the defining characteristic.
The prime-field Frobenius fixes the numbering of a 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 prime-field Frobenius raises every coordinate of the split weight torus to the p-th
power.
The Frobenius raises every coordinate of the split weight torus to the q-th power.
A point of the ambient group is fixed by the Frobenius exactly when all of its matrix entries
lie in the field of definition. Writing 𝔽_q for TauCeti.ValidLieTypeIndex.fixedField, the copy
of the field of q elements inside the algebraic closure, the fixed points of the Frobenius are the
points of the standard symplectic carrier whose entries all lie in 𝔽_q.
The Steinberg endomorphism #
The Steinberg endomorphism of a validated type-C index: the q-power Frobenius of the
ambient group, q being the field order the index records. The family is untwisted, so no diagram
automorphism and no half-Frobenius enters; TauCeti.TypeCLieIndex.diagramPerm_eq_one records that
the diagram permutation attached to the index is trivial.
It is formed on the standard symplectic carrier;
TauCeti.TypeCLieIndex.carrierEquivPinned_steinberg matches it with entrywise Frobenius on the
points of the symplectic group scheme over ℤ.
Instances For
The Steinberg map of a type-C index equals the carrier's Frobenius.
The Steinberg map fixes the numbering of a simple-root subgroup and raises its parameter to
the q-th power, that is, Frob_q (x_i(u)) = x_i(u ^ q), the simple-root-subgroup action
formula of an untwisted Steinberg endomorphism.
A point of the ambient group is fixed by the Steinberg map exactly when all of its matrix
entries lie in the field of definition, so the fixed group H_d of the family is the group of
points of the standard symplectic carrier whose entries lie in 𝔽_q. Like
mem_fixedSubgroup_frobenius_iff, it is not a simp lemma.
The finite-group candidate #
The fixed subgroup of the Steinberg endomorphism attached to a type-C index.
Equations
Instances For
The finite-simple-group candidate attached to a type-C 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.