The standard representation of the generated short-root type-G2 subgroup

Let k be a commutative 𝔽₃-algebra. The scalar extensions to k of the four numbered simple root subgroups and of the weight torus of the short-root type-G₂ carrier over 𝔽₃ generate a closed subgroup of GL₇ over k, whose coordinate Hopf algebra is TauCeti.G2ShortRoot.PrimeField.generatedCoordinateHopfAlgebra. Its standard representation is the corestriction of the standard O(GL₇)-comodule along the quotient coordinate morphism.

This file proves that the standard representation is faithful, and that it is simple over every field of characteristic three. Restricted to the weight torus it is the direct sum of seven distinct weight lines, the six short roots and zero, so a subcomodule is spanned by the coordinate vectors it contains. The numbered root subgroups at parameter one then move each coordinate vector to its neighbours in the weight string

2α₁ + α₂,  α₁ + α₂,  α₁,  0,  -α₁,  -(α₁ + α₂),  -(2α₁ + α₂),

with coefficient one, except for the two steps out of the zero weight along α₁ and -α₁, which have coefficient two. Two is a unit in characteristic three, so every coordinate vector is reached from every other one. (Over a field of characteristic two the same matrices kill the zero weight vector, which then spans a subrepresentation.)

Main declarations

• TauCeti.G2ShortRoot.PrimeField.generatedWeightTorusCoordinateMap: the weight torus factored through the generated subgroup.
• TauCeti.G2ShortRoot.PrimeField.generatedStandardComodule: its standard comodule on k⁷.
• TauCeti.G2ShortRoot.PrimeField.isFaithful_generatedStandardComodule: faithfulness.
• TauCeti.G2ShortRoot.PrimeField.rootSubgroupPoints_mulVec_mem: subcomodules are stable under the numbered root-subgroup points.
• TauCeti.G2ShortRoot.PrimeField.generatedTorusCorestrict_eq_ofWeights: the weight decomposition under the weight torus.
• TauCeti.G2ShortRoot.PrimeField.instIsSimpleOrderGeneratedSubcomodule: simplicity over a field of characteristic three.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX.

The corestriction and weight-line steps follow the simplicity proof for the type-E₆ minuscule carrier in TauCeti.Algebra.Lie.E6.Minuscule.StandardComodule.

noncomputable def TauCeti.G2ShortRoot.PrimeField.generatedWeightTorusCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : generatedCoordinateHopfAlgebra k ⟶ (DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (Fin 2))).obj

The weight torus of the generated subgroup, as a coordinate morphism into the coordinate Hopf algebra of the rank-two split torus formed directly over k.

Equations

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

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_comp_generatedWeightTorusCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) (generatedWeightTorusCoordinateMap k) = GeneralLinear.weightTorusBaseChangeCoordinateMap (ZMod 3) k weight

Restricted to the generated subgroup, the weight torus is the scalar extension to k of the weight-torus coordinate map over 𝔽₃.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_comp_generatedWeightTorusCoordinateMap_assoc (k : Type u) [CommRing k] [Algebra (ZMod 3) k] {Z : CommHopfAlgCat k} (h : ↧(MonoidAlgebra k ↑(SplitTorus.characterGroup (Fin 2))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) (CategoryTheory.CategoryStruct.comp (generatedWeightTorusCoordinateMap k) h) = CategoryTheory.CategoryStruct.comp (GeneralLinear.weightTorusBaseChangeCoordinateMap (ZMod 3) k weight) h

Restricted to the generated subgroup, the weight torus is the scalar extension to k of the weight-torus coordinate map over 𝔽₃.

@[instance_reducible]

noncomputable def TauCeti.G2ShortRoot.PrimeField.generatedStandardComodule (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : Comodule k (↑(generatedCoordinateHopfAlgebra k)) (Fin 7 → k)

The standard right comodule of the generated short-root type-G₂ subgroup on k⁷.

Equations

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

theorem TauCeti.G2ShortRoot.PrimeField.isFaithful_generatedStandardComodule (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : Comodule.IsFaithful

The standard comodule of the generated short-root type-G₂ subgroup is faithful.

theorem TauCeti.G2ShortRoot.PrimeField.rootSubgroupPoints_mulVec_mem (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (N : Subcomodule k (↑(generatedCoordinateHopfAlgebra k)) (Fin 7 → k)) (j : Fin 2 ⊕ Fin 2) (u : Multiplicative k) {w : Fin 7 → k} (hw : w ∈ N) : (↑↑((rootSubgroupPoints j k) u)).mulVec w ∈ N

A subcomodule of the standard comodule of the generated subgroup is stable under every numbered root-subgroup point.

theorem TauCeti.G2ShortRoot.PrimeField.generatedTorusCorestrict_eq_ofWeights (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : Comodule.Corestrict (CommHopfAlgCat.Hom.hom (generatedWeightTorusCoordinateMap k)).toCoalgHom = Comodule.ofWeights (Pi.basisFun k (Fin 7)) fun (a : Fin 7) => SplitTorus.weightCharacter (weight a)

Restricting the standard comodule of the generated subgroup to the weight torus gives the direct sum of the seven distinct weight lines of the short-root diagram: the coordinate vector at a spans the weight line of the torus character weight a.

Simplicity in characteristic three

instance TauCeti.G2ShortRoot.PrimeField.instIsSimpleOrderGeneratedSubcomodule (k : Type u) [Field k] [Algebra (ZMod 3) k] : IsSimpleOrder (Subcomodule k (↑(generatedCoordinateHopfAlgebra k)) (Fin 7 → k))

The standard comodule of the generated short-root type-G₂ subgroup is simple over every field of characteristic three.