The special isogeny of type G2 as a matrix of minors

Over a field of characteristic three the group of type G₂ admits an endomorphism τ exchanging the two root lengths: it raises the parameter of a short simple root element to the third power and leaves that of a long one alone. It is the special isogeny, and the Ree groups ²G₂(3^(2m+1)) are cut out by the fixed points of its odd powers. This file writes τ as the explicit polynomial map Matrix.g2SpecialIsogeny of signed 2 × 2 minors of a 7 × 7 matrix, read in the weight basis of the seven-dimensional module of TauCeti.Algebra.Lie.G2.ShortRoot.Basic, and computes it on the simple root elements and on the diagonal torus of that module.

Where the formula comes from

The type-G₂ Lie algebra acts on the seven-dimensional module V, and in characteristic three the span I of the short root vectors and the short coroots is an ideal of it. The quotient by I is again seven-dimensional, with the six long roots and zero as its weights, and the adjoint action of a group element on that quotient, read in a basis matched to the weight basis of V through the length-exchanging map on weights, is the special isogeny. The Lie algebra lies in the skew endomorphisms of V for its invariant symmetric form, so every entry of that adjoint action is a signed sum of 2 × 2 minors of the group element; the seven index pairs and the two corrections at the middle index are the resulting bookkeeping. That the formula is multiplicative in characteristic three, when both matrices preserve the invariant cross product and the left factor also fixes the invariant dual form by congruence, is proved in TauCeti.Algebra.Lie.G2.ShortRoot.IsogenyMultiplicative.

What is proved here

The pinning equations and the torus equation are polynomial identities valid over every commutative ring, and none of them assumes a characteristic. The simple root elements are written as explicit matrices, 1 + t E + t² E⁽²⁾ for the raising generator E of TauCeti.G2ShortRoot.raisingMatrix and its divided square, and likewise for the lowering generators; this file does not construct a group containing them.

Main definitions

• TauCeti.g2SpecialIsogenyPair: the seven index pairs carrying the minors.
• Matrix.g2SpecialIsogenyColumn: the column combinations of minors on a fixed row pair.
• Matrix.g2SpecialIsogeny: the matrix of signed 2 × 2 minors carrying the isogeny.

Main results

• Matrix.g2SpecialIsogeny_one, Matrix.g2SpecialIsogeny_map and Matrix.g2SpecialIsogeny_diagonal: the formula fixes the identity, commutes with entrywise ring morphisms, and sends diagonal matrices to diagonal matrices.
• TauCeti.G2ShortRoot.g2SpecialIsogeny_one_add_smul_raisingMatrix_zero and its three siblings: the pinning equations τ (x_{α₁}(t)) = x_{α₂}(t³) and τ (x_{α₂}(t)) = x_{α₁}(t), together with their negative-root counterparts, so τ exchanges the two root lengths with exponent three at the short simple root and one at the long one.
• TauCeti.G2ShortRoot.g2SpecialIsogeny_diagonal_torusCharacter: on the diagonal torus of the weight basis the formula acts through (s₀, s₁) ↦ (s₁, s₀³).

References

• R. W. Carter, Simple Groups of Lie Type, §§12.3 and 13.4.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• S. Garibaldi and R. M. Guralnick, Simple groups stabilizing polynomials, Forum of Mathematics Pi 3 (2015), §6, for the quotient by the short-root ideal in characteristic three.
• The explicit matrix formula and pinning computations were adapted from the earlier closed Tau Ceti PR #6703.

The shape of the definitions follows the special isogeny of Sp₄ in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.SpecialIsogeny.

def TauCeti.g2SpecialIsogenyPair : Fin 7 → Fin 7 × Fin 7

The seven index pairs whose 2 × 2 minors carry the type-G₂ special isogeny.

Equations

• TauCeti.g2SpecialIsogenyPair = ![(0, 1), (0, 2), (1, 4), (1, 5), (2, 5), (4, 6), (5, 6)]

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_zero : g2SpecialIsogenyPair 0 = (0, 1)

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_one : g2SpecialIsogenyPair 1 = (0, 2)

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_two : g2SpecialIsogenyPair 2 = (1, 4)

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_three : g2SpecialIsogenyPair 3 = (1, 5)

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_four : g2SpecialIsogenyPair 4 = (2, 5)

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_five : g2SpecialIsogenyPair 5 = (4, 6)

@[simp]

theorem TauCeti.g2SpecialIsogenyPair_six : g2SpecialIsogenyPair 6 = (5, 6)

def Matrix.g2SpecialIsogenyColumn {R : Type u} [CommRing R] (g : Matrix (Fin 7) (Fin 7) R) (p : Fin 7 × Fin 7) (j : Fin 7) : R

The minors of g on a fixed row pair p against the j-th column combination: the pair TauCeti.g2SpecialIsogenyPair j, joined by the pair (2, 4) at the middle index 3.

Equations

• g.g2SpecialIsogenyColumn p j = g.pairMinor p (TauCeti.g2SpecialIsogenyPair j) + if j = 3 then g.pairMinor p (2, 4) else 0

@[simp]

theorem Matrix.g2SpecialIsogenyColumn_def {R : Type u} [CommRing R] (g : Matrix (Fin 7) (Fin 7) R) (p : Fin 7 × Fin 7) (j : Fin 7) : g.g2SpecialIsogenyColumn p j = g.pairMinor p (TauCeti.g2SpecialIsogenyPair j) + if j = 3 then g.pairMinor p (2, 4) else 0

The defining equation of the column combination of minors.

def Matrix.g2SpecialIsogeny {R : Type u} [CommRing R] (g : Matrix (Fin 7) (Fin 7) R) : Matrix (Fin 7) (Fin 7) R

The type-G₂ matrix of signed 2 × 2 minors. Its (i, j) entry reads the j-th column combination of minors on the row pair TauCeti.g2SpecialIsogenyPair i, diminished at the middle index 3 by the same combination taken on the row pair (0, 6).

Equations

• g.g2SpecialIsogeny = Matrix.of fun (i j : Fin 7) => g.g2SpecialIsogenyColumn (TauCeti.g2SpecialIsogenyPair i) j - if i = 3 then g.g2SpecialIsogenyColumn (0, 6) j else 0

@[simp]

theorem Matrix.g2SpecialIsogeny_apply {R : Type u} [CommRing R] (g : Matrix (Fin 7) (Fin 7) R) (i j : Fin 7) : g.g2SpecialIsogeny i j = g.g2SpecialIsogenyColumn (TauCeti.g2SpecialIsogenyPair i) j - if i = 3 then g.g2SpecialIsogenyColumn (0, 6) j else 0

The entrywise formula for the type-G₂ matrix of signed minors.

@[simp]

theorem Matrix.g2SpecialIsogeny_map {R : Type u} [CommRing R] {S : Type u_1} {F : Type u_2} [CommRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (g : Matrix (Fin 7) (Fin 7) R) : (g.map ⇑f).g2SpecialIsogeny = g.g2SpecialIsogeny.map ⇑f

The formula commutes with entrywise application of any morphism of rings.

@[simp]

theorem Matrix.g2SpecialIsogeny_diagonal {R : Type u} [CommRing R] (d : Fin 7 → R) : (diagonal d).g2SpecialIsogeny = diagonal ![d 0 * d 1, d 0 * d 2, d 1 * d 4, d 1 * d 5, d 2 * d 5, d 4 * d 6, d 5 * d 6]

The formula sends diagonal matrices to diagonal matrices, pairing up the entries along the seven distinguished index pairs. The two corrections at the middle index contribute nothing, because the pairs they add are distinct from all seven.

@[simp]

theorem Matrix.g2SpecialIsogeny_one {R : Type u} [CommRing R] : g2SpecialIsogeny 1 = 1

The formula fixes the identity matrix.

The action on the simple root elements

theorem TauCeti.G2ShortRoot.g2SpecialIsogeny_one_add_smul_raisingMatrix_zero {R : Type u} [CommRing R] (t : R) : (1 + t • (raisingMatrix 0).map Int.cast + t ^ 2 • Matrix.single 2 4 1).g2SpecialIsogeny = 1 + t ^ 3 • (raisingMatrix 1).map Int.cast

The special isogeny on the short positive simple root element: τ (x_{α₁}(t)) = x_{α₂}(t³), the parameter cubed and the root exchanged for the long one.

theorem TauCeti.G2ShortRoot.g2SpecialIsogeny_one_add_smul_raisingMatrix_one {R : Type u} [CommRing R] (t : R) : (1 + t • (raisingMatrix 1).map Int.cast).g2SpecialIsogeny = 1 + t • (raisingMatrix 0).map Int.cast + t ^ 2 • Matrix.single 2 4 1

The special isogeny on the long positive simple root element: τ (x_{α₂}(t)) = x_{α₁}(t), the parameter kept and the root exchanged for the short one.

theorem TauCeti.G2ShortRoot.g2SpecialIsogeny_one_add_smul_loweringMatrix_zero {R : Type u} [CommRing R] (t : R) : (1 + t • (loweringMatrix 0).map Int.cast + t ^ 2 • Matrix.single 4 2 1).g2SpecialIsogeny = 1 + t ^ 3 • (loweringMatrix 1).map Int.cast

The special isogeny on the short negative simple root element: τ (x_{-α₁}(t)) = x_{-α₂}(t³).

theorem TauCeti.G2ShortRoot.g2SpecialIsogeny_one_add_smul_loweringMatrix_one {R : Type u} [CommRing R] (t : R) : (1 + t • (loweringMatrix 1).map Int.cast).g2SpecialIsogeny = 1 + t • (loweringMatrix 0).map Int.cast + t ^ 2 • Matrix.single 4 2 1

The special isogeny on the long negative simple root element: τ (x_{-α₂}(t)) = x_{-α₁}(t).

The action on the diagonal torus

theorem TauCeti.G2ShortRoot.g2SpecialIsogeny_diagonal_torusCharacter {R : Type u} [CommRing R] (s : Fin 2 → Rˣ) : (Matrix.diagonal fun (a : Fin 7) => ↑(torusCharacter s (weight a))).g2SpecialIsogeny = Matrix.diagonal fun (a : Fin 7) => ↑(torusCharacter ![s 1, s 0 ^ 3] (weight a))

The special isogeny on the diagonal torus. On the diagonal matrix of the weight characters of a torus point s, the formula returns the diagonal matrix of the weight characters of the length-exchanged point (s₁, s₀³). On characters this is the map μ ↦ (3 μ₁, μ₀) that the special isogeny induces on the character lattice.