The standard representation of the type-E7 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-seven 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.E7Minuscule.standardComodule: its standard comodule on R⁵⁶.
• TauCeti.E7Minuscule.isFaithful_standardComodule: faithfulness of the standard comodule.
• TauCeti.E7Minuscule.specializedPointsMulEquiv: specialized coordinate-algebra points are identified with concrete carrier points.
• TauCeti.E7Minuscule.points_mulVec_mem: invariant submodules are stable under concrete carrier points.
• TauCeti.E7Minuscule.isSimpleOrder_of_minusculeWeights_of_rootSubgroupPoints: a comodule with the minuscule weight decomposition whose subcomodules are stable under the numbered root matrices is simple.
• TauCeti.E7Minuscule.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 VI.

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.

@[instance_reducible]

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

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

Equations

• TauCeti.E7Minuscule.standardComodule R = TauCeti.GeneralLinear.corestrictStandardComodule R 56 (CommHopfAlgCat.Hom.hom (TauCeti.E7Minuscule.coordinateMap R))

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

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

theorem TauCeti.E7Minuscule.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 56)) ∘ₗ Comodule.endOfPoint (Fin 56 → R) g.ofConv = ↑(Matrix.GeneralLinearGroup.toLin (GeneralLinear.pointToGeneralLinear 56 ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R 56) (baseChangeDefiningIdeal R) ↧A)) g))) ∘ₗ ↑(TensorProduct.piScalarRight R A A (Fin 56))

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

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

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

noncomputable def TauCeti.E7Minuscule.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.E7Minuscule.quotientPointsHom_specializedPointsMulEquiv_symm (R : Type u) [CommRing R] (g : ↥(points R)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R 56) (baseChangeDefiningIdeal R) ↧R)) ((specializedPointsMulEquiv R).symm g) = (GeneralLinear.pointsMulEquiv 56).symm ↑g

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

theorem TauCeti.E7Minuscule.points_mulVec_mem (R : Type u) [CommRing R] (N : Subcomodule R (↑(coordinateHopfAlgebra R)) (Fin 56 → R)) (g : ↥(points R)) {w : Fin 56 → 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.E7Minuscule.minusculeCharacter (a : Fin 56) : Multiplicative (Fin 7 →₀ ℤ)

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

Equations

• TauCeti.E7Minuscule.minusculeCharacter a = TauCeti.SplitTorus.weightCharacter (TauCeti.DynkinType.e7MinusculeWeight a)

theorem TauCeti.E7Minuscule.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 56 → k)] (f : H →ₗc[k] MonoidAlgebra k (Multiplicative (Fin 7 →₀ ℤ))) (hweights : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun k (Fin 56)) minusculeCharacter) (hroot : ∀ (N : Subcomodule k H (Fin 56 → k)) (i : Fin 7 ⊕ Fin 7), ∀ w ∈ N, (↑↑((rootSubgroupPoints i k) (Multiplicative.ofAdd 1))).mulVec w ∈ N) : IsSimpleOrder (Subcomodule k H (Fin 56 → 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.E7Minuscule.instIsSimpleOrderSubcomodule (k : Type u) [Field k] : IsSimpleOrder (Subcomodule k (↑(coordinateHopfAlgebra k)) (Fin 56 → k))

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