The standard comodule of the generated type-E₆ minuscule subgroup

The subgroup of GL₂₇ generated directly over a commutative ring by the numbered minuscule root subgroups and weight torus has a faithful standard comodule. Over any field this comodule is simple: the torus separates the 27 weight lines, and the root matrices connect them.

This subgroup is not identified with the specialization of the integral minuscule carrier. In particular, its representation-theoretic properties do not imply reducedness of that specialization. The two comodules share their weight decomposition and root matrices, so the simplicity criterion TauCeti.E6Minuscule.isSimpleOrder_of_minusculeWeights_of_rootSubgroupPoints applies to both without repeating the weight-graph argument.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.

The quotient-comodule construction follows TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generated.StandardComodule.

noncomputable def TauCeti.E6Minuscule.generatedWeightTorusCoordinateMap (R : Type u) [CommRing R] : generatedCoordinateHopfAlgebra R ⟶ (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (Fin 6))).obj

The weight torus factored through the subgroup generated over R.

Equations

• TauCeti.E6Minuscule.generatedWeightTorusCoordinateMap R = TauCeti.E6Minuscule.generatedCoordinateLift R (Sum.inr ())

@[simp]

theorem TauCeti.E6Minuscule.generatedCoordinateMap_comp_generatedWeightTorusCoordinateMap (R : Type u) [CommRing R] : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap R) (generatedWeightTorusCoordinateMap R) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ R weightTable.weight

The generated subgroup's weight torus recovers the ambient minuscule weight torus.

@[simp]

theorem TauCeti.E6Minuscule.generatedCoordinateMap_comp_generatedWeightTorusCoordinateMap_assoc (R : Type u) [CommRing R] {Z : CommHopfAlgCat R} (h : ↧(MonoidAlgebra R ↑(SplitTorus.characterGroup (Fin 6))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap R) (CategoryTheory.CategoryStruct.comp (generatedWeightTorusCoordinateMap R) h) = CategoryTheory.CategoryStruct.comp (GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ R weightTable.weight) h

The generated subgroup's weight torus recovers the ambient minuscule weight torus.

@[simp]

theorem TauCeti.E6Minuscule.pointToGeneralLinear_mapDomain_generatedCoordinateLift_inl_eq_rootSubgroupPoints (R : Type u) [CommRing R] (i : Fin 6 ⊕ Fin 6) (B : CommAlgCat R) (q : ↑(HopfAlgebra.points B)) : GeneralLinear.pointToGeneralLinear 27 ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom (generatedCoordinateMap R))) (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (generatedCoordinateLift R (Sum.inl i)))))) = ↑((rootSubgroupPoints i ↑B) (AdditiveGroup.gaPointsMulEquiv q))

A point induced by a generated root-subgroup lift maps to the numbered minuscule root matrix with the same parameter, over every value algebra.

@[instance_reducible]

noncomputable def TauCeti.E6Minuscule.generatedStandardComodule (R : Type u) [CommRing R] : Comodule R (↑(generatedCoordinateHopfAlgebra R)) (Fin 27 → R)

The standard right comodule of the generated type-E₆ minuscule subgroup on R²⁷.

Equations

• TauCeti.E6Minuscule.generatedStandardComodule R = TauCeti.GeneralLinear.corestrictStandardComodule R 27 (CommHopfAlgCat.Hom.hom (TauCeti.E6Minuscule.generatedCoordinateMap R))

theorem TauCeti.E6Minuscule.isFaithful_generatedStandardComodule (R : Type u) [CommRing R] : Comodule.IsFaithful

The standard comodule of the generated type-E₆ minuscule subgroup is faithful over every commutative ring.

theorem TauCeti.E6Minuscule.generatedRootSubgroupPoints_mulVec_mem (R : Type u) [CommRing R] (N : Subcomodule R (↑(generatedCoordinateHopfAlgebra R)) (Fin 27 → R)) (i : Fin 6 ⊕ Fin 6) (t : Multiplicative R) {w : Fin 27 → R} (hw : w ∈ N) : (↑↑((rootSubgroupPoints i R) t)).mulVec w ∈ N

A subcomodule of the generated subgroup's standard comodule is stable under each numbered positive and negative root-subgroup matrix, with any parameter.

theorem TauCeti.E6Minuscule.generatedTorusCorestrict_eq_ofWeights (R : Type u) [CommRing R] : Comodule.Corestrict (CommHopfAlgCat.Hom.hom (generatedWeightTorusCoordinateMap R)).toCoalgHom = Comodule.ofWeights (Pi.basisFun R (Fin 27)) minusculeCharacter

Restriction of the generated subgroup's standard comodule to the weight torus is the direct sum of the 27 minuscule weight lines.

instance TauCeti.E6Minuscule.instIsSimpleOrderGeneratedSubcomodule (k : Type u) [Field k] : have x := generatedStandardComodule k; IsSimpleOrder (Subcomodule k (↑(generatedCoordinateHopfAlgebra k)) (Fin 27 → k))

The standard comodule of the generated type-E₆ minuscule subgroup is simple over every field, including characteristics two and three.