Tensor invariance for the short-root type-G2 carrier over the prime field

The four numbered simple root subgroups and the weight torus of the short-root type-G₂ carrier over 𝔽₃ preserve the type-G₂ cross product and fix the invariant dual form by congruence. Both statements are equations between matrices, so they pass from the generators to the whole generated subgroup of points, and hence to the universal point of the carrier's coordinate Hopf algebra.

This is what the special isogeny of characteristic three needs: by Matrix.g2SpecialIsogeny_mul, the matrix Matrix.g2SpecialIsogeny of signed two-by-two minors is multiplicative on a product g * h of matrices preserving the cross product whenever the left factor g also fixes the invariant dual form by congruence. Points of the carrier satisfy both hypotheses.

Main results

• TauCeti.G2ShortRoot.PrimeField.preservesG2Cross_of_mem_points and TauCeti.G2ShortRoot.PrimeField.preservesDualForm_of_mem_points: every matrix-valued point of the carrier preserves both tensors.
• TauCeti.G2ShortRoot.PrimeField.preservesG2Cross_carrierGenericMatrix and TauCeti.G2ShortRoot.PrimeField.preservesDualForm_carrierGenericMatrix: the universal point does too.

References

• S. Garibaldi and R. M. Guralnick, Simple groups stabilizing polynomials, Forum of Mathematics Pi 3 (2015), §6.
• R. W. Carter, Simple Groups of Lie Type, §§12.3 and 13.4.

theorem TauCeti.G2ShortRoot.PrimeField.exists_map_genericMatrix_generator_inl (k : Fin 2 ⊕ Fin 2) : ∃ (u : Multiplicative ↑(AdditiveGroup.coordinateHopfAlgebra (ZMod 3))), (GeneralLinear.genericMatrix (ZMod 3) 7).map ⇑↑(CommHopfAlgCat.Hom.hom (generator (Sum.inl k))) = ↑↑((rootSubgroupPoints k ↑(AdditiveGroup.coordinateHopfAlgebra (ZMod 3))) u)

The generic matrix of GL₇ pushed along the coordinate map of a numbered simple root subgroup is the matrix of a root-subgroup point at a universal parameter.

theorem TauCeti.G2ShortRoot.PrimeField.exists_map_genericMatrix_generator_inr : ∃ (s : Fin 2 → (↑(DiagonalizableGroup.coordinateRing (ZMod 3) (SplitTorus.characterGroup (Fin 2))).obj)ˣ), (GeneralLinear.genericMatrix (ZMod 3) 7).map ⇑↑(CommHopfAlgCat.Hom.hom (generator (Sum.inr ()))) = ↑↑((weightTorusPoints ↑(DiagonalizableGroup.coordinateRing (ZMod 3) (SplitTorus.characterGroup (Fin 2))).obj) s)

The generic matrix of GL₇ pushed along the coordinate map of the weight torus is the matrix of a torus point at universal coordinates.

theorem TauCeti.G2ShortRoot.PrimeField.coe_rootSubgroupPoints_inl_zero {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inl 0) A) (Multiplicative.ofAdd t)) = 1 + t • (raisingMatrix 0).map Int.cast + t ^ 2 • Matrix.single 2 4 1

The matrix of the point at parameter t of the root subgroup numbered inl 0.

theorem TauCeti.G2ShortRoot.PrimeField.coe_rootSubgroupPoints_inl_one {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inl 1) A) (Multiplicative.ofAdd t)) = 1 + t • (raisingMatrix 1).map Int.cast

The matrix of the point at parameter t of the root subgroup numbered inl 1.

theorem TauCeti.G2ShortRoot.PrimeField.coe_rootSubgroupPoints_inr_zero {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inr 0) A) (Multiplicative.ofAdd t)) = 1 + t • (loweringMatrix 0).map Int.cast + t ^ 2 • Matrix.single 4 2 1

The matrix of the point at parameter t of the root subgroup numbered inr 0.

theorem TauCeti.G2ShortRoot.PrimeField.coe_rootSubgroupPoints_inr_one {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inr 1) A) (Multiplicative.ofAdd t)) = 1 + t • (loweringMatrix 1).map Int.cast

The matrix of the point at parameter t of the root subgroup numbered inr 1.

theorem TauCeti.G2ShortRoot.PrimeField.preservesG2Cross_of_mem_points {A : Type v} [CommRing A] [Algebra (ZMod 3) A] {g : GL (Fin 7) A} (hg : g ∈ points A) : (↑g).PreservesG2Cross

Every point of the short-root type-G₂ carrier preserves the invariant cross product.

theorem TauCeti.G2ShortRoot.PrimeField.preservesDualForm_of_mem_points {A : Type v} [CommRing A] [Algebra (ZMod 3) A] {g : GL (Fin 7) A} (hg : g ∈ points A) : ↑g * invariantDualForm.map Int.cast * (↑g).transpose = invariantDualForm.map Int.cast

Every point of the short-root type-G₂ carrier fixes the invariant dual form by congruence.

theorem TauCeti.G2ShortRoot.PrimeField.preservesG2Cross_carrierGenericMatrix : carrierGenericMatrix.PreservesG2Cross

The universal point of the carrier preserves the invariant cross product.

theorem TauCeti.G2ShortRoot.PrimeField.preservesDualForm_carrierGenericMatrix : carrierGenericMatrix * invariantDualForm.map Int.cast * carrierGenericMatrix.transpose = invariantDualForm.map Int.cast

The universal point of the carrier fixes the invariant dual form by congruence.