Special node permutations of a Dynkin type

A graph automorphism of a Dynkin diagram is a permutation of its Bourbaki-numbered nodes preserving the standard Cartan matrix; those are pinned in TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean, and each of them lifts to an automorphism of the pinned group scheme of the type. This file is about the other kind of node permutation, the one that transposes the Cartan matrix while exchanging the long and the short simple roots:

A (σ i) (σ j) = A j i,      σ i long ↔ i short.

Such a σ is a symmetry of the dual diagram rather than of the diagram, so no automorphism of the pinned group realises it. It is realised instead by a special isogeny τ, whose defining action on the numbered simple root subgroups is τ (x_i(a)) = x_{σ i}(a ^ q i) with q i = 1 on a long node and q i = p on a short one, and which therefore satisfies τ ^ 2 = Frob_p. The predicate defined here, TauCeti.DynkinType.IsSpecialNodePerm, is the root-level datum such an isogeny carries.

The point of the file is that this datum is completely rigid, and the theorems saying so make the node permutation, and hence the root-subgroup indexing datum for a future special isogeny, canonical:

• it exists exactly for B₂, F₄ and G₂ among the valid types (TauCeti.DynkinType.exists_isSpecialNodePerm_iff);
• when it exists it is unique (TauCeti.DynkinType.IsSpecialNodePerm.unique), hence an involution (TauCeti.DynkinType.IsSpecialNodePerm.sq_eq_one);
• the two squared root lengths it exchanges multiply to 2 for B₂ and F₄ and to 3 for G₂ (TauCeti.DynkinType.exists_prime_rootLength_mul_rootLength), which is the prime whose Frobenius the isogeny squares to.

The exclusions in the first item are the small-rank accidents. A length-exchanging permutation restricts to a bijection between the long and the short nodes, so a type admitting one has as many of each; a valid simply-laced type has no short node and a node to spare, Bₙ has n - 1 long nodes against one short one and Cₙ the reverse, so only B₂, F₄ and G₂ survive. Uniqueness genuinely needs the Cartan condition and not only the length condition: four permutations of the F₄ nodes exchange its two long nodes with its two short ones, and only the diagram reversal transposes its Cartan matrix. It is proved by composing two candidates into a permutation that preserves the Cartan matrix, and observing that each of the three types has no such permutation but the identity.

Nothing here constructs an isogeny, or any group or Lie algebra. This is the combinatorial input to that construction, stated against the pinned Bourbaki numbering of TauCeti.DynkinType.cartanMatrix, in which Bourbaki node i sits at Fin index i - 1.

Main definitions

• TauCeti.DynkinType.IsSpecialNodePerm: a permutation of the nodes of a Dynkin type exchanging long and short simple roots and transposing the standard Cartan matrix.

Main results

• TauCeti.DynkinType.isSpecialNodePerm_B2, TauCeti.DynkinType.isSpecialNodePerm_F4 and TauCeti.DynkinType.isSpecialNodePerm_G2: the three special node permutations, taken from the pinned length permutations of TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean.
• TauCeti.DynkinType.exists_isSpecialNodePerm_iff: a valid Dynkin type admits a special node permutation exactly when it is B₂, F₄ or G₂.
• TauCeti.DynkinType.IsSpecialNodePerm.unique and TauCeti.DynkinType.IsSpecialNodePerm.sq_eq_one: it is then unique, and an involution.
• TauCeti.DynkinType.exists_prime_rootLength_mul_rootLength: the two squared lengths it exchanges multiply to a prime, which is 2 or 3.
• TauCeti.DynkinType.IsSpecialNodePerm.submatrix_cartanMatrix_ne: it is never a graph automorphism.

References

This is the root-level combinatorics underlying the "special isogenies in characteristics two and three" item of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. See R. Steinberg, Lectures on Chevalley Groups, §11, for the isogeny itself, and R. W. Carter, Simple Groups of Lie Type, §12.3-12.4, for the Suzuki and Ree groups it produces.

structure TauCeti.DynkinType.IsSpecialNodePerm (t : DynkinType) (σ : Equiv.Perm (Fin t.rank)) : Prop

A permutation σ of the Bourbaki-numbered nodes of a Dynkin type is a special node permutation when it exchanges the long and the short simple roots and carries the standard Cartan matrix to the transposed matrix.

