The standard representation of the tripled type-D4 carrier

The tripled type-D₄ carrier is a closed subgroup of GL₂₄, constructed from the direct sum of the vector and two half-spin eight-dimensional representations. After base change to a commutative ring R, its standard representation is 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. It also identifies the action of an algebra-valued point with multiplication by its ambient 24 × 24 matrix and deduces that subcomodules are stable under the concrete carrier points.

The tripled representation is designed to have three eight-dimensional constituents, and it is not simple. Instead, every union of the summands V(ϖ₁), V(ϖ₃) and V(ϖ₄) spans a subcomodule over every commutative ring, because the carrier lies in the block-diagonal subgroup of the summands. Over a field the representation is completely reducible. Restriction to the weight torus separates the twenty-four distinct weight lines, so a subcomodule is spanned by the coordinate vectors it contains. The positive and negative simple-root points move a coordinate vector to that of each reflected weight, and the simple reflections act transitively on each summand. Hence every subcomodule is the span of a union of summands, and the remaining summands span a complement.

Main declarations

• TauCeti.D4Tripled.standardComodule: the standard comodule on R²⁴.
• TauCeti.D4Tripled.isFaithful_standardComodule: faithfulness of the standard comodule.
• TauCeti.D4Tripled.piScalarRight_comp_endOfPoint: algebra-valued points act through their ambient matrices.
• TauCeti.D4Tripled.points_mulVec_mem: invariant submodules are stable under concrete carrier points.
• TauCeti.D4Tripled.summandSubcomodule: the subcomodule spanned by a union of summands.
• TauCeti.D4Tripled.torusCorestrict_eq_ofWeights: the weight decomposition under the weight torus, over every commutative ring.
• TauCeti.D4Tripled.isCompletelyReducible_standardComodule: complete reducibility 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 IV.

The corestriction and point-action interface follows TauCeti.Algebra.AlgebraicGroup.GeneralLinear.StandardComodule; the organization is adapted from TauCeti.Algebra.Lie.E7.Minuscule.StandardComodule. The weight-line and reflection steps follow the simplicity proof in TauCeti.Algebra.Lie.E6.Minuscule.StandardComodule, and the complement construction follows TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Weight.Levi.StandardComodule.

@[instance_reducible]

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

The standard right comodule of the specialized tripled type-D₄ carrier.

Equations

• TauCeti.D4Tripled.standardComodule R = TauCeti.GeneralLinear.corestrictStandardComodule R 24 (CommHopfAlgCat.Hom.hom (TauCeti.D4Tripled.coordinateMap R))

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

The standard comodule of the specialized tripled type-D₄ carrier is faithful.

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

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

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

A subcomodule of the standard carrier comodule is stable under every coordinate-algebra point over the base ring.

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

A subcomodule of the standard carrier comodule is stable under every concrete tripled type-D₄ carrier point.

The summand subcomodules

noncomputable def TauCeti.D4Tripled.summandSubcomodule (R : Type u) [CommRing R] (s : Set (Fin 24)) (hs : ∀ (a b : Fin 24), DynkinType.d4TripledSummand a = DynkinType.d4TripledSummand b → b ∈ s → a ∈ s) : Subcomodule R (↑(coordinateHopfAlgebra R)) (Fin 24 → R)

A union of summands spans a subcomodule of the standard carrier comodule, over every commutative ring: the carrier preserves each of V(ϖ₁), V(ϖ₃) and V(ϖ₄).

Equations

• TauCeti.D4Tripled.summandSubcomodule R s hs = (Pi.basisFun R (Fin 24)).coordinateSpanSubcomodule s ⋯

@[simp]

theorem TauCeti.D4Tripled.summandSubcomodule_toSubmodule (R : Type u) [CommRing R] (s : Set (Fin 24)) (hs : ∀ (a b : Fin 24), DynkinType.d4TripledSummand a = DynkinType.d4TripledSummand b → b ∈ s → a ∈ s) : (summandSubcomodule R s hs).toSubmodule = Submodule.span R (⇑(Pi.basisFun R (Fin 24)) '' s)

A summand subcomodule is the span of the coordinate vectors of its summands.

@[simp]

theorem TauCeti.D4Tripled.mem_summandSubcomodule (R : Type u) [CommRing R] (s : Set (Fin 24)) (hs : ∀ (a b : Fin 24), DynkinType.d4TripledSummand a = DynkinType.d4TripledSummand b → b ∈ s → a ∈ s) (v : Fin 24 → R) : v ∈ summandSubcomodule R s hs ↔ ∀ a ∉ s, v a = 0

Membership in a summand subcomodule means vanishing outside the chosen summands.

The weight decomposition under the weight torus

@[reducible, inline]

noncomputable abbrev TauCeti.D4Tripled.tripledCharacter (a : Fin 24) : Multiplicative (Fin 4 →₀ ℤ)

The character of the weight torus on the coordinate vector at a tripled weight index.

Equations

• TauCeti.D4Tripled.tripledCharacter a = Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm (TauCeti.DynkinType.d4TripledWeight a))

theorem TauCeti.D4Tripled.torusCorestrict_eq_ofWeights (R : Type u) [CommRing R] : have x := standardComodule R; Comodule.Corestrict (CommHopfAlgCat.Hom.hom (weightTorusToBaseChangeCoordinateMap R)).toCoalgHom = Comodule.ofWeights (Pi.basisFun R (Fin 24)) tripledCharacter

Restricting the standard carrier comodule to the rank-four weight torus gives the direct sum of the twenty-four distinct tripled weight comodules. The coordinate vector at a spans the weight line of the torus character tripledCharacter a, over every commutative ring.

Complete reducibility over a field

theorem TauCeti.D4Tripled.isCompletelyReducible_standardComodule (k : Type u) [Field k] : Comodule.IsCompletelyReducible k (↑(coordinateHopfAlgebra k)) (Fin 24 → k)

The standard comodule of the specialized tripled type-D₄ carrier is completely reducible over every field. Every subcomodule is the span of a union of the three summands, and the remaining summands span a complementary subcomodule.