Diagram symmetries of the pinned Geck lattice

A symmetry of a Dynkin diagram permutes both the roots of the pinned simply connected root datum and the Bourbaki-numbered simple roots. Geck's construction turns those two permutations into a coordinate permutation of its defining module. This file specializes that construction to the pinned data and proves the two facts needed by the Chevalley--Demazure group-scheme construction:

• the coordinate permutation preserves the integral Geck lattice; and
• it intertwines the represented simple raising and lowering generators.

The first point is not a consequence of an abstract root-datum isomorphism: the group-scheme construction acts on the concrete lattice TauCeti.DynkinType.geckCoordinateLattice. Here it is proved directly from the integer-coordinate characterization of that lattice. The second point is the representation-level pinning equation which can be passed to TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedNumberedSymmetryIso.

The weight equation in this file also records how the same coordinate permutation normalizes the represented split torus. It is the remaining input for extending the root-generated symmetry to the toral carrier.

Main definitions

• TauCeti.DynkinType.geckDiagramIndexEquiv: the coordinate permutation of the pinned Geck module.
• TauCeti.DynkinType.geckDiagramModuleEquiv: the resulting rational linear equivalence.
• TauCeti.DynkinType.geckDiagramFinPerm: the same coordinate permutation in the finite-ordinal indexing used by the group-scheme construction.
• TauCeti.DynkinType.diagramRootGeneratorPerm: the induced permutation of the simple raising and lowering indices.

Main results

• TauCeti.DynkinType.geckDiagramModuleEquiv_mem_geckCoordinateLattice_iff: the coordinate permutation preserves the pinned integral lattice in both directions.
• TauCeti.DynkinType.geckWeight_geckDiagramIndexEquiv: the weights are permuted contragrediently.
• TauCeti.DynkinType.geckDiagramModuleEquiv_geckCoordinateBasisFin and TauCeti.DynkinType.geckWeightFin_geckDiagramFinPerm: the finite-ordinal basis and weight equations consumed by the Kostant toral-closure symmetry construction.
• TauCeti.DynkinType.geckDiagramModuleEquiv_geckRepresentation_rootGenerator: the defining representation intertwines every numbered root generator with its permuted generator.
• TauCeti.DynkinType.geckDiagramIndexEquiv_pow_eq_one and TauCeti.DynkinType.geckDiagramFinPerm_pow_eq_one: the coordinate permutation satisfies every order relation the node permutation satisfies.

References

The coordinate construction is due to M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247. The passage from a pinned diagram symmetry to a graph automorphism follows R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15.

This is a prerequisite for the pinned isomorphism theorem in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L1, ordinary and graph-twisted Steinberg maps, of TauCetiRoadmap/CFSGStatement/README.md.

noncomputable def TauCeti.DynkinType.geckDiagramBaseEquiv {t : DynkinType} (ht : t.Valid) (sigma : Equiv.Perm (Fin t.rank)) : ↥(t.rationalBase ht).support ≃ ↥(t.rationalBase ht).support

The permutation of the support of the pinned rational base induced by a permutation of its Bourbaki-numbered nodes.

Equations

• TauCeti.DynkinType.geckDiagramBaseEquiv ht sigma = (t.simpleSupportEquiv ht).permCongr sigma

@[simp]

theorem TauCeti.DynkinType.geckDiagramBaseEquiv_apply_simpleSupportEquiv {t : DynkinType} (ht : t.Valid) (sigma : Equiv.Perm (Fin t.rank)) (i : Fin t.rank) : (geckDiagramBaseEquiv ht sigma) ((t.simpleSupportEquiv ht) i) = (t.simpleSupportEquiv ht) (sigma i)

The induced permutation on simple-root support acts through the node permutation.

noncomputable def TauCeti.DynkinType.geckDiagramIndexEquiv {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) : t.GeckIndex ht ≃ t.GeckIndex ht

The coordinate permutation of the pinned Geck module induced by a symmetry of its Bourbaki-numbered Dynkin diagram. It acts by the node permutation on the base-support coordinates and by TauCeti.DynkinType.diagramRootPerm on the root coordinates.

Equations

• TauCeti.DynkinType.geckDiagramIndexEquiv ht hsigma = TauCeti.geckIndexEquiv (TauCeti.DynkinType.rationalDiagramAut ht hsigma) (TauCeti.DynkinType.geckDiagramBaseEquiv ht sigma)

@[simp]

theorem TauCeti.DynkinType.geckDiagramIndexEquiv_apply_inl {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : ↥(t.rationalBase ht).support) : (geckDiagramIndexEquiv ht hsigma) (Sum.inl i) = Sum.inl ((geckDiagramBaseEquiv ht sigma) i)

