The two minuscule subcomodules of the doubled E₆ carrier

The standard representation of the doubled minuscule carrier is the corestriction of the standard O(GL₅₄)-comodule along its quotient coordinate morphism. It is faithful over every commutative ring. Its two coordinate blocks V(ϖ₁) and V(ϖ₆) are complementary subcomodules: the carrier preserves them scheme-theoretically, so this decomposition persists after arbitrary base change.

The parameter dual = false selects the first block, and dual = true the contragredient block. Membership means vanishing outside the selected block. Restriction to the weight torus identifies the fifty-four weight lines, and subcomodules are stable under concrete carrier points. These two constituents provide the block decomposition used to prove complete reducibility over fields in TauCeti.Algebra.Lie.E6.DoubledMinuscule.CompletelyReducible.

The carrier has not been identified with the pinned simply connected group scheme of type E₆. Transfer of these representations to that pinned group requires such an identification.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.1–2.
• R. W. Carter, Simple Groups of Lie Type, §12.2.
• The corestriction interface follows TauCeti.Algebra.Lie.E6.Minuscule.StandardComodule; the presented point identification follows the same module; the coordinate subcomodules follow TauCeti.Algebra.Lie.D4.Tripled.StandardComodule.

@[instance_reducible]

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

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

Equations

• TauCeti.E6DoubledMinuscule.standardComodule R = TauCeti.GeneralLinear.corestrictStandardComodule R 54 (CommHopfAlgCat.Hom.hom (TauCeti.E6DoubledMinuscule.coordinateMap R))

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

The standard representation of the doubled minuscule carrier is faithful over every commutative ring.

theorem TauCeti.E6DoubledMinuscule.coefficientMatrix_basisFun (R : Type u) [CommRing R] (a b : Fin 54) : Comodule.coefficientMatrix (Pi.basisFun R (Fin 54)) a b = (CommHopfAlgCat.Hom.hom (coordinateMap R)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R 54) ((GeneralLinear.coordinateRingMap R 54) (MvPolynomial.X (a, b))))

The coefficient matrix of the standard comodule consists of the ambient matrix coordinates mapped to the carrier's coordinate algebra. This explicit rewrite also applies when the comodule instance's body is hidden by the module boundary.

noncomputable def TauCeti.E6DoubledMinuscule.summandSubcomodule (R : Type u) [CommRing R] (dual : Bool) : Subcomodule R (↑(coordinateHopfAlgebra R)) (Fin 54 → R)

The minuscule (dual = false) or contragredient minuscule (dual = true) block as a subcomodule of the standard carrier comodule.

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.summandSubcomodule_toSubmodule (R : Type u) [CommRing R] (dual : Bool) : (summandSubcomodule R dual).toSubmodule = Submodule.span R (⇑(Pi.basisFun R (Fin 54)) '' {a : Fin 54 | matrixSummand a = if dual = true then 1 else 0})

Each summand subcomodule is the span of the corresponding coordinate basis vectors.

@[simp]

theorem TauCeti.E6DoubledMinuscule.mem_summandSubcomodule (R : Type u) [CommRing R] (dual : Bool) (v : Fin 54 → R) : v ∈ summandSubcomodule R dual ↔ ∀ (a : Fin 54), (matrixSummand a ≠ if dual = true then 1 else 0) → v a = 0

Membership in a minuscule summand means vanishing outside its coordinate block.

theorem TauCeti.E6DoubledMinuscule.isCompl_summandSubcomodule (R : Type u) [CommRing R] : IsCompl (summandSubcomodule R false).toSubmodule (summandSubcomodule R true).toSubmodule

The two minuscule summands are complementary over every commutative ring.

noncomputable def TauCeti.E6DoubledMinuscule.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.

@[simp]

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

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

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

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

@[reducible, inline]

noncomputable abbrev TauCeti.E6DoubledMinuscule.minusculeCharacter (a : Fin 54) : Multiplicative (Fin 6 →₀ ℤ)

The weight-torus character of a doubled minuscule coordinate.

Equations

• TauCeti.E6DoubledMinuscule.minusculeCharacter a = TauCeti.SplitTorus.weightCharacter (TauCeti.E6DoubledMinuscule.matrixWeight a)

theorem TauCeti.E6DoubledMinuscule.torusCorestrict_eq_ofWeights (R : Type u) [CommRing R] : Comodule.Corestrict (CommHopfAlgCat.Hom.hom (weightTorusToBaseChangeCoordinateMap R)).toCoalgHom = Comodule.ofWeights (Pi.basisFun R (Fin 54)) minusculeCharacter

Restriction of the standard comodule to the weight torus gives its fifty-four weight lines, over every commutative ring.