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

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

This subgroup is not identified here with the specialization of the integral minuscule carrier. The two comodules share their weight decomposition and root matrices, so the simplicity criterion TauCeti.E7Minuscule.isSimpleOrder_of_minusculeWeights_of_rootSubgroupPoints applies to both without repeating the weight-graph argument.

Main declarations

• TauCeti.E7Minuscule.generatedWeightTorusCoordinateMap: the weight torus factored through the generated subgroup.
• TauCeti.E7Minuscule.generatedStandardComodule: the standard comodule on R⁵⁶.
• TauCeti.E7Minuscule.isFaithful_generatedStandardComodule: faithfulness over every commutative ring.
• TauCeti.E7Minuscule.generatedRootSubgroupPoints_mulVec_mem: subcomodules are stable under the numbered root-subgroup matrices.
• TauCeti.E7Minuscule.generatedTorusCorestrict_eq_ofWeights: the weight decomposition under the weight torus.
• TauCeti.E7Minuscule.instIsSimpleOrderGeneratedSubcomodule: simplicity over every field.

References

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

The construction is adapted from the generated type-E₆ minuscule subgroup in TauCeti.Algebra.Lie.E6.Minuscule.Generated.StandardComodule.

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

The weight torus factored through the subgroup generated over R.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.generatedCoordinateMap_comp_generatedWeightTorusCoordinateMap (R : Type u) [CommRing R] : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap R) (generatedWeightTorusCoordinateMap R) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ R DynkinType.e7MinusculeWeight

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

@[simp]

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

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

@[simp]

theorem TauCeti.E7Minuscule.pointToGeneralLinear_mapDomain_generatedCoordinateLift_inl_eq_rootSubgroupPoints (R : Type u) [CommRing R] (i : Fin 7 ⊕ Fin 7) (B : CommAlgCat R) (q : ↑(HopfAlgebra.points B)) : GeneralLinear.pointToGeneralLinear 56 ((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.E7Minuscule.generatedStandardComodule (R : Type u) [CommRing R] : Comodule R (↑(generatedCoordinateHopfAlgebra R)) (Fin 56 → R)

The standard right comodule of the generated type-E₇ minuscule subgroup on R⁵⁶.

Equations

• TauCeti.E7Minuscule.generatedStandardComodule R = TauCeti.GeneralLinear.corestrictStandardComodule R 56 (CommHopfAlgCat.Hom.hom (TauCeti.E7Minuscule.generatedCoordinateMap R))

theorem TauCeti.E7Minuscule.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.E7Minuscule.generatedRootSubgroupPoints_mulVec_mem (R : Type u) [CommRing R] (N : Subcomodule R (↑(generatedCoordinateHopfAlgebra R)) (Fin 56 → R)) (i : Fin 7 ⊕ Fin 7) (t : Multiplicative R) {w : Fin 56 → 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.E7Minuscule.generatedTorusCorestrict_eq_ofWeights (R : Type u) [CommRing R] : Comodule.Corestrict (CommHopfAlgCat.Hom.hom (generatedWeightTorusCoordinateMap R)).toCoalgHom = Comodule.ofWeights (Pi.basisFun R (Fin 56)) minusculeCharacter

Restricting the generated subgroup's standard comodule to the weight torus gives the direct sum of the 56 minuscule weight lines.

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

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