Numbered diagram permutations for the finite groups of Lie type

This file pins the permutations of Bourbaki-numbered simple roots used by the graph automorphisms and exceptional isogenies in the construction of finite groups of Lie type. Bourbaki node i is represented by Fin index i - 1, as in TauCeti.DynkinType.cartanMatrix.

The ordinary graph automorphisms preserve the relevant Cartan matrix. The Suzuki--Ree permutations instead exchange long and short nodes; the corresponding special isogenies attach different field exponents to the two root lengths.

The conventions follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, plates I--IX, and the CFSGStatement roadmap's conventions for Steinberg endomorphisms.

Main definitions

• TauCeti.graphPermA: reversal of the Aₙ chain.
• TauCeti.graphPermD: exchange of the final two indices, giving the fork symmetry of Dₙ for 4 ≤ n.
• TauCeti.graphPermE6: the order-two symmetry of E₆.
• TauCeti.trialityPermD4: the order-three triality symmetry of D₄.
• TauCeti.lengthPermRankTwo: the length-exchanging permutation for B₂ and G₂.
• TauCeti.lengthPermF4: the length-exchanging permutation for F₄.
• TauCeti.DynkinType.diagramSymmetry: the group of node permutations preserving the Cartan matrix of a Dynkin type, of which the graph permutations above are members.

Main results

• TauCeti.orderOf_graphPermA, TauCeti.orderOf_graphPermD, TauCeti.orderOf_graphPermE6 and TauCeti.orderOf_trialityPermD4: the graph permutations have order exactly two (for graphPermA, on at least two nodes), except for triality, which has order three, with TauCeti.trialityPermD4_apply_apply_apply the pointwise form of that order relation.
• TauCeti.cartanMatrix_A_graphPermA, TauCeti.cartanMatrix_D_graphPermD, TauCeti.cartanMatrix_E6_graphPermE6 and TauCeti.cartanMatrix_D4_trialityPermD4: each graph permutation is an automorphism of the corresponding Cartan matrix.
• TauCeti.cartanMatrix_B2_lengthPermRankTwo, TauCeti.cartanMatrix_G2_lengthPermRankTwo and TauCeti.cartanMatrix_F4_lengthPermF4: each length permutation instead carries its Cartan matrix to the transposed matrix, and TauCeti.cartanMatrix_B2_submatrix_lengthPermRankTwo_ne and its two counterparts record that this is a different matrix, so a length permutation is not a diagram symmetry.
• TauCeti.lengthPermRankTwo_lengthPermRankTwo and TauCeti.lengthPermF4_lengthPermF4: the length permutations are involutions, and TauCeti.lengthPermRankTwo_apply, TauCeti.graphPermA_apply and TauCeti.lengthPermF4_apply evaluate them as reversals.

def TauCeti.graphPermA (n : ℕ) : Equiv.Perm (Fin n)

The Aₙ diagram automorphism, reversing its chain of Bourbaki-numbered nodes.

Equations

• TauCeti.graphPermA n = Fin.revPerm

def TauCeti.graphPermD (n : ℕ) (hn : 2 ≤ n) : Equiv.Perm (Fin n)

The permutation exchanging the final two indices of Fin n. For 4 ≤ n, this is the Dₙ diagram automorphism exchanging its two fork nodes and fixing the chain.

Equations

• TauCeti.graphPermD n hn = Equiv.swap ⟨n - 2, ⋯⟩ ⟨n - 1, ⋯⟩

def TauCeti.graphPermE6 : Equiv.Perm (Fin 6)

The E₆ diagram automorphism, exchanging Bourbaki nodes 1 ↔ 6 and 3 ↔ 5.

Equations

• TauCeti.graphPermE6 = Equiv.swap 0 5 * Equiv.swap 2 4

def TauCeti.trialityPermD4 : Equiv.Perm (Fin 4)

Triality of D₄, cycling its three outer nodes (0 2 3) and fixing the central node 1.

Equations

• TauCeti.trialityPermD4 = Equiv.swap 0 3 * Equiv.swap 0 2

def TauCeti.lengthPermRankTwo : Equiv.Perm (Fin 2)

The length-exchanging permutation of the two nodes of B₂ and G₂.

Equations

• TauCeti.lengthPermRankTwo = Equiv.swap 0 1

def TauCeti.lengthPermF4 : Equiv.Perm (Fin 4)

The length-exchanging permutation of F₄, reversing its four-node diagram.

Equations

• TauCeti.lengthPermF4 = TauCeti.graphPermA 4

theorem TauCeti.graphPermA_ne_one {n : ℕ} (hn : 2 ≤ n) : graphPermA n ≠ 1

Reversal of a chain of at least two nodes moves the first node, so it is not the identity. The bound is necessary: graphPermA 0 and graphPermA 1 are the identity.

@[simp]

theorem TauCeti.graphPermA_sq (n : ℕ) : graphPermA n ^ 2 = 1

Reversing the Aₙ chain twice is the identity.

@[simp]

theorem TauCeti.orderOf_graphPermA {n : ℕ} (hn : 2 ≤ n) : orderOf (graphPermA n) = 2

Reversal of a chain of at least two nodes has order exactly two.

@[simp]

theorem TauCeti.graphPermD_apply_left (n : ℕ) (hn : 2 ≤ n) : (graphPermD n hn) ⟨n - 2, ⋯⟩ = ⟨n - 1, ⋯⟩

The final-index swap sends index n - 2 to index n - 1; for 4 ≤ n, these are the two Dₙ fork nodes.

@[simp]

theorem TauCeti.graphPermD_apply_right (n : ℕ) (hn : 2 ≤ n) : (graphPermD n hn) ⟨n - 1, ⋯⟩ = ⟨n - 2, ⋯⟩

The final-index swap sends index n - 1 to index n - 2; for 4 ≤ n, these are the two Dₙ fork nodes.

@[simp]

theorem TauCeti.graphPermD_apply_of_ne_of_ne (n : ℕ) (hn : 2 ≤ n) (i : Fin n) (hi : ↑i ≠ n - 2) (hi' : ↑i ≠ n - 1) : (graphPermD n hn) i = i

The final-index swap fixes every index except n - 2 and n - 1; for 4 ≤ n, these are the two Dₙ fork nodes.

@[simp]

theorem TauCeti.graphPermD_symm (n : ℕ) (hn : 2 ≤ n) : Equiv.symm (graphPermD n hn) = graphPermD n hn

The final-index swap is its own inverse.

@[simp]

theorem TauCeti.graphPermD_sq (n : ℕ) (hn : 2 ≤ n) : graphPermD n hn ^ 2 = 1

Swapping the final two indices twice is the identity.

@[simp]

theorem TauCeti.graphPermD_apply_apply (n : ℕ) (hn : 2 ≤ n) (i : Fin n) : (graphPermD n hn) ((graphPermD n hn) i) = i

Applying the final-index swap twice returns an index to itself.

theorem TauCeti.graphPermD_ne_one (n : ℕ) (hn : 2 ≤ n) : graphPermD n hn ≠ 1

The two swapped indices are distinct, so the swap is not the identity.

@[simp]

theorem TauCeti.orderOf_graphPermD (n : ℕ) (hn : 2 ≤ n) : orderOf (graphPermD n hn) = 2

Exchanging the final two indices has order exactly two.

@[simp]

theorem TauCeti.graphPermE6_apply_zero : graphPermE6 0 = 5

The E₆ graph permutation sends node 0 to node 5.

@[simp]

theorem TauCeti.graphPermE6_apply_one : graphPermE6 1 = 1

The E₆ graph permutation fixes node 1.

@[simp]

theorem TauCeti.graphPermE6_apply_two : graphPermE6 2 = 4

The E₆ graph permutation sends node 2 to node 4.

@[simp]

theorem TauCeti.graphPermE6_apply_three : graphPermE6 3 = 3

The E₆ graph permutation fixes node 3.

@[simp]

theorem TauCeti.graphPermE6_apply_four : graphPermE6 4 = 2

The E₆ graph permutation sends node 4 to node 2.

@[simp]

theorem TauCeti.graphPermE6_apply_five : graphPermE6 5 = 0

The E₆ graph permutation sends node 5 to node 0.

@[simp]

theorem TauCeti.graphPermE6_sq : graphPermE6 ^ 2 = 1

Applying the E₆ graph permutation twice is the identity.

@[simp]

theorem TauCeti.graphPermE6_symm : Equiv.symm graphPermE6 = graphPermE6

The E₆ graph permutation is its own inverse.

@[simp]

theorem TauCeti.orderOf_graphPermE6 : orderOf graphPermE6 = 2

The E₆ graph permutation has order exactly two.

@[simp]

theorem TauCeti.trialityPermD4_apply_zero : trialityPermD4 0 = 2

Triality sends outer node 0 to outer node 2.

@[simp]

theorem TauCeti.trialityPermD4_apply_one : trialityPermD4 1 = 1

Triality fixes the central node 1.

@[simp]

theorem TauCeti.trialityPermD4_apply_two : trialityPermD4 2 = 3

Triality sends outer node 2 to outer node 3.

@[simp]

theorem TauCeti.trialityPermD4_apply_three : trialityPermD4 3 = 0

Triality sends outer node 3 to outer node 0.

@[simp]

theorem TauCeti.trialityPermD4_pow_three : trialityPermD4 ^ 3 = 1

Applying triality three times is the identity.

@[simp]

theorem TauCeti.trialityPermD4_apply_apply_apply (i : Fin 4) : trialityPermD4 (trialityPermD4 (trialityPermD4 i)) = i

Applying triality three times fixes every node of the D₄ diagram; the pointwise form of TauCeti.trialityPermD4_pow_three.

@[simp]

theorem TauCeti.orderOf_trialityPermD4 : orderOf trialityPermD4 = 3

Triality has order exactly three.

@[simp]

theorem TauCeti.lengthPermRankTwo_apply_zero : lengthPermRankTwo 0 = 1

The rank-two length permutation sends node 0 to node 1.

@[simp]

theorem TauCeti.lengthPermRankTwo_apply_one : lengthPermRankTwo 1 = 0

The rank-two length permutation sends node 1 to node 0.

@[simp]

theorem TauCeti.lengthPermRankTwo_sq : lengthPermRankTwo ^ 2 = 1

Exchanging the two rank-two nodes twice is the identity.

@[simp]

theorem TauCeti.lengthPermRankTwo_lengthPermRankTwo (i : Fin 2) : lengthPermRankTwo (lengthPermRankTwo i) = i

Exchanging the two rank-two nodes is an involution.

theorem TauCeti.lengthPermRankTwo_ne_one : lengthPermRankTwo ≠ 1

The two rank-two nodes are distinct, so exchanging them is not the identity.

theorem TauCeti.lengthPermRankTwo_apply (i : Fin 2) : lengthPermRankTwo i = i.rev

On two nodes, exchanging them is reversal.

@[simp]

theorem TauCeti.orderOf_lengthPermRankTwo : orderOf lengthPermRankTwo = 2

Exchanging the two rank-two nodes has order exactly two.

theorem TauCeti.graphPermA_apply (n : ℕ) (i : Fin n) : (graphPermA n) i = i.rev

Reversal of a chain sends a node to its reverse.

theorem TauCeti.lengthPermF4_apply (i : Fin 4) : lengthPermF4 i = i.rev

Reversal of the F₄ diagram sends node i to the node at the mirrored index.

@[simp]

theorem TauCeti.graphPermA_graphPermA (n : ℕ) (i : Fin n) : (graphPermA n) ((graphPermA n) i) = i

Reversal of a chain is an involution.

@[simp]

theorem TauCeti.lengthPermF4_lengthPermF4 (i : Fin 4) : lengthPermF4 (lengthPermF4 i) = i

Reversing the F₄ diagram is an involution.

@[simp]

theorem TauCeti.cartanMatrix_A_graphPermA (n : ℕ) (i j : Fin n) : (DynkinType.A n).cartanMatrix ((graphPermA n) i) ((graphPermA n) j) = (DynkinType.A n).cartanMatrix i j

Reversal is an automorphism of the type-A Cartan matrix.

@[simp]

theorem TauCeti.cartanMatrix_D_graphPermD (n : ℕ) (hn : 4 ≤ n) (i j : Fin n) : (DynkinType.D n).cartanMatrix ((graphPermD n ⋯) i) ((graphPermD n ⋯) j) = (DynkinType.D n).cartanMatrix i j

Swapping the fork nodes is an automorphism of the type-D Cartan matrix.

@[simp]

theorem TauCeti.cartanMatrix_E6_graphPermE6 (i j : Fin 6) : DynkinType.E6.cartanMatrix (graphPermE6 i) (graphPermE6 j) = DynkinType.E6.cartanMatrix i j

The pinned order-two permutation is an automorphism of the type-E₆ Cartan matrix.

@[simp]

theorem TauCeti.cartanMatrix_D4_trialityPermD4 (i j : Fin 4) : (DynkinType.D 4).cartanMatrix (trialityPermD4 i) (trialityPermD4 j) = (DynkinType.D 4).cartanMatrix i j

The pinned triality permutation is an automorphism of the type-D₄ Cartan matrix.

@[simp]

theorem TauCeti.isLongSimpleRoot_lengthPermRankTwo_iff_not_isLongSimpleRoot_B2 (i : Fin 2) : (DynkinType.B 2).IsLongSimpleRoot (lengthPermRankTwo i) ↔ ¬(DynkinType.B 2).IsLongSimpleRoot i

The rank-two permutation exchanges the long and short nodes of B₂.

@[simp]

theorem TauCeti.isLongSimpleRoot_lengthPermRankTwo_iff_not_isLongSimpleRoot_G2 (i : Fin 2) : DynkinType.G2.IsLongSimpleRoot (lengthPermRankTwo i) ↔ ¬DynkinType.G2.IsLongSimpleRoot i

The rank-two permutation exchanges the long and short nodes of G₂.

@[simp]

theorem TauCeti.isLongSimpleRoot_lengthPermF4_iff_not_isLongSimpleRoot_F4 (i : Fin 4) : DynkinType.F4.IsLongSimpleRoot (lengthPermF4 i) ↔ ¬DynkinType.F4.IsLongSimpleRoot i

Diagram reversal exchanges the long and short nodes of F₄.

The length permutations transpose the Cartan matrix

A length-exchanging permutation is not a symmetry of its diagram: it carries the Cartan matrix to the transposed matrix, which is the Cartan matrix of the dual diagram. That is the reason the families ²B₂, ²G₂ and ²F₄ are built from an odd power of a half-Frobenius rather than from a graph automorphism composed with a field Frobenius, and it is what makes the exceptional isogeny attach the two different exponents 1 and p to the two root lengths.

@[simp]

theorem TauCeti.cartanMatrix_B2_lengthPermRankTwo (i j : Fin 2) : (DynkinType.B 2).cartanMatrix (lengthPermRankTwo i) (lengthPermRankTwo j) = (DynkinType.B 2).cartanMatrix j i

The rank-two length permutation carries the B₂ Cartan matrix to its transpose.

@[simp]

theorem TauCeti.cartanMatrix_G2_lengthPermRankTwo (i j : Fin 2) : DynkinType.G2.cartanMatrix (lengthPermRankTwo i) (lengthPermRankTwo j) = DynkinType.G2.cartanMatrix j i

The rank-two length permutation carries the G₂ Cartan matrix to its transpose.

@[simp]

theorem TauCeti.cartanMatrix_F4_lengthPermF4 (i j : Fin 4) : DynkinType.F4.cartanMatrix (lengthPermF4 i) (lengthPermF4 j) = DynkinType.F4.cartanMatrix j i

Diagram reversal carries the F₄ Cartan matrix to its transpose.

theorem TauCeti.cartanMatrix_B2_submatrix_lengthPermRankTwo_ne : (DynkinType.B 2).cartanMatrix.submatrix ⇑lengthPermRankTwo ⇑lengthPermRankTwo ≠ (DynkinType.B 2).cartanMatrix

The rank-two length permutation is not an automorphism of the B₂ Cartan matrix: the entry it moves to the corner (0, 1) is -1 rather than -2.

theorem TauCeti.cartanMatrix_G2_submatrix_lengthPermRankTwo_ne : DynkinType.G2.cartanMatrix.submatrix ⇑lengthPermRankTwo ⇑lengthPermRankTwo ≠ DynkinType.G2.cartanMatrix

The rank-two length permutation is not an automorphism of the G₂ Cartan matrix.

theorem TauCeti.cartanMatrix_F4_submatrix_lengthPermF4_ne : DynkinType.F4.cartanMatrix.submatrix ⇑lengthPermF4 ⇑lengthPermF4 ≠ DynkinType.F4.cartanMatrix

Diagram reversal is not an automorphism of the F₄ Cartan matrix: it exchanges the two entries -1 and -2 across the double bond.

Symmetries of the Bourbaki-numbered Cartan matrix

def TauCeti.DynkinType.diagramSymmetry (t : DynkinType) : Subgroup (Equiv.Perm (Fin t.rank))

The symmetry group of a Bourbaki-numbered Dynkin diagram: the permutations of the nodes which preserve the Cartan matrix. This is TauCeti.matrixSymmetryGroup at that matrix.

Equations

• t.diagramSymmetry = TauCeti.matrixSymmetryGroup t.cartanMatrix

theorem TauCeti.DynkinType.mem_diagramSymmetry_iff_submatrix {t : DynkinType} {σ : Equiv.Perm (Fin t.rank)} : σ ∈ t.diagramSymmetry ↔ t.cartanMatrix.submatrix ⇑σ ⇑σ = t.cartanMatrix

The matrix form of membership in TauCeti.DynkinType.diagramSymmetry. This is the shape in which TauCeti.serreDiagramAut takes a Cartan-matrix symmetry.

theorem TauCeti.DynkinType.mem_diagramSymmetry_iff {t : DynkinType} {σ : Equiv.Perm (Fin t.rank)} : σ ∈ t.diagramSymmetry ↔ ∀ (i j : Fin t.rank), t.cartanMatrix (σ i) (σ j) = t.cartanMatrix i j

The entrywise form of membership in TauCeti.DynkinType.diagramSymmetry. This is the shape in which the graph permutations above are shown to be diagram symmetries.