Triality on the tripled type-D4 carrier

The order-three symmetry of the Bourbaki-numbered D₄ diagram, TauCeti.trialityPermD4, fixes the central node and cycles the three outer nodes, and with them the three eight-dimensional representations V(ϖ₁), V(ϖ₃) and V(ϖ₄). On the tripled weight table it is the symmetry TauCeti.D4Tripled.trialitySymmetry, and on the rational tripled module the coordinate permutation TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv of that symmetry intertwines the represented positive and negative simple-root generators. Every nonzero entry of a raising or lowering matrix on the tripled weight basis is 1, so no signs are needed: the lift permutes the lattice basis with every scaling coefficient equal to one. This file descends that lift to the tripled carrier through the numbered-symmetry construction on Kostant toral closures.

The resulting automorphism TauCeti.D4Tripled.trialityAutomorphism carries each numbered root subgroup to the subgroup numbered by triality, without changing its additive parameter, and carries the represented split torus to itself, relabelling its coordinates by the inverse of the diagram permutation: weightTorus ≫ γ.hom = relabel σ⁻¹ ≫ weightTorus, a distinction that matters for a permutation of order three. It has order dividing three. On matrix-valued points it is conjugation by the permutation matrix of TauCeti.DynkinType.d4TripledTrialityPerm, and that matrix is compatible with every change of value ring. The action on the numbered root subgroups already determines it, since those subgroups generate the carrier.

No reductivity, maximality of the represented torus, or identification of the carrier with the pinned simply connected group scheme of type D₄ is asserted here.

Main declarations

• TauCeti.D4Tripled.trialityAutomorphism: the triality automorphism of the tripled carrier.
• TauCeti.D4Tripled.rootSubgroup_comp_trialityAutomorphism_hom: its action on the numbered simple-root subgroups, γ ∘ x_k = x_{σ k}.
• TauCeti.D4Tripled.eq_trialityAutomorphism_hom_of_rootSubgroup and TauCeti.D4Tripled.eq_trialityAutomorphism_of_rootSubgroup: that action determines it, among endomorphisms and among automorphisms of the carrier.
• TauCeti.D4Tripled.weightTorus_comp_trialityAutomorphism_hom: its action on the split weight torus.
• TauCeti.D4Tripled.trialityAutomorphism_pow_three, TauCeti.D4Tripled.trialityAutomorphism_hom_comp_self_comp_self and TauCeti.D4Tripled.trialityAutomorphism_inv: its order-three relation on the carrier.
• TauCeti.D4Tripled.trialityMatrix: the permutation matrix inducing triality on points, with TauCeti.D4Tripled.map_trialityMatrix its compatibility with ring homomorphisms.
• TauCeti.D4Tripled.trialityPoints: the same automorphism on matrix-valued points.
• TauCeti.D4Tripled.trialityPoints_rootSubgroupPoints and TauCeti.D4Tripled.trialityPoints_weightTorusPoints: its pointwise equations on the numbered simple-root subgroups and the represented weight torus.
• TauCeti.D4Tripled.schemePointsMulEquiv_trialityAutomorphism_comp_carrierι: the action on scheme-valued points is conjugation by trialityMatrix.
• TauCeti.D4Tripled.trialityPoints_pow_three and TauCeti.D4Tripled.trialityPoints_symm_apply: its pointwise order-three relation.
• TauCeti.D4Tripled.pointsMap_comp_trialityPoints: its naturality in the value ring, and so its commutation with every Frobenius map.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15.
• R. W. Carter, Simple Groups of Lie Type, §12.2.
• The construction follows the formal template of TauCeti.Algebra.Lie.E6.DoubledMinuscule.GraphAutomorphism, with the signed involution there replaced by an unsigned permutation of order three.
• K. Morrison and Claude Code, Tau Ceti PR #6671, whose scheme-level automorphism, point action, and order-three proofs are adapted here to the current generic symmetry API.

The inputs of the numbered-symmetry construction

The triality automorphism of the carrier

noncomputable def TauCeti.D4Tripled.trialityAutomorphism : CategoryTheory.Aut groupScheme

The triality automorphism of the tripled type-D₄ carrier, characterized on the numbered simple-root subgroups by rootSubgroup_comp_trialityAutomorphism_hom and on the represented weight torus by weightTorus_comp_trialityAutomorphism_hom.

Equations

• TauCeti.D4Tripled.trialityAutomorphism = TauCeti.D4Tripled.toralTrialityAutomorphism✝

@[simp]

theorem TauCeti.D4Tripled.rootSubgroup_comp_trialityAutomorphism_hom (k : Fin 4 ⊕ Fin 4) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) trialityAutomorphism.hom = rootSubgroup (trialitySymmetry.rootPerm k)

The triality automorphism renumbers each positive and negative numbered simple-root subgroup by triality, without changing its additive parameter: γ ∘ x_k = x_{σ k}.

@[simp]

theorem TauCeti.D4Tripled.rootSubgroup_comp_trialityAutomorphism_hom_assoc (k : Fin 4 ⊕ Fin 4) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) (CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom h) = CategoryTheory.CategoryStruct.comp (rootSubgroup (trialitySymmetry.rootPerm k)) h

The triality automorphism renumbers each positive and negative numbered simple-root subgroup by triality, without changing its additive parameter: γ ∘ x_k = x_{σ k}.

theorem TauCeti.D4Tripled.eq_trialityAutomorphism_hom_of_rootSubgroup (φ : groupScheme ⟶ groupScheme) (hroot : ∀ (k : Fin 4 ⊕ Fin 4), CategoryTheory.CategoryStruct.comp (rootSubgroup k) φ = rootSubgroup (trialitySymmetry.rootPerm k)) : φ = trialityAutomorphism.hom

Triality has exactly one realization on the carrier. An endomorphism of the carrier carrying each numbered simple-root subgroup to the one at the triality image of its node, with the same additive parameter, is the triality automorphism. The numbered root subgroups generate the carrier, so these equations leave nothing free; in particular no condition on the represented weight torus is needed.

theorem TauCeti.D4Tripled.eq_trialityAutomorphism_of_rootSubgroup (γ : CategoryTheory.Aut groupScheme) (hroot : ∀ (k : Fin 4 ⊕ Fin 4), CategoryTheory.CategoryStruct.comp (rootSubgroup k) γ.hom = rootSubgroup (trialitySymmetry.rootPerm k)) : γ = trialityAutomorphism

The triality automorphism is the unique automorphism of the carrier realizing the three-cycle of the outer D₄ nodes on the numbered simple-root subgroups.

@[simp]

theorem TauCeti.D4Tripled.weightTorus_comp_trialityAutomorphism_hom : CategoryTheory.CategoryStruct.comp weightTorus trialityAutomorphism.hom = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ trialityPermD4⁻¹) weightTorus

The triality automorphism relabels the represented split weight torus by the inverse of the diagram permutation.

@[simp]

theorem TauCeti.D4Tripled.weightTorus_comp_trialityAutomorphism_hom_assoc {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp weightTorus (CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom h) = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ trialityPermD4⁻¹) (CategoryTheory.CategoryStruct.comp weightTorus h)

The triality automorphism relabels the represented split weight torus by the inverse of the diagram permutation.

@[simp]

theorem TauCeti.D4Tripled.trialityAutomorphism_pow_three : trialityAutomorphism ^ 3 = 1

The triality automorphism has order dividing three.

@[simp]

theorem TauCeti.D4Tripled.trialityAutomorphism_hom_comp_self_comp_self : CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom (CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom trialityAutomorphism.hom) = CategoryTheory.CategoryStruct.id groupScheme

Applying the triality automorphism three times is the identity on the tripled carrier.

@[simp]

theorem TauCeti.D4Tripled.trialityAutomorphism_hom_comp_self_comp_self_assoc {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom (CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom (CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom h)) = h

Applying the triality automorphism three times is the identity on the tripled carrier.

@[simp]

theorem TauCeti.D4Tripled.trialityAutomorphism_inv : trialityAutomorphism.inv = CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom trialityAutomorphism.hom

The inverse leg of the triality automorphism is the square of its forward leg.

Triality on matrix-valued points

noncomputable def TauCeti.D4Tripled.trialityMatrix (A : Type v) [CommRing A] : GL (Fin 24) A

The permutation matrix inducing triality on matrix-valued points.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.coe_trialityMatrix_apply (A : Type v) [CommRing A] (i j : Fin 24) : ↑(trialityMatrix A) i j = if i = DynkinType.d4TripledTrialityPerm j then 1 else 0

The triality matrix is the permutation matrix of d4TripledTrialityPerm.

@[simp]

theorem TauCeti.D4Tripled.map_trialityMatrix {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) : (Matrix.GeneralLinearGroup.map f) (trialityMatrix A) = trialityMatrix B

The triality matrix is compatible with every ring homomorphism of value rings.

@[simp]

theorem TauCeti.D4Tripled.trialityMatrix_pow_three (A : Type v) [CommRing A] : trialityMatrix A ^ 3 = 1

The triality matrix has order dividing three over every commutative ring.

noncomputable def TauCeti.D4Tripled.trialityPoints (A : Type v) [CommRing A] : MulAut ↥(points A)

Triality on matrix-valued points of the tripled carrier, given by conjugation by the triality permutation matrix.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.coe_trialityPoints (A : Type v) [CommRing A] (g : ↥(points A)) : ↑((trialityPoints A) g) = trialityMatrix A * ↑g * (trialityMatrix A)⁻¹

On matrices, triality on points is conjugation by the triality matrix.

theorem TauCeti.D4Tripled.coe_trialityPoints_symm (A : Type v) [CommRing A] (g : ↥(points A)) : ↑((MulEquiv.symm (trialityPoints A)) g) = (trialityMatrix A)⁻¹ * ↑g * trialityMatrix A

On matrices, the inverse of triality on points is conjugation by the inverse of the triality matrix.

@[simp]

theorem TauCeti.D4Tripled.trialityPoints_rootSubgroupPoints (A : Type v) [CommRing A] (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) : (trialityPoints A) ((rootSubgroupPoints k A) u) = (rootSubgroupPoints (trialitySymmetry.rootPerm k) A) u

Triality on points renumbers every numbered positive and negative simple-root subgroup without changing its additive parameter: γ (x_k(u)) = x_{σ k}(u).

@[simp]

theorem TauCeti.D4Tripled.trialityPoints_weightTorusPoints (A : Type v) [CommRing A] (s : Fin 4 → Aˣ) : (trialityPoints A) ((weightTorusPoints A) s) = (weightTorusPoints A) fun (k : Fin 4) => s ((Equiv.symm trialityPermD4) k)

Triality on points relabels the coordinates of a represented split-torus point by the inverse of the diagram permutation.

theorem TauCeti.D4Tripled.schemePointsMulEquiv_trialityAutomorphism_comp_carrierι (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ groupScheme.X) : (GeneralLinear.schemePointsMulEquiv 24 A) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp trialityAutomorphism.hom carrierι).hom.hom) = trialityMatrix A * (GeneralLinear.schemePointsMulEquiv 24 A) (CategoryTheory.CategoryStruct.comp p carrierι.hom.hom) * (trialityMatrix A)⁻¹

Triality on matrix-valued points is the map induced by the carrier automorphism. After inclusion into GL₂₄, composing a scheme-valued point with trialityAutomorphism is conjugation by trialityMatrix.

theorem TauCeti.D4Tripled.pointsMap_comp_trialityPoints {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) : (pointsMap f).comp (MulEquiv.toMonoidHom (trialityPoints A)) = (MulEquiv.toMonoidHom (trialityPoints B)).comp (pointsMap f)

Triality on matrix-valued points is natural in the value ring: it commutes with the map on points induced by any ring homomorphism, in particular with every Frobenius map of the carrier.

@[simp]

theorem TauCeti.D4Tripled.trialityPoints_pow_three (A : Type v) [CommRing A] : trialityPoints A ^ 3 = 1

Triality on matrix-valued points has order dividing three.

@[simp]

theorem TauCeti.D4Tripled.trialityPoints_trialityPoints_trialityPoints (A : Type v) [CommRing A] (g : ↥(points A)) : (trialityPoints A) ((trialityPoints A) ((trialityPoints A) g)) = g

Applying triality three times to a matrix-valued point is the identity.

@[simp]

theorem TauCeti.D4Tripled.trialityPoints_symm_apply (A : Type v) [CommRing A] (g : ↥(points A)) : (MulEquiv.symm (trialityPoints A)) g = (trialityPoints A) ((trialityPoints A) g)

The inverse of triality on matrix-valued points is the square of triality, its order dividing three.