The diagram symmetry acts on a base-support coordinate by the transported node permutation.

@[simp]

theorem TauCeti.DynkinType.geckDiagramIndexEquiv_apply_inr {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : Fin t.numRoots) : (geckDiagramIndexEquiv ht hsigma) (Sum.inr i) = Sum.inr ((diagramRootPerm ht hsigma) i)

The diagram symmetry acts on a root coordinate by the induced root permutation.

noncomputable def TauCeti.DynkinType.geckDiagramModuleEquiv {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) : (t.GeckIndex ht → ℚ) ≃ₗ[ℚ] t.GeckIndex ht → ℚ

The rational linear equivalence of the pinned Geck module induced by a diagram symmetry. It is the permutation of coordinate functions along TauCeti.DynkinType.geckDiagramIndexEquiv.

Equations

• TauCeti.DynkinType.geckDiagramModuleEquiv ht hsigma = TauCeti.geckModuleEquiv (TauCeti.DynkinType.rationalDiagramAut ht hsigma) (TauCeti.DynkinType.geckDiagramBaseEquiv ht sigma)

@[simp]

theorem TauCeti.DynkinType.geckDiagramModuleEquiv_apply {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (v : t.GeckIndex ht → ℚ) (i : t.GeckIndex ht) : (geckDiagramModuleEquiv ht hsigma) v i = v ((geckDiagramIndexEquiv ht hsigma).symm i)

The pinned Geck-module equivalence acts by precomposition with the inverse coordinate permutation.

@[simp]

theorem TauCeti.DynkinType.geckDiagramModuleEquiv_single {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : t.GeckIndex ht) (r : ℚ) : (geckDiagramModuleEquiv ht hsigma) (Pi.single i r) = Pi.single ((geckDiagramIndexEquiv ht hsigma) i) r

The pinned Geck-module equivalence sends a standard coordinate vector to the standard vector at the permuted coordinate.

theorem TauCeti.DynkinType.geckDiagramModuleEquiv_mem_geckCoordinateLattice_iff {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (v : t.GeckIndex ht → ℚ) : (geckDiagramModuleEquiv ht hsigma) v ∈ t.geckCoordinateLattice ht ↔ v ∈ t.geckCoordinateLattice ht

A diagram symmetry preserves the pinned integral Geck lattice. Membership is equivalent in both directions because the symmetry merely permutes the integer-valued coordinates. This is the lattice-stability hypothesis used by the Kostant group-scheme symmetry construction.

This is deliberately not a simp lemma: TauCeti.DynkinType.mem_geckCoordinateLattice_iff is itself simp, so both sides are unfolded into coordinate conditions before this statement could ever fire.

@[simp]

theorem TauCeti.DynkinType.geckWeight_geckDiagramIndexEquiv {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (x : t.GeckIndex ht) (i : Fin t.rank) : t.geckWeight ht ((geckDiagramIndexEquiv ht hsigma) x) (sigma i) = t.geckWeight ht x i

The coordinate permutation carries weights contragrediently. Equivalently, the weight of the permuted coordinate at node sigma i is the original weight at node i. This is the equation which makes the same permutation normalize the represented split torus.

The coordinate permutation in the finite-ordinal indexing

noncomputable def TauCeti.DynkinType.geckDiagramFinPerm {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) : Equiv.Perm (Fin (t.geckDim ht))

The coordinate permutation of a diagram symmetry, in the finite-ordinal indexing. The group-scheme construction indexes the Geck coordinate basis by Fin (t.geckDim ht) through Fintype.equivFin; this is TauCeti.DynkinType.geckDiagramIndexEquiv transported along that reindexing.

Equations

• TauCeti.DynkinType.geckDiagramFinPerm ht hsigma = (Fintype.equivFin (t.GeckIndex ht)).permCongr (TauCeti.DynkinType.geckDiagramIndexEquiv ht hsigma)

@[simp]

theorem TauCeti.DynkinType.equivFin_symm_geckDiagramFinPerm {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : Fin (t.geckDim ht)) : (Fintype.equivFin (t.GeckIndex ht)).symm ((geckDiagramFinPerm ht hsigma) i) = (geckDiagramIndexEquiv ht hsigma) ((Fintype.equivFin (t.GeckIndex ht)).symm i)

theorem TauCeti.DynkinType.geckDiagramModuleEquiv_geckCoordinateBasisFin {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : Fin (t.geckDim ht)) : (geckDiagramModuleEquiv ht hsigma) ↑((t.geckCoordinateBasisFin ht) i) = ↑((t.geckCoordinateBasisFin ht) ((geckDiagramFinPerm ht hsigma) i))

The pinned Geck-module symmetry permutes the finite-ordinal coordinate basis. This is the basis-permutation hypothesis of the Kostant toral-closure symmetry construction.

This is deliberately not a simp lemma: TauCeti.DynkinType.coe_geckCoordinateBasisFin and TauCeti.DynkinType.geckDiagramModuleEquiv_single are themselves simp, so both sides are already rewritten to the same standard coordinate vector and simp proves this statement outright.

@[simp]

theorem TauCeti.DynkinType.geckWeightFin_geckDiagramFinPerm {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : Fin (t.geckDim ht)) (k : Fin t.rank) : t.geckWeightFin ht ((geckDiagramFinPerm ht hsigma) i) (sigma k) = t.geckWeightFin ht i k

The finite-ordinal Geck weights are equivariant for the coordinate permutation and the node permutation. This is the weight hypothesis of the Kostant toral-closure symmetry construction, and it is what makes the same permutation intertwine the represented split torus with relabelling.

The order of the coordinate permutation

theorem TauCeti.DynkinType.geckDiagramIndexEquiv_pow_eq_one {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) {m : ℕ} (hm : sigma ^ m = 1) : geckDiagramIndexEquiv ht hsigma ^ m = 1

A node permutation of finite order induces a coordinate permutation of the pinned Geck module satisfying the same relation.

theorem TauCeti.DynkinType.geckDiagramFinPerm_pow_eq_one {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) {m : ℕ} (hm : sigma ^ m = 1) : geckDiagramFinPerm ht hsigma ^ m = 1

A node permutation of finite order induces a finite-ordinal coordinate permutation satisfying the same relation. This is the source of the order relation for the graph automorphism on the algebra-valued points of the pinned Geck carrier.

The permutation of the numbered generators

def TauCeti.DynkinType.diagramRootGeneratorPerm {t : DynkinType} (sigma : Equiv.Perm (Fin t.rank)) : Equiv.Perm (Fin t.rank ⊕ Fin t.rank)

The permutation of the simple raising and lowering indices induced by a diagram symmetry. The same node permutation acts on both halves.

Equations

• TauCeti.DynkinType.diagramRootGeneratorPerm sigma = Equiv.sumCongr sigma sigma

@[simp]

theorem TauCeti.DynkinType.diagramRootGeneratorPerm_apply_inl {t : DynkinType} {sigma : Equiv.Perm (Fin t.rank)} (i : Fin t.rank) : (diagramRootGeneratorPerm sigma) (Sum.inl i) = Sum.inl (sigma i)

The diagram permutation acts on a raising-generator index through sigma.

@[simp]

theorem TauCeti.DynkinType.diagramRootGeneratorPerm_apply_inr {t : DynkinType} {sigma : Equiv.Perm (Fin t.rank)} (i : Fin t.rank) : (diagramRootGeneratorPerm sigma) (Sum.inr i) = Sum.inr (sigma i)

The diagram permutation acts on a lowering-generator index through sigma.

theorem TauCeti.DynkinType.diagramRootGeneratorPerm_pow_eq_one {t : DynkinType} {sigma : Equiv.Perm (Fin t.rank)} {m : ℕ} (hm : sigma ^ m = 1) : diagramRootGeneratorPerm sigma ^ m = 1

A relation satisfied by a diagram symmetry is satisfied by the permutation it induces on the numbered generator indices. The induced permutation is the diagonal value of the bundled homomorphism Equiv.Perm.sumCongrHom, so it inherits that homomorphism's power law.

@[simp]

theorem TauCeti.DynkinType.geckDiagramModuleEquiv_geckRepresentation_rootGenerator {t : DynkinType} (ht : t.Valid) {sigma : Equiv.Perm (Fin t.rank)} (hsigma : sigma ∈ t.diagramSymmetry) (i : Fin t.rank ⊕ Fin t.rank) (v : t.GeckIndex ht → ℚ) : (geckDiagramModuleEquiv ht hsigma) (((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.mkAlgHom ℚ ↥(t.lieAlgebra ht)) ((TensorAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator i)))) v) = ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.mkAlgHom ℚ ↥(t.lieAlgebra ht)) ((TensorAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator ((diagramRootGeneratorPerm sigma) i))))) ((geckDiagramModuleEquiv ht hsigma) v)

The pinned Geck-module symmetry intertwines every represented simple root generator with the generator carrying the permuted number. This is exactly the additive pinning equation required to construct the corresponding automorphism of the root-generated Kostant group scheme.