The standard representation of the type-E6 minuscule carrier

The full-weight type-E₆ minuscule carrier is a closed subgroup of GL₂₇. After base change to a commutative ring R, its standard representation is therefore the corestriction of the standard O(GL₂₇)-comodule along the quotient coordinate morphism.

This file proves that the resulting representation is faithful over every commutative ring and simple over every field. For simplicity, restriction to the rank-six weight torus separates a nonzero invariant vector into its one-dimensional weight components. The positive and negative simple-root elements then move a coordinate vector across the connected minuscule weight graph.

Main declarations

• TauCeti.E6Minuscule.standardComodule: its standard comodule on R²⁷.
• TauCeti.E6Minuscule.isFaithful_standardComodule: faithfulness of the standard comodule.
• TauCeti.E6Minuscule.specializedPointsMulEquiv: specialized coordinate-algebra points are identified with concrete carrier points.
• TauCeti.E6Minuscule.points_mulVec_mem: invariant submodules are stable under concrete carrier points.
• TauCeti.E6Minuscule.instIsSimpleOrderSubcomodule: simplicity over a field.

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 V.

The corestriction and point-action interface follows TauCeti.Algebra.AlgebraicGroup.GeneralLinear.StandardComodule and is adapted from TauCeti.Algebra.AlgebraicGroup.SpecialLinear.StandardComodule; the specialized point identification uses TauCeti.Algebra.AlgebraicGroup.GeneralLinear.HopfIdealPoints.BaseChange. The proof of simplicity follows the parallel type-E₇ construction in TauCeti.Algebra.Lie.E7.Minuscule.StandardComodule.

@[instance_reducible]

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

The standard right comodule of the specialized type-E₆ minuscule carrier.

Equations

• TauCeti.E6Minuscule.standardComodule R = TauCeti.GeneralLinear.corestrictStandardComodule R 27 (CommHopfAlgCat.Hom.hom (TauCeti.E6Minuscule.coordinateMap R))

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

The standard comodule of the specialized type-E₆ minuscule carrier is faithful.

theorem TauCeti.E6Minuscule.piScalarRight_comp_endOfPoint (R : Type u) [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R) →ₐ[R] A)) : ↑(TensorProduct.piScalarRight R A A (Fin 27)) ∘ₗ Comodule.endOfPoint (Fin 27 → R) g.ofConv = ↑(Matrix.GeneralLinearGroup.toLin (GeneralLinear.pointToGeneralLinear 27 ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R 27) (baseChangeDefiningIdeal R) ↧A)) g))) ∘ₗ ↑(TensorProduct.piScalarRight R A A (Fin 27))

Under scalar extension, a carrier-valued point acts on the standard comodule by the matrix obtained from its ambient GL₂₇ point.

theorem TauCeti.E6Minuscule.mulVec_mem (R : Type u) [CommRing R] (N : Subcomodule R (↑(coordinateHopfAlgebra R)) (Fin 27 → R)) (g : WithConv (↑(coordinateHopfAlgebra R) →ₐ[R] R)) {w : Fin 27 → R} (hw : w ∈ N) : (↑(GeneralLinear.pointToGeneralLinear 27 ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R 27) (baseChangeDefiningIdeal R) ↧R)) g))).mulVec w ∈ N

A subcomodule of the standard carrier comodule is stable under every carrier-valued point.

noncomputable def TauCeti.E6Minuscule.specializedPointsMulEquiv (R : Type u) [CommRing R] : ↑(HopfAlgebra.points ↧R) ≃* ↥(points R)

Base-valued points of the specialized coordinate algebra, identified with points of the integral minuscule carrier after base change.

Equations

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

theorem TauCeti.E6Minuscule.quotientPointsHom_specializedPointsMulEquiv_symm (R : Type u) [CommRing R] (g : ↥(points R)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R 27) (baseChangeDefiningIdeal R) ↧R)) ((specializedPointsMulEquiv R).symm g) = (GeneralLinear.pointsMulEquiv 27).symm ↑g

Under the specialized point equivalence, the quotient point is represented by the carrier point's ambient general-linear matrix.

theorem TauCeti.E6Minuscule.points_mulVec_mem (R : Type u) [CommRing R] (N : Subcomodule R (↑(coordinateHopfAlgebra R)) (Fin 27 → R)) (g : ↥(points R)) {w : Fin 27 → R} (hw : w ∈ N) : (↑↑g).mulVec w ∈ N

A subcomodule of the standard carrier comodule is stable under every concrete carrier point.

Simplicity over a field

@[reducible, inline]

noncomputable abbrev TauCeti.E6Minuscule.minusculeCharacter (a : Fin 27) : Multiplicative (Fin 6 →₀ ℤ)

The character of the weight torus corresponding to a minuscule-basis index.

Equations

• TauCeti.E6Minuscule.minusculeCharacter a = TauCeti.SplitTorus.weightCharacter (TauCeti.DynkinType.e6MinusculeWeight a)

theorem TauCeti.E6Minuscule.torusCorestrict_eq_ofWeights (k : Type u) [Field k] : have x := standardComodule k; Comodule.Corestrict (CommHopfAlgCat.Hom.hom (weightTorusToBaseChangeCoordinateMap k)).toCoalgHom = Comodule.ofWeights (Pi.basisFun k (Fin 27)) minusculeCharacter

Restricting the standard carrier comodule to the rank-six weight torus gives the direct sum of the 27 distinct minuscule weight comodules. Corestricting along weightTorusToBaseChangeCoordinateMap turns the standard comodule on Fin 27 → k into the comodule in which the coordinate basis vector at a spans the weight line of the torus character minusculeCharacter a.

theorem TauCeti.E6Minuscule.isSimpleOrder_of_minusculeWeights_of_rootSubgroupPoints (k : Type u) [Field k] {H : Type u_1} [AddCommGroup H] [Module k H] [Coalgebra k H] [Comodule k H (Fin 27 → k)] (f : H →ₗc[k] MonoidAlgebra k (Multiplicative (Fin 6 →₀ ℤ))) (hweights : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun k (Fin 27)) minusculeCharacter) (hroot : ∀ (N : Subcomodule k H (Fin 27 → k)) (i : Fin 6 ⊕ Fin 6), ∀ w ∈ N, (↑↑((rootSubgroupPoints i k) (Multiplicative.ofAdd 1))).mulVec w ∈ N) : IsSimpleOrder (Subcomodule k H (Fin 27 → k))

A comodule with the type-E₆ minuscule weight decomposition is simple if its subcomodules are stable under the numbered positive and negative minuscule root matrices at parameter one. This applies both to the integral carrier's specialization and to the subgroup generated directly over the field.

instance TauCeti.E6Minuscule.instIsSimpleOrderSubcomodule (k : Type u) [Field k] : IsSimpleOrder (Subcomodule k (↑(coordinateHopfAlgebra k)) (Fin 27 → k))

The standard comodule of the specialized type-E₆ minuscule carrier is simple over every field.