This is the root-level datum of a special isogeny: the isogeny sends the root subgroup of the simple root αᵢ to the root subgroup of α_{σ i}, raising its parameter to the power 1 or p according as αᵢ is long or short. Transposing rather than preserving the Cartan matrix is what separates it from a graph automorphism (TauCeti.DynkinType.IsSpecialNodePerm.submatrix_cartanMatrix_ne); accordingly no automorphism of the pinned group realises it.

• isLongSimpleRoot_apply (i : Fin t.rank) : t.IsLongSimpleRoot (σ i) ↔ ¬t.IsLongSimpleRoot i

  The permutation exchanges long and short simple roots.

• cartanMatrix_apply (i j : Fin t.rank) : t.cartanMatrix (σ i) (σ j) = t.cartanMatrix j i

  The permutation carries the standard Cartan matrix to the transposed matrix.

theorem TauCeti.DynkinType.IsSpecialNodePerm.inv {t : DynkinType} {σ : Equiv.Perm (Fin t.rank)} (h : t.IsSpecialNodePerm σ) : t.IsSpecialNodePerm σ⁻¹

The inverse of a special node permutation is one: both defining conditions are symmetric in σ and σ⁻¹ once the roles of the two indices are exchanged.

theorem TauCeti.DynkinType.IsSpecialNodePerm.cartanMatrix_apply_inv_mul {t : DynkinType} {σ τ : Equiv.Perm (Fin t.rank)} (hσ : t.IsSpecialNodePerm σ) (hτ : t.IsSpecialNodePerm τ) (i j : Fin t.rank) : t.cartanMatrix ((τ⁻¹ * σ) i) ((τ⁻¹ * σ) j) = t.cartanMatrix i j

Composing a special node permutation with the inverse of another one gives a permutation that preserves the Cartan matrix: the two transpositions cancel. This is how uniqueness is proved.

theorem TauCeti.DynkinType.IsSpecialNodePerm.not_isSimplyLaced {t : DynkinType} {σ : Equiv.Perm (Fin t.rank)} (ht : t.Valid) (h : t.IsSpecialNodePerm σ) : ¬t.IsSimplyLaced

A type carrying a special node permutation has a short simple root, so it is not simply laced.

The three types that admit one

theorem TauCeti.DynkinType.isSpecialNodePerm_B2 : (B 2).IsSpecialNodePerm lengthPermRankTwo

Exchanging the two nodes of B₂ is a special node permutation: the first node is long and the second short, and the swap transposes the B₂ Cartan matrix.

theorem TauCeti.DynkinType.isSpecialNodePerm_G2 : G2.IsSpecialNodePerm lengthPermRankTwo

Exchanging the two nodes of G₂ is a special node permutation: the second node is long and the first short, and the swap transposes the G₂ Cartan matrix.

theorem TauCeti.DynkinType.isSpecialNodePerm_F4 : F4.IsSpecialNodePerm lengthPermF4

Reversing the F₄ diagram is a special node permutation: it exchanges the two long nodes 0 and 1 with the two short nodes 2 and 3, and transposes the F₄ Cartan matrix.

The types that do not

A length-exchanging permutation is a bijection between the long and the short nodes, so it forces the two to be equinumerous. A valid simply-laced type is ruled out by TauCeti.DynkinType.IsSpecialNodePerm.not_isSimplyLaced, and each proof below exhibits two nodes of one kind whose images would have to be the single node of the other kind.

theorem TauCeti.DynkinType.not_isSpecialNodePerm_B {n : ℕ} (hn : 3 ≤ n) (σ : Equiv.Perm (Fin (B n).rank)) : ¬(B n).IsSpecialNodePerm σ

Bₙ has no special node permutation once 3 ≤ n: its nodes 0 and 1 are then both long, while its only short node is the last one, so the two would have the same image.

theorem TauCeti.DynkinType.not_isSpecialNodePerm_C {n : ℕ} (hn : 3 ≤ n) (σ : Equiv.Perm (Fin (C n).rank)) : ¬(C n).IsSpecialNodePerm σ

Cₙ has no special node permutation once 3 ≤ n: its nodes 0 and 1 are then both short, while its only long node is the last one, so the two would have the same image.

theorem TauCeti.DynkinType.exists_isSpecialNodePerm_iff {t : DynkinType} (ht : t.Valid) : (∃ (σ : Equiv.Perm (Fin t.rank)), t.IsSpecialNodePerm σ) ↔ t = B 2 ∨ t = F4 ∨ t = G2

A valid Dynkin type admits a special node permutation exactly when it is B₂, F₄ or G₂.

These are the three types whose finite groups of Lie type include a Suzuki--Ree family: the special isogeny of B₂ in characteristic two gives ²B₂, that of G₂ in characteristic three gives ²G₂, and that of F₄ in characteristic two gives ²F₄ and the Tits group.

Rigidity

Each of B₂, F₄ and G₂ has a trivial diagram automorphism group, in the strong sense that the identity is the only permutation of its nodes preserving its standard Cartan matrix. Since the composite of one special node permutation with the inverse of another preserves the Cartan matrix, uniqueness follows.

theorem TauCeti.DynkinType.eq_one_of_cartanMatrix_B2 {ρ : Equiv.Perm (Fin 2)} (h : ∀ (i j : Fin 2), (B 2).cartanMatrix (ρ i) (ρ j) = (B 2).cartanMatrix i j) : ρ = 1

The identity is the only permutation of the two B₂ nodes preserving its Cartan matrix, the B₂ matrix being asymmetric.

theorem TauCeti.DynkinType.eq_one_of_cartanMatrix_G2 {ρ : Equiv.Perm (Fin 2)} (h : ∀ (i j : Fin 2), G2.cartanMatrix (ρ i) (ρ j) = G2.cartanMatrix i j) : ρ = 1

The identity is the only permutation of the two G₂ nodes preserving its Cartan matrix, the G₂ matrix being asymmetric.

theorem TauCeti.DynkinType.eq_one_of_cartanMatrix_F4 {ρ : Equiv.Perm (Fin 4)} (h : ∀ (i j : Fin 4), F4.cartanMatrix (ρ i) (ρ j) = F4.cartanMatrix i j) : ρ = 1

The identity is the only permutation of the four F₄ nodes preserving its Cartan matrix.

The entry -2 occurs once, at the double bond (1, 2), so a Cartan-preserving permutation fixes both of those nodes; the two end nodes are then pinned by the entries -1 beside them.

theorem TauCeti.DynkinType.IsSpecialNodePerm.unique {t : DynkinType} (ht : t.Valid) {σ τ : Equiv.Perm (Fin t.rank)} (hσ : t.IsSpecialNodePerm σ) (hτ : t.IsSpecialNodePerm τ) : σ = τ

A valid Dynkin type has at most one special node permutation. Thus its numbered-node permutation, and hence its root-subgroup indexing datum, is canonical whenever it exists.

theorem TauCeti.DynkinType.IsSpecialNodePerm.sq_eq_one {t : DynkinType} (ht : t.Valid) {σ : Equiv.Perm (Fin t.rank)} (h : t.IsSpecialNodePerm σ) : σ ^ 2 = 1

A special node permutation of a valid type is an involution, because its inverse is one too and there is only one. This is the node-level shadow of τ ^ 2 = Frob_p, whose square acts trivially on the numbering and only raises the root-subgroup parameters to the power p.

theorem TauCeti.DynkinType.IsSpecialNodePerm.submatrix_cartanMatrix_ne {t : DynkinType} (ht : t.Valid) {σ : Equiv.Perm (Fin t.rank)} (h : t.IsSpecialNodePerm σ) : t.cartanMatrix.submatrix ⇑σ ⇑σ ≠ t.cartanMatrix

A special node permutation is never a graph automorphism: it transposes the Cartan matrix, and for the three types that carry one the transposed matrix is a different matrix.

The prime attached to a special node permutation

theorem TauCeti.DynkinType.exists_prime_rootLength_mul_rootLength {t : DynkinType} (ht : t.Valid) {σ : Equiv.Perm (Fin t.rank)} (h : t.IsSpecialNodePerm σ) : ∃ (p : ℕ), Nat.Prime p ∧ (p = 2 ∨ p = 3) ∧ ∀ (i : Fin t.rank), t.rootLength i * t.rootLength (σ i) = ↑p

The two squared root lengths that a special node permutation exchanges multiply to a prime, namely 2 for B₂ and F₄ and 3 for G₂.

That prime is the characteristic in which the corresponding special isogeny exists: the isogeny raises a root-subgroup parameter to the power 1 on a long node and to the power p on a short one, so either composite of the two exponents is p, and its square is the p-power Frobenius.