The type-G2 cross product

The seven-dimensional module of type G₂ carries an invariant alternating multiplication, the cross product, together with an invariant symmetric bilinear form. This file writes down the cross product and the invariant form of the dual module in the weight basis of TauCeti.Algebra.Lie.G2.ShortRoot.Basic, says what it is for a matrix to preserve the cross product, and records the contraction of an alternating matrix against it.

The dual form is the one that appears in the applications, because they transport alternating matrices by congruence W ↦ g W gᵀ: what such an argument needs is the matrix B with g B gᵀ = B, which is the Gram matrix of the induced form on the dual module, not of the form on the module itself. For an invertible g the two conditions are equivalent, since gᵀ G g = G is the same as g G⁻¹ gᵀ = G⁻¹; the congruence form is stated because it is what the proofs use and because it does not assume invertibility.

Read on alternating matrices, congruence W ↦ g W gᵀ is the exterior square of g. Away from characteristic two, the contraction kernel identifies the copy of the Lie algebra inside the alternating matrices. It is stable under congruence because g preserves the cross product. In characteristic three, the span of crossBivector is its short-root ideal and is stable when g also fixes the invariant dual form. These facts drive the multiplicativity of the special isogeny; the isogeny itself appears downstream, in TauCeti.Algebra.Lie.G2.ShortRoot.IsogenyMultiplicative.

Main definitions

• TauCeti.G2ShortRoot.crossOperator and TauCeti.G2ShortRoot.invariantDualForm: the cross product, and the invariant symmetric form of the dual module, in the weight basis, with their tables TauCeti.G2ShortRoot.crossOperator_def and TauCeti.G2ShortRoot.invariantDualForm_def.
• TauCeti.G2ShortRoot.crossBivector: the cross-product operators transported by the invariant dual form, alternating matrices that span the short-root ideal in characteristic three.
• Matrix.PreservesG2Cross: multiplicativity of a matrix for the cross product.
• Matrix.g2CrossMap: the contraction of a matrix against the cross product, as a linear map.

Main results

• Matrix.preservesG2Cross_one and Matrix.PreservesG2Cross.mul: the matrices preserving the cross product are closed under multiplication and contain the identity.
• Matrix.PreservesG2Cross.map and TauCeti.G2ShortRoot.preservesDualForm_map: both invariance conditions transport along any ring homomorphism.
• Matrix.g2CrossMap_mul_mul_transpose: a matrix preserving the cross product intertwines the congruence action on alternating matrices with its tautological action on vectors.
• Matrix.g2CrossMap_rankTwo: contraction of u vᵀ - v uᵀ is twice u × v.
• TauCeti.G2ShortRoot.mul_crossBivector_mul_transpose: stability of the short-root span under congruence.
• Matrix.g2CrossMap_crossBivector: in characteristic three the short-root matrices lie in the kernel of the contraction.

References

• R. W. Carter, Simple Groups of Lie Type, §§12.3 and 13.4.
• 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 coordinate cross-product and invariant-form development was adapted from the earlier closed Tau Ceti PR #6708.

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

The seven matrices of the invariant cross product of the seven-dimensional module of type G₂, in the weight basis of TauCeti.Algebra.Lie.G2.ShortRoot.Basic: crossOperator k is the operator v ↦ e_k × v of the alternating multiplication the Lie algebra acts on by derivations.

Equations

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

def TauCeti.G2ShortRoot.invariantDualForm : Matrix (Fin 7) (Fin 7) ℤ

The Gram matrix, in the dual of the weight basis, of the invariant symmetric bilinear form induced on the dual of the seven-dimensional module. Equivalently it is the invariant symmetric tensor in the module tensored with itself, the inverse of the Gram matrix of the invariant form on the module itself, taken primitive over the integers. It pairs the coordinate of a weight with the coordinate of its negative, and a matrix preserves it by the congruence g B gᵀ = B.

Equations

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

theorem TauCeti.G2ShortRoot.crossOperator_def : crossOperator = ![!![0, 0, 0, -2, 0, 0, 0; 0, 0, 0, 0, -2, 0, 0; 0, 0, 0, 0, 0, -2, 0; 0, 0, 0, 0, 0, 0, -1; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0], !![0, 0, 2, 0, 0, 0, 0; 0, 0, 0, 2, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, -1, 0; 0, 0, 0, 0, 0, 0, -2; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0], !![0, -2, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 2, 0, 0, 0; 0, 0, 0, 0, 1, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, -2; 0, 0, 0, 0, 0, 0, 0], !![2, 0, 0, 0, 0, 0, 0; 0, -2, 0, 0, 0, 0, 0; 0, 0, -2, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 2, 0, 0; 0, 0, 0, 0, 0, 2, 0; 0, 0, 0, 0, 0, 0, -2], !![0, 0, 0, 0, 0, 0, 0; 2, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, -1, 0, 0, 0, 0; 0, 0, 0, -2, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 2, 0], !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 2, 0, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, -2, 0, 0, 0; 0, 0, 0, 0, -2, 0, 0], !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0; 0, 2, 0, 0, 0, 0, 0; 0, 0, 2, 0, 0, 0, 0; 0, 0, 0, 2, 0, 0, 0]]

The table of the cross-product operators, the defining equation of TauCeti.G2ShortRoot.crossOperator.

theorem TauCeti.G2ShortRoot.invariantDualForm_def : invariantDualForm = !![0, 0, 0, 0, 0, 0, 2; 0, 0, 0, 0, 0, -2, 0; 0, 0, 0, 0, 2, 0, 0; 0, 0, 0, -1, 0, 0, 0; 0, 0, 2, 0, 0, 0, 0; 0, -2, 0, 0, 0, 0, 0; 2, 0, 0, 0, 0, 0, 0]

The table of the invariant dual form, the defining equation of TauCeti.G2ShortRoot.invariantDualForm.

theorem TauCeti.G2ShortRoot.weight_eq_add_of_crossOperator_ne_zero (k i j : Fin 7) (h : crossOperator k i j ≠ 0) : weight i = weight k + weight j

A nonzero cross-product coefficient has output weight equal to the sum of the input weights.

theorem TauCeti.G2ShortRoot.weight_add_eq_zero_of_invariantDualForm_ne_zero (i j : Fin 7) (h : invariantDualForm i j ≠ 0) : weight i + weight j = 0

The invariant dual form pairs only basis vectors whose weights sum to zero.

def TauCeti.G2ShortRoot.crossBivector (a : Fin 7) : Matrix (Fin 7) (Fin 7) ℤ

The seven matrices crossOperator a * invariantDualForm, the cross-product operators transported by the invariant dual form. They are alternating, and in characteristic three they span the short-root ideal of the Lie algebra, read inside the alternating matrices.

Equations

• TauCeti.G2ShortRoot.crossBivector a = TauCeti.G2ShortRoot.crossOperator a * TauCeti.G2ShortRoot.invariantDualForm

theorem TauCeti.G2ShortRoot.crossBivector_eq : crossBivector = ![!![0, 0, 0, 2, 0, 0, 0; 0, 0, -4, 0, 0, 0, 0; 0, 4, 0, 0, 0, 0, 0; -2, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0], !![0, 0, 0, 0, 4, 0, 0; 0, 0, 0, -2, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 2, 0, 0, 0, 0, 0; -4, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0], !![0, 0, 0, 0, 0, 4, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, -2, 0, 0, 0; 0, 0, 2, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; -4, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0], !![0, 0, 0, 0, 0, 0, 4; 0, 0, 0, 0, 0, 4, 0; 0, 0, 0, 0, -4, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 4, 0, 0, 0, 0; 0, -4, 0, 0, 0, 0, 0; -4, 0, 0, 0, 0, 0, 0], !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 4; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, -2, 0, 0; 0, 0, 0, 2, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, -4, 0, 0, 0, 0, 0], !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 4; 0, 0, 0, 0, 0, -2, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 2, 0, 0, 0; 0, 0, -4, 0, 0, 0, 0], !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 2; 0, 0, 0, 0, 0, -4, 0; 0, 0, 0, 0, 4, 0, 0; 0, 0, 0, -2, 0, 0, 0]]

The entries of the transported cross-product operators, computed once from the two tables so that a coordinate argument does not recompute a matrix product for every entry it reads.

theorem TauCeti.G2ShortRoot.crossBivector_def (a : Fin 7) : crossOperator a * invariantDualForm = crossBivector a

Transporting a cross-product operator by the invariant dual form gives the corresponding alternating matrix. This is the defining equation of TauCeti.G2ShortRoot.crossBivector, stated because the module system hides the body from a consumer.

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

A matrix preserves the cross product when it is multiplicative for it, g (u × v) = (g u) × (g v), written as one matrix identity for each basis vector of the first argument.

Equations

• g.PreservesG2Cross = ∀ (k : Fin 7), g * (TauCeti.G2ShortRoot.crossOperator k).map Int.cast = (∑ a : Fin 7, g a k • (TauCeti.G2ShortRoot.crossOperator a).map Int.cast) * g

theorem Matrix.preservesG2Cross_def {R : Type u} [CommRing R] (g : Matrix (Fin 7) (Fin 7) R) : g.PreservesG2Cross ↔ ∀ (k : Fin 7), g * (TauCeti.G2ShortRoot.crossOperator k).map Int.cast = (∑ a : Fin 7, g a k • (TauCeti.G2ShortRoot.crossOperator a).map Int.cast) * g

The defining equations of cross-product preservation.

@[simp]

theorem Matrix.preservesG2Cross_one {R : Type u} [CommRing R] : PreservesG2Cross 1

The identity matrix preserves the cross product.

theorem Matrix.PreservesG2Cross.mul {R : Type u} [CommRing R] {g h : Matrix (Fin 7) (Fin 7) R} (hg : g.PreservesG2Cross) (hh : h.PreservesG2Cross) : (g * h).PreservesG2Cross

Matrices preserving the cross product are closed under multiplication.

theorem Matrix.PreservesG2Cross.map {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) {g : Matrix (Fin 7) (Fin 7) R} (hg : g.PreservesG2Cross) : (g.map ⇑f).PreservesG2Cross

Preserving the type-G₂ cross product is inherited by the image of a matrix under a ring homomorphism.

theorem TauCeti.G2ShortRoot.preservesDualForm_map {S : Type u_1} {T : Type u_2} [Ring S] [Ring T] (f : S →+* T) {M : Matrix (Fin 7) (Fin 7) S} (h : M * invariantDualForm.map Int.cast * M.transpose = invariantDualForm.map Int.cast) : M.map ⇑f * invariantDualForm.map Int.cast * (M.map ⇑f).transpose = invariantDualForm.map Int.cast

Fixing the invariant dual form by congruence is inherited by the image of a matrix under a ring homomorphism.

theorem TauCeti.G2ShortRoot.mul_crossBivector_mul_transpose {R : Type u} [CommRing R] {g : Matrix (Fin 7) (Fin 7) R} (hg : g.PreservesG2Cross) (hB : g * invariantDualForm.map Int.cast * g.transpose = invariantDualForm.map Int.cast) (k : Fin 7) : g * (crossBivector k).map Int.cast * g.transpose = ∑ a : Fin 7, g a k • (crossBivector a).map Int.cast

The span of the alternating matrices crossBivector is stable under congruence. A matrix preserving the cross product and fixing the invariant dual form by congruence permutes them through the tautological action on their index.

def Matrix.g2CrossMap {R : Type u} [CommRing R] : Matrix (Fin 7) (Fin 7) R →ₗ[R] Fin 7 → R

The cross product contracted against a matrix: the m-th coordinate of g2CrossMap W pairs W with the m-th row of the cross-product operators. It reads the cross product on the exterior square up to a factor of two, g2CrossMap (u vᵀ - v uᵀ) = 2 (u × v), the two counting the two orderings of the double contraction.

Equations

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

theorem Matrix.g2CrossMap_def {R : Type u} [CommRing R] (W : Matrix (Fin 7) (Fin 7) R) (m : Fin 7) : g2CrossMap W m = ∑ k : Fin 7, ((TauCeti.G2ShortRoot.crossOperator k).map Int.cast * W.transpose) m k

The defining formula of the contraction.

theorem Matrix.g2CrossMap_map {R : Type u} [CommRing R] (W : Matrix (Fin 7) (Fin 7) ℤ) (m : Fin 7) : g2CrossMap (W.map Int.cast) m = ↑(g2CrossMap W m)

The contraction of the image of an integral matrix is the integer contraction, coerced.

@[simp]

theorem Matrix.g2CrossMap_crossBivector {R : Type u} [CommRing R] [CharP R 3] (a m : Fin 7) : g2CrossMap ((TauCeti.G2ShortRoot.crossBivector a).map Int.cast) m = 0

In characteristic three the matrices spanning the short-root ideal lie in the kernel of the contraction: over the integers their contractions are divisible by three.

theorem Matrix.g2CrossMap_mul_mul_transpose {R : Type u} [CommRing R] {g : Matrix (Fin 7) (Fin 7) R} (hg : g.PreservesG2Cross) (W : Matrix (Fin 7) (Fin 7) R) (m : Fin 7) : g2CrossMap (g * W * g.transpose) m = ∑ c : Fin 7, g m c * g2CrossMap W c

The contraction is equivariant. A matrix preserving the cross product intertwines its congruence action on alternating matrices with its tautological action on vectors.

theorem Matrix.g2CrossMap_apply {R : Type u} [CommRing R] (W : Matrix (Fin 7) (Fin 7) R) (m : Fin 7) : g2CrossMap W m = ∑ k : Fin 7, ∑ l : Fin 7, ↑(TauCeti.G2ShortRoot.crossOperator k m l) * W k l

The contraction written entrywise.

theorem Matrix.g2CrossMap_rankTwo {R : Type u} [CommRing R] (u v : Fin 7 → R) (m : Fin 7) : g2CrossMap (of fun (i j : Fin 7) => u i * v j - v i * u j) m = 2 * ∑ k : Fin 7, u k * ∑ l : Fin 7, ↑(TauCeti.G2ShortRoot.crossOperator k m l) * v l

The contraction of a rank-two alternating matrix is twice the cross product. The cross product u × v is written through crossOperator, avoiding a second public definition of the same bilinear operation.

@[simp]

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

The matrices crossBivector are alternating over any commutative ring.

@[simp]

theorem TauCeti.G2ShortRoot.crossBivector_apply_self (l a : Fin 7) : crossBivector l a a = 0

The matrices crossBivector have zero diagonal.