Diagram automorphisms of the pinned simply connected root datum #
A symmetry of the Bourbaki-numbered Dynkin diagram of a valid TauCeti.DynkinType is a permutation
σ of Fin t.rank preserving the Cartan matrix. This file turns each such permutation into an
automorphism of the pinned simply connected root datum
TauCeti.DynkinType.simplyConnectedRootDatum, multiplicatively in σ.
Both pinned lattices are coordinate spaces, so both maps of the automorphism are permutations of
coordinates, but the two permutations are transpose to one another and must be told apart. The
character lattice carries the fundamental weights as its standard basis, and its map is
precomposition with σ⁻¹, which permutes the fundamental weights by σ. Mathlib's coweight slot
holds the transpose of that map, so the cocharacter lattice, which carries the simple coroots as
its standard basis, receives precomposition with σ, which permutes the simple coroots by σ⁻¹;
the coroots themselves are nevertheless permuted by σ, by
TauCeti.DynkinType.coroot_diagramRootPerm.
What is not visible from the coordinates is the accompanying permutation of the root enumeration
Fin t.numRoots, since the non-simple roots are stored as explicit coordinate tables per family.
That permutation is obtained here from Mathlib's RootPairing.Base.equivOfCartanMatrixEq applied
to the rational root system TauCeti.DynkinType.rationalRootSystem, which is where the roots span
and a base therefore determines an isomorphism; the resulting equations transport back to ℤ
because the base change is the coordinatewise cast.
The multiplicativity is the point rather than a bonus. A Steinberg endomorphism of a graph-twisted
finite group of Lie type composes the field Frobenius with the graph automorphism attached to a
diagram symmetry of order two or three, and the relation γ ^ 2 = 1 or γ ^ 3 = 1 it needs is the
image of the corresponding relation on σ under the homomorphism
TauCeti.DynkinType.diagramAutHom built below.
The group of node permutations that the construction consumes is
TauCeti.DynkinType.diagramSymmetry, pinned in
TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean.
Main definitions #
TauCeti.DynkinType.diagramRootPerm: the induced permutation of the pinned root enumeration.TauCeti.DynkinType.rationalDiagramAutandTauCeti.DynkinType.diagramAut: the induced automorphisms of the rational root system and of the pinned integral datum.TauCeti.DynkinType.diagramAutHom: the homomorphism out ofdiagramSymmetrysending each diagram symmetry to the automorphismdiagramAutit induces on the pinned integral datum.
Main results #
TauCeti.DynkinType.diagramRootPerm_simpleIndex: the induced permutation extendsσalong the Bourbaki numbering of the simple roots.TauCeti.DynkinType.root_diagramRootPermandTauCeti.DynkinType.coroot_diagramRootPerm: every root and coroot has its coordinates permuted byσ.TauCeti.DynkinType.eq_diagramAut: an automorphism of the pinned datum whose weight map is the coordinate permutation is the diagram automorphism, so the construction is the unique such automorphism.TauCeti.DynkinType.diagramAut_eq_one_iff: the induced automorphism is trivial exactly when the node permutation is trivial.TauCeti.DynkinType.diagramAut_pow_eq_one: a node permutation of finite order induces an automorphism of the same finite order relation.
References #
The diagram automorphism attached to a symmetry of a pinned root datum is Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md: "Pinnings ... This is what makes 'the' graph
automorphism well defined, so it is data, not a property", and it is the "isomorphism of root data"
that the isomorphism theorem for pinned groups there lifts to a group scheme. Its consumer is
milestone L1 of TauCetiRoadmap/CFSGStatement/README.md, the graph-twisted Steinberg maps. See
R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15, and
N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4.
The induced permutation of the pinned root enumeration #
The automorphism of the rational root system attached to a symmetry of the Bourbaki-numbered
Cartan matrix. Over ℚ the roots span, so a self-map of the base which preserves the Cartan matrix
extends to the whole root system, by Mathlib's rigidity theorem.
Equations
- TauCeti.DynkinType.rationalDiagramAut ht hσ = (t.rationalBase ht).equivOfCartanMatrixEq (t.rationalBase ht) ((t.simpleSupportEquiv ht).permCongr σ) ⋯
Instances For
The permutation of the pinned root enumeration realized by a symmetry of the Cartan matrix.
Equations
Instances For
The rational diagram automorphism acts on the root enumeration by
TauCeti.DynkinType.diagramRootPerm.
The induced permutation of the root enumeration extends the node permutation along the Bourbaki numbering of the simple roots.
The coordinates are permuted by the node permutation #
The weight map of the rational automorphism is precomposition with σ⁻¹, so it permutes the
fundamental weights, the standard basis of the character lattice, by σ.
Every root of the pinned datum has its fundamental-weight coordinates permuted by a symmetry of the Cartan matrix.
The inverse of the coweight equivalence of the rational automorphism is precomposition with
σ⁻¹, so it permutes the simple coroots, the standard basis of the cocharacter lattice, by σ.
It is this inverse, and not the coweight map itself, which carries a coroot to the coroot of the
permuted index.
The coweight map of the rational automorphism is precomposition with σ, the transpose of the
weight map, so it permutes the simple coroots by σ⁻¹.
Every coroot of the pinned datum has its simple-coroot coordinates permuted by a symmetry of the Cartan matrix.
The automorphism of the pinned integral datum #
The diagram automorphism of the pinned simply connected root datum attached to a symmetry of
the Bourbaki-numbered Cartan matrix. Both lattice maps are precompositions, the character one with
σ⁻¹ and the cocharacter one, its transpose, with σ, and the root enumeration is permuted by
TauCeti.DynkinType.diagramRootPerm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diagram automorphism acts on the root enumeration by
TauCeti.DynkinType.diagramRootPerm.
The weight map of the diagram automorphism is precomposition with σ⁻¹, so it permutes the
fundamental weights, the standard basis of the character lattice, by σ.
The coweight map of the diagram automorphism is precomposition with σ, the transpose of the
weight map, so it permutes the simple coroots by σ⁻¹.
An automorphism of the pinned datum is the diagram automorphism as soon as its weight map is the coordinate permutation, since an automorphism of a root pairing is determined by that map.
Multiplicativity #
The diagram automorphism attached to the identity node permutation is the identity.
The diagram automorphism is trivial exactly when its node permutation is trivial. In particular, the construction is faithful on diagram symmetries.
The construction is multiplicative in the node permutation.
The induced permutation of the root enumeration is the index component of the diagram
automorphism, so it inherits multiplicativity from TauCeti.DynkinType.diagramAut_mul.
The identity node permutation induces the identity permutation of the root enumeration.
The diagram automorphisms of the pinned datum, as a homomorphism out of the symmetry group of the Bourbaki-numbered Cartan matrix. This is what converts a relation satisfied by a node permutation into the same relation for the automorphism it induces.
Equations
- TauCeti.DynkinType.diagramAutHom ht = { toFun := fun (g : ↥t.diagramSymmetry) => TauCeti.DynkinType.diagramAut ht ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The diagram automorphism attached to the inverse node permutation is the inverse automorphism.
A node permutation of finite order induces an automorphism satisfying the same relation.
This is the source of γ ^ 2 = 1 for the order-two diagram symmetries of Aₙ, Dₙ and E₆, and
of γ ^ 3 = 1 for the triality of D₄.