Multiplicativity of the type-G2 special isogeny

The (i, j) entry of Matrix.g2SpecialIsogeny g is a fixed linear functional applied to the congruence transform g W gᵀ of a fixed alternating matrix. Multiplicativity of the minor formula therefore asks that the seven alternating matrices isogenySource and the seven functionals isogenyProjection split a g-stable subspace of the alternating matrices.

That subspace is the copy of the Lie algebra: the kernel of the contraction Matrix.g2CrossMap against the cross product, which is stable exactly because g preserves the cross product. Inside it, the kernel of the seven functionals is the short-root ideal, spanned by the matrices crossBivector, which in characteristic three is again stable, because g fixes the invariant dual form as well. The proof splits this subspace in characteristic three: that is where the short-root vectors span an ideal and where the seven matrices crossBivector fall into the kernel of the contraction.

Multiplicativity fails on the whole of GL₇, so the two preservation hypotheses cannot be dropped. Nothing below verifies them for any particular matrix, and no group of matrix-valued points is formed on which the formula would restrict to an endomorphism.

Main definitions

• TauCeti.G2ShortRoot.isogenySource and TauCeti.G2ShortRoot.isogenyProjection: the alternating matrices and the functionals through which the minor formula is read, with TauCeti.G2ShortRoot.isogenySource_eq writing the former through single unit matrices.

Main results

• Matrix.g2SpecialIsogeny_apply_eq: the minor formula as a functional of a congruence transform.
• Matrix.g2SpecialIsogeny_mul: multiplicativity of the special isogeny.

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 cross product and the short-root ideal in characteristic three.
• The congruence setup was adapted from the earlier closed Tau Ceti PR #6703, and the splitting and multiplicativity argument from its successor Tau Ceti PR #6708.

def TauCeti.G2ShortRoot.isogenySource : Fin 7 → Matrix (Fin 7) (Fin 7) ℤ

The seven alternating matrices whose congruence transforms the special isogeny reads: the alternating matrix of the j-th distinguished index pair, joined at the middle index by the alternating matrix of the pair (2, 4).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.isogenySource_eq (j : Fin 7) : isogenySource j = Matrix.single (g2SpecialIsogenyPair j).1 (g2SpecialIsogenyPair j).2 1 - Matrix.single (g2SpecialIsogenyPair j).2 (g2SpecialIsogenyPair j).1 1 + if j = 3 then Matrix.single 2 4 1 - Matrix.single 4 2 1 else 0

The alternating matrices read by the special isogeny: the j-th is the alternating matrix e_p ∧ e_q of the distinguished index pair (p, q) = TauCeti.g2SpecialIsogenyPair j, joined at the middle index 3 by the alternating matrix of the pair (2, 4).

@[simp]

theorem Matrix.g2CrossMap_isogenySource {R : Type u} [CommRing R] (j m : Fin 7) : g2CrossMap ((TauCeti.G2ShortRoot.isogenySource j).map Int.cast) m = 0

The alternating matrices read by the special isogeny lie in the kernel of the contraction, so they lie in the Lie algebra.

def TauCeti.G2ShortRoot.isogenyProjection {R : Type u} [CommRing R] (i : Fin 7) : Matrix (Fin 7) (Fin 7) R →ₗ[R] R

The linear functional the special isogeny reads on the i-th distinguished index pair: the entry there, diminished at the middle index by the entry at the pair (0, 6).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.isogenyProjection_apply {R : Type u} [CommRing R] (i : Fin 7) (W : Matrix (Fin 7) (Fin 7) R) : (isogenyProjection i) W = W (g2SpecialIsogenyPair i).1 (g2SpecialIsogenyPair i).2 - if i = 3 then W 0 6 else 0

The entrywise formula for the functional.

@[simp]

theorem TauCeti.G2ShortRoot.isogenyProjection_isogenySource {R : Type u} [CommRing R] (i j : Fin 7) : (isogenyProjection i) ((isogenySource j).map Int.cast) = if i = j then 1 else 0

The functionals and the alternating matrices isogenySource are dual to one another.

@[simp]

theorem TauCeti.G2ShortRoot.isogenyProjection_crossBivector {R : Type u} [CommRing R] (i a : Fin 7) : (isogenyProjection i) ((crossBivector a).map Int.cast) = 0

The functionals kill the alternating matrices spanning the short-root ideal.

theorem Matrix.g2SpecialIsogeny_apply_eq {R : Type u} [CommRing R] (g : Matrix (Fin 7) (Fin 7) R) (i j : Fin 7) : g.g2SpecialIsogeny i j = (TauCeti.G2ShortRoot.isogenyProjection i) (g * (TauCeti.G2ShortRoot.isogenySource j).map Int.cast * g.transpose)

The minor formula read by congruence. The (i, j) entry of the special isogeny of g is the i-th functional applied to the congruence transform by g of the j-th alternating matrix.

@[simp]

theorem TauCeti.G2ShortRoot.transpose_isogenySource_map {R : Type u} [CommRing R] (l : Fin 7) : ((isogenySource l).map Int.cast).transpose = -(isogenySource l).map Int.cast

The alternating matrices read by the special isogeny are alternating over any commutative ring.

theorem Matrix.g2SpecialIsogeny_mul {R : Type u} [CommRing R] [CharP R 3] {g h : Matrix (Fin 7) (Fin 7) R} (hg : g.PreservesG2Cross) (hgB : g * TauCeti.G2ShortRoot.invariantDualForm.map Int.cast * g.transpose = TauCeti.G2ShortRoot.invariantDualForm.map Int.cast) (hh : h.PreservesG2Cross) : (g * h).g2SpecialIsogeny = g.g2SpecialIsogeny * h.g2SpecialIsogeny

The special isogeny is multiplicative in characteristic three on matrices preserving the cross product, the left factor fixing the invariant dual form by congruence as well. Multiplicativity fails on the whole of GL₇: it is the two preservation hypotheses that make the quotient by the short-root ideal an invariant subquotient and so turn the minor formula into a homomorphism. Nothing here verifies those hypotheses for any particular matrix.