Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.SerreGraphAutomorphism

Serre graph automorphisms for the graph-twisted families #

For a graph-twisted finite group of Lie type, the graph part of its Steinberg endomorphism starts with the automorphism of the split semisimple Lie algebra which permutes the Chevalley generators according to the symmetry of the Dynkin diagram. This file constructs that automorphism on the explicit Serre presentation attached to every TauCeti.GraphTwistedIndex.

The construction joins two existing pieces of pinned data. The permutation TauCeti.GraphTwistedIndex.diagramPerm records the Bourbaki-numbered diagram symmetry selected by the CFSG index, and TauCeti.serreDiagramAut turns any Cartan-matrix symmetry into an automorphism of the corresponding Serre Lie algebra. The matrix invariance proof here is the audit boundary between them. No root datum, Lie algebra, or automorphism is selected by choice.

The resulting automorphism sends each of the three generator families without signs,

H_i ↦ H_{γ i},   E_i ↦ E_{γ i},   F_i ↦ F_{γ i},

and its iterate at twistOrder is the identity. Thus the order-two relations for ²Aₙ, ²Dₙ and ²E₆, and the order-three relation for ³D₄, are already present before the automorphism is descended through the Kostant form to the pinned group scheme. It also commutes with the Chevalley involution, as both automorphisms visibly do on the Serre generators.

Main declarations #

Roadmap and references #

This is a prerequisite for the Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. That construction descends diagram automorphisms from the Lie algebra through the Kostant integral form to the pinned group scheme. It is consumed by milestone L1 of TauCetiRoadmap/CFSGStatement/README.md, which forms graph-twisted Steinberg maps and requires γ² = 1 or γ³ = 1 together with the displayed simple-root-subgroup equation.

The conventions follow R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15, and the Bourbaki numbering pinned by the root-systems roadmap.

source
@[simp]
theorem TauCeti.GraphTwistedIndex.cartanMatrix_submatrix_diagramPerm (d : GraphTwistedIndex) :
(↑d).dynkinType.cartanMatrix.submatrix ⇑d.diagramPerm ⇑d.diagramPerm = (↑d).dynkinType.cartanMatrix

The diagram permutation selected by a graph-twisted index preserves the Cartan matrix of its underlying untwisted Dynkin diagram. This is the matrix form consumed by serreDiagramAut.

source
@[simp]
theorem TauCeti.GraphTwistedIndex.cartanMatrix_transpose_submatrix_diagramPerm (d : GraphTwistedIndex) :
(↑d).dynkinType.cartanMatrix.transpose.submatrix ⇑d.diagramPerm ⇑d.diagramPerm = (↑d).dynkinType.cartanMatrix.transpose

The diagram permutation also preserves the transposed Cartan matrix used by the Serre presentation of the pinned Lie algebra.

source
noncomputable def TauCeti.GraphTwistedIndex.serreGraphAut (d : GraphTwistedIndex) (R : Type u) [CommRing R] :
Matrix.ToLieAlgebra R (↑d).dynkinType.cartanMatrix.transpose ≃ₗ⁅R⁆ Matrix.ToLieAlgebra R (↑d).dynkinType.cartanMatrix.transpose

The graph automorphism of the Serre Lie algebra attached to a graph-twisted index.

It is induced by the pinned permutation of the Bourbaki-numbered nodes. On an untwisted family the permutation is the identity; on ²Aₙ, ²Dₙ, ²E₆, and ³D₄ it is respectively the chain reversal, fork exchange, E₆ involution, or triality.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GraphTwistedIndex.serreGraphAut_serreH (d : GraphTwistedIndex) (R : Type u) [CommRing R] (i : Fin (↑d).rank) :
    (d.serreGraphAut R) (serreH R (↑d).dynkinType.cartanMatrix.transpose i) = serreH R (↑d).dynkinType.cartanMatrix.transpose (d.diagramPerm i)

    The graph automorphism sends the i-th Cartan generator to the generator indexed by the diagram permutation.

    source
    @[simp]
    theorem TauCeti.GraphTwistedIndex.serreGraphAut_serreE (d : GraphTwistedIndex) (R : Type u) [CommRing R] (i : Fin (↑d).rank) :
    (d.serreGraphAut R) (serreE R (↑d).dynkinType.cartanMatrix.transpose i) = serreE R (↑d).dynkinType.cartanMatrix.transpose (d.diagramPerm i)

    The graph automorphism sends the i-th positive simple-root generator to the generator indexed by the diagram permutation, without changing its sign.

    source
    @[simp]
    theorem TauCeti.GraphTwistedIndex.serreGraphAut_serreF (d : GraphTwistedIndex) (R : Type u) [CommRing R] (i : Fin (↑d).rank) :
    (d.serreGraphAut R) (serreF R (↑d).dynkinType.cartanMatrix.transpose i) = serreF R (↑d).dynkinType.cartanMatrix.transpose (d.diagramPerm i)

    The graph automorphism sends the i-th negative simple-root generator to the generator indexed by the diagram permutation, without changing its sign.

    source
    @[simp]
    theorem TauCeti.GraphTwistedIndex.serreGraphAut_iterate_twistOrder (d : GraphTwistedIndex) (R : Type u) [CommRing R] :
    (⇑(d.serreGraphAut R))^[d.twistOrder] = id

    Applying the Serre graph automorphism twistOrder times is the identity. This is the uniform form of γ² = 1 on ²Aₙ, ²Dₙ, and ²E₆, and γ³ = 1 on ³D₄; on an untwisted family the twist order is one and the automorphism itself is the identity.

    source
    theorem TauCeti.GraphTwistedIndex.serreChevalleyInvolution_comm_serreGraphAut (d : GraphTwistedIndex) (R : Type u) [CommRing R] :
    (serreChevalleyInvolution R (↑d).dynkinType.cartanMatrix.transpose).trans (d.serreGraphAut R) = (d.serreGraphAut R).trans (serreChevalleyInvolution R (↑d).dynkinType.cartanMatrix.transpose)

    The Chevalley involution commutes with the graph automorphism selected by the index. The former exchanges positive and negative generators with a sign, while the latter applies the same node permutation to all three Serre-generator families.