The three families on a type-D diagram, and the candidate groups of Dₙ(q) and ²Dₙ(q) #
Three classification-list families are built on the diagram Dₙ: the untwisted Dₙ(q), the
graph-twisted ²Dₙ(q), and, at rank four, the triality-twisted ³D₄(q). They share a diagram, and
TauCeti.TypeDDiagramLieIndex is the subtype that collects exactly them.
This file attaches to such an index the group of algebraic-closure-valued points of Tau Ceti's
explicit full-weight type-D spin Chevalley carrier at the index's own rank,
TauCeti.TypeDSpinCarrier.points, together with that group's Bourbaki-numbered simple root
subgroups and its q-power Frobenius; and it then forms the Steinberg endomorphism and the
candidate group on the untwisted branch, where the Frobenius is the Steinberg map, and on the
graph-twisted branch, where the Steinberg map is the Frobenius composed with the fork-exchange
graph automorphism of the carrier.
The rank is available because it is at least four on this subtype, by
TauCeti.TypeDDiagramLieIndex.four_le_rank, which is exactly the hypothesis the carrier takes: the
carrier is built from the type-Dₙ Serre presentation, whose diagram is A₁ × A₁ at rank two and
A₃ at rank three, so it is offered only in the range where Dₙ is a valid Dynkin type.
The spin carrier rather than the Geck carrier is used because the Geck carrier is built from the
adjoint representation, so its weights span the whole character lattice exactly in the types E₈,
F₄ and G₂, by TauCeti.DynkinType.span_range_geckWeight_eq_top_iff. A type-D diagram is not
one of those, by TauCeti.LieTypeIndex.not_hasUnimodularDiagram_of_hasTypeDDiagram, and the full
spin representation is what sees both spinor cosets of the type-D root lattice; its weights span
that lattice, by TauCeti.TypeDSpinCarrier.span_range_basisWeight_eq_top.
The three Steinberg maps #
The three families differ exactly in the endomorphism whose fixed points the classification recipe
takes. On the untwisted branch that endomorphism is the q-power Frobenius outright, and
TauCeti.TypeDLieIndex.diagramPerm_toGraphTwistedIndex checks that the diagram permutation the
index carries is trivial. So TauCeti.TypeDLieIndex.steinberg is the shared Frobenius, and the
recipe
H_d = fixedSubgroup d.steinberg, d.Group = [H_d, H_d] / Z([H_d, H_d])
runs on this branch, on the spin carrier.
On the graph-twisted branch the Steinberg map is γ₂ ∘ Frob_q, where γ₂ is the graph
automorphism TauCeti.TypeDSpinCarrier.graphAutPoints of the carrier, conjugation by a signed
permutation matrix of the spin coordinates. It realizes the diagram permutation the index carries,
the fork exchange TauCeti.graphPermD, by the pinned equation γ₂ (x_i(u)) = x_{σ i}(u) on the
simple-root subgroups, it is an involution, and it commutes with the Frobenius, so that
F = γ₂ ∘ Frob_q = Frob_q ∘ γ₂, F (x_i(u)) = x_{σ i}(u ^ q).
TauCeti.TypeTwistedDLieIndex.steinberg is this composite and the same recipe runs on it. The
Frobenius fixed points are the points with entries in 𝔽_q; the fixed points of the composite are
not characterized here.
The triality-twisted branch takes γ₃ ∘ Frob_q for an order-three symmetry that has no linear
realization on the spin module: triality permutes the three eight-dimensional representations of
D₄, so the spin module 8ₛ ⊕ 8_c is not stable under it and no fixed linear automorphism of that
module realizes it. (The spin representation is faithful, so triality does act on the spin carrier
as an abstract automorphism; it is an explicit linear realization that is missing.) The ³D₄(q)
branch is therefore built on the tripled carrier TauCeti.D4Tripled.groupScheme, on which triality
is a permutation of the weight basis, in TauCeti/GroupTheory/SpecificGroups/CFSG/TrialityD4.lean;
the spin-carrier points and Frobenius attached below to a triality-twisted index are not the
ambient group and Frobenius of that branch.
The spin carrier is not identified with the pinned simply connected Chevalley--Demazure group
scheme of type Dₙ, and nothing here identifies the two: the constructions below transfer to that
pinned group only along such an identification, once one is proved. Nor is it asserted that the
carrier is reductive, that its weight torus is maximal, or that any group below is finite, perfect,
or simple.
Main declarations #
TauCeti.TypeDDiagramLieIndex.AmbientGroup: the algebraic-closure-valued points of the full-weight type-Dspin carrier at the rank the index names, the group inside which the classification recipe is run on the two branches below.TauCeti.TypeDDiagramLieIndex.simpleRootSubgroup: the positive simple-root subgroup at a Bourbaki node.TauCeti.TypeDDiagramLieIndex.rootGeneratorWeight_eq_root_simpleIndex: the character of that subgroup is the corresponding simple root of the root datum of the Dynkin type the index names.TauCeti.TypeDDiagramLieIndex.frobenius,TauCeti.TypeDDiagramLieIndex.coe_frobenius_applyandTauCeti.TypeDDiagramLieIndex.frobenius_simpleRootSubgroup: theq-power Frobenius, its entrywise description, and its pinned equationFrob_q (x_i(u)) = x_i(u ^ q).TauCeti.TypeDDiagramLieIndex.mem_fixedSubgroup_frobenius_iff: its fixed points are the points whose matrix entries lie in the field of definition𝔽_q.TauCeti.TypeDLieIndex.steinbergandTauCeti.TypeDLieIndex.Group: the Steinberg endomorphism of the untwisted familyDₙ(q), which is the Frobenius, and its candidate group.TauCeti.TypeTwistedDLieIndex.graphAut, withTauCeti.TypeTwistedDLieIndex.graphAut_simpleRootSubgroup,TauCeti.TypeTwistedDLieIndex.graphAut_sq,TauCeti.TypeTwistedDLieIndex.graphAut_pow_twistOrderandTauCeti.TypeTwistedDLieIndex.graphAut_comp_frobenius: the fork-exchange graph automorphism of the ambient group of a²Dₙindex, its pinned equationγ₂ (x_i(u)) = x_{σ i}(u), the relationγ₂ ^ 2 = 1, also in the form the twist order of the index states it, and its commutation with the Frobenius.TauCeti.TypeTwistedDLieIndex.steinberg, withTauCeti.TypeTwistedDLieIndex.steinberg_def,TauCeti.TypeTwistedDLieIndex.steinberg_eq_frobenius_comp_graphAutandTauCeti.TypeTwistedDLieIndex.steinberg_simpleRootSubgroup: the Steinberg endomorphismγ₂ ∘ Frob_qof²Dₙ(q), its two factorizations, and its pinned equationF (x_i(u)) = x_{σ i}(u ^ q).TauCeti.TypeTwistedDLieIndex.FixedPointsandTauCeti.TypeTwistedDLieIndex.Group: the fixed subgroup of that Steinberg map, and the candidate group of²Dₙ(q).TauCeti.TypeDDiagramLieIndex.primeFrobenius, withTauCeti.TypeDDiagramLieIndex.primeFrobenius_simpleRootSubgroupandTauCeti.TypeDDiagramLieIndex.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 #
- C. Chevalley, The Algebraic Theory of Spinors, Chapter II, for the spin representation the carrier is built from.
- R. W. Carter, Simple Groups of Lie Type, §§4.4, 12.2 and 14.
- R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §§1.15 and 1.17.
- R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV, for the numbering of the
Dₙdiagram that the index's rank and diagram permutation are read in.
The ambient group and its simple root subgroups #
The ambient group this file attaches to a validated index on a type-D diagram: the points
of the explicit full-weight type-Dₙ spin Chevalley carrier, at the rank the index names, over the
algebraic closure of its prime field.
It is infinite, and it is the same group for every index on the diagram of a given rank and field
order. The untwisted and graph-twisted families run their recipes inside it; the triality-twisted
family's own branch is instead built on the tripled carrier, in
TauCeti/GroupTheory/SpecificGroups/CFSG/TrialityD4.lean. No finiteness, reductivity, pinning or
maximality statement is attached to it, and it is not identified with the points of the pinned
simply connected Dₙ group scheme, as the module docstring describes.
Equations
- d.AmbientGroup = ↥(TauCeti.TypeDSpinCarrier.points (↑d).rank ⋯ (↑d).Closure)
Instances For
The positive simple-root subgroup at the Bourbaki-numbered node i of the Dₙ diagram. It is
the carrier's numbered raising subgroup at the same node, the index type Fin d.1.rank being the
upstream Bourbaki index type of the index's own Dynkin type and the carrier's own rank.
Equations
- d.simpleRootSubgroup i = TauCeti.TypeDSpinCarrier.rootSubgroupPoints (↑d).rank ⋯ (Sum.inl i) (↑d).Closure
Instances For
The simple-root subgroup is the carrier's numbered raising subgroup at the corresponding node.
This is the equation through which the upstream root-subgroup API reaches simpleRootSubgroup,
whose definition itself stays sealed.
It is deliberately not a simp lemma: frobenius_simpleRootSubgroup is the normal form the pinned
equations of this file are stated against, and unfolding to
TauCeti.TypeDSpinCarrier.rootSubgroupPoints would keep it from firing.
The simple-root subgroups sit at the simple roots of the type-Dₙ root datum. The
character by which the carrier's split torus rescales the parameter of simpleRootSubgroup i is
the i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at the Dynkin type the
index names, in the same Bourbaki numbering. This is the sense in which the spin 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.
The character itself is TauCeti.TypeDStd.rootGeneratorWeight, which
TauCeti.TypeDSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints exhibits as the one conjugation
by the carrier's split torus rescales the parameter by.
The Frobenius endomorphism #
The q-power Frobenius endomorphism of the ambient group of an index on a type-D
diagram, for q the field order the index records. On the untwisted family Dₙ(q) it is the
Steinberg map itself, by TauCeti.TypeDLieIndex.steinberg_def. On the two twisted families it is
not: there the Steinberg map is γ ∘ Frob_q for a nontrivial diagram permutation, and this is the
factor that composite composes with, as TauCeti.TypeTwistedDLieIndex.steinberg_def records on the
graph-twisted family.
Equations
- d.frobenius = TauCeti.TypeDSpinCarrier.frobenius (↑d).rank ⋯ (↑d).characteristic (↑d).fieldExponent (↑d).Closure
Instances For
The Frobenius of an index on a type-D diagram is the carrier's Frobenius at the exponent the
index records. This is its unfolding lemma; the definition itself stays sealed.
It is deliberately not a simp lemma: frobenius_simpleRootSubgroup and coe_frobenius_apply are
the normal forms the pinned equations of this file are stated against, and unfolding to
TauCeti.TypeDSpinCarrier.frobenius would keep them from firing.
The Frobenius acts on the ambient group by raising every matrix entry to the q-th power.
The Frobenius fixes the Bourbaki 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 diagram permutation of a
twisted family enters through the graph factor of its Steinberg map, and not through this one.
The prime-field Frobenius of the spin carrier of an index on a type-D diagram, 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.TypeDSpinCarrier.frobenius (↑d).rank ⋯ (↑d).characteristic 1 (↑d).Closure
Instances For
The prime-field Frobenius is the spin 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 Bourbaki 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.
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 Frobenius fixed points are the points
of the spin carrier whose entries lie in 𝔽_q.
As for TauCeti.ValidLieTypeIndex.mem_fixedSubgroup_geckFrobenius_iff, this is not a simp lemma:
TauCeti.fixedSubgroup is MonoidHom.eqLocus against the identity, so simp rewrites its
left-hand side to d.frobenius g = g through MonoidHom.mem_eqLocus, and the simpNF linter
rejects the annotation.
The Steinberg endomorphism of the untwisted family #
The Steinberg endomorphism of a validated untwisted type-D index, formed on the spin
carrier: 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;
diagramPerm_toGraphTwistedIndex is the check that its diagram permutation is trivial.
It is the Steinberg map of Dₙ(q) on the pinned simply connected group only along an
identification of the spin carrier with that group, as the module docstring describes.
Equations
Instances For
The Steinberg map of an untwisted type-D index is the Frobenius that all three families on a
type-D diagram share. This is its unfolding lemma; the definition itself stays sealed, and it is
through this equation that the ambient-group API of TauCeti.TypeDDiagramLieIndex reaches the
Steinberg map.
The Steinberg map fixes the Bourbaki 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 pinned equation of
an untwisted family.
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 group H_d that the classification recipe is run
on below is the group of points of the spin carrier whose entries lie in 𝔽_q.
The candidate group of the untwisted family #
The finite-simple-group candidate attached to Dₙ(q), formed on the spin carrier: the
derived subgroup of the fixed points of the Steinberg map above, modulo the centre of that derived
subgroup. It becomes the candidate on the pinned simply connected group along an identification of
the spin carrier with that group, as the module docstring describes. No finiteness or simplicity
assertion is part of this definition.
Equations
Instances For
The graph automorphism factor of the Steinberg map of ²Dₙ(q) #
The graph automorphism of the ambient group of a validated ²Dₙ index: conjugation by the
signed permutation matrix of the spin coordinates that realizes the fork exchange of the Dₙ
diagram on the spin carrier. It sends the Bourbaki-numbered simple-root subgroup at i to the one
at σ i, for σ the diagram permutation the index carries, without changing its parameter, and
it is the left-hand factor γ₂ of the Steinberg map γ₂ ∘ Frob_q of the family.
Equations
- d.graphAut = TauCeti.TypeDSpinCarrier.graphAutPoints (↑d).rank ⋯ (↑d).Closure
Instances For
The graph automorphism of a ²Dₙ index is the spin carrier's graph automorphism on points at
the index's rank, over its closure. This is its unfolding lemma; the definition itself stays
sealed.
The graph automorphism has the pinned action on every simple-root subgroup: it sends
x_i(u) to x_{σ i}(u), where σ is the diagram permutation the index carries, the fork
exchange. 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 is an involution.
The graph automorphism squares to the identity: γ₂ ^ 2 = 1.
The twist order of the index annihilates its graph automorphism. This is the order relation
on the graph factor of the Steinberg map of a graph-twisted family, and it matches
TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder on the diagram permutation that γ₂
realizes.
The graph automorphism commutes with the Frobenius, as an identity of endomorphisms:
γ₂ ∘ Frob_q = Frob_q ∘ γ₂. The graph automorphism is natural in the value ring, and the Frobenius
is the map on points induced by a ring endomorphism of the closure.
The Steinberg endomorphism of the graph-twisted family #
The Steinberg endomorphism of ²Dₙ(q) on the spin carrier: the fork-exchange graph
automorphism composed with the q-power Frobenius, γ₂ ∘ Frob_q, for q the field order the
index records. The two factors commute, so the order of composition is immaterial, by
steinberg_eq_frobenius_comp_graphAut.
It is the Steinberg map of ²Dₙ(q) on the pinned simply connected group only along an
identification of the spin carrier with that group, as the module docstring describes.
Equations
Instances For
The Steinberg map of ²Dₙ(q) is its graph automorphism composed with the shared Frobenius
of the type-D diagram. This is its unfolding lemma; the definition itself stays sealed, and it
is through this equation that the two factors reach the Steinberg map.
The Steinberg map may equally be read with its Frobenius factor last, the two factors commuting.
The Steinberg map has the pinned action on every simple-root subgroup. It sends x_i(u)
to x_{σ i}(u ^ q), where σ is the diagram permutation the index carries, the fork exchange, and
q is its recorded field order.
The candidate group of the graph-twisted family #
The fixed subgroup of the Steinberg endomorphism of ²Dₙ(q). Its points are not the points
with entries in 𝔽_q, which are the fixed points of the Frobenius factor alone.
Equations
Instances For
The finite-simple-group candidate attached to ²Dₙ(q), formed on the spin carrier: the
derived subgroup of the fixed points of its Steinberg map, modulo the centre of that derived
subgroup. It becomes the candidate on the pinned simply connected group along an identification of
the spin carrier with that group, as the module docstring describes. No finiteness or simplicity
assertion is part of this definition.