The graph automorphism of the doubled type-E6 minuscule carrier

The nontrivial symmetry of the Bourbaki-numbered E₆ diagram exchanges the two minuscule representations V(ϖ₁) and V(ϖ₆). On their direct sum it has a signed monomial lift which intertwines the represented positive and negative simple-root generators. This file constructs that lift and descends it to the full-weight doubled minuscule carrier.

The resulting automorphism TauCeti.E6DoubledMinuscule.graphAutomorphism carries each numbered root subgroup to the subgroup numbered by TauCeti.DynkinType.graphPermE6, without changing its additive parameter, and relabels the represented split torus by the same diagram involution. It has order dividing two, and it is the only endomorphism of the carrier with that action on the numbered root subgroups, which generate it.

No reductivity, maximality of the represented torus, or identification of the carrier's root datum is asserted here.

Main declarations

• TauCeti.E6DoubledMinuscule.graphRootPerm: the diagram involution on the positive and negative simple-root indices.
• TauCeti.E6DoubledMinuscule.graphModuleEquiv: its signed monomial lift to the doubled minuscule module.
• TauCeti.E6DoubledMinuscule.graphAutomorphism: the induced automorphism of the doubled carrier.
• TauCeti.E6DoubledMinuscule.rootSubgroup_comp_graphAutomorphism_hom: its action on the numbered simple-root subgroups.
• TauCeti.E6DoubledMinuscule.eq_graphAutomorphism_hom_of_rootSubgroup and TauCeti.E6DoubledMinuscule.eq_graphAutomorphism_of_rootSubgroup: that action determines it, among endomorphisms and among automorphisms of the carrier.
• TauCeti.E6DoubledMinuscule.weightTorus_comp_graphAutomorphism_hom: its action on the split weight torus.
• TauCeti.E6DoubledMinuscule.graphAutomorphism_hom_comp_self and TauCeti.E6DoubledMinuscule.graphAutomorphism_inv: its order-two relation on the carrier.
• TauCeti.E6DoubledMinuscule.graphAutomorphismPoints: the same automorphism on matrix-valued points.
• TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_rootSubgroupPoints and TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_weightTorusPoints: its pointwise equations on the numbered simple-root subgroups and represented weight torus.
• TauCeti.E6DoubledMinuscule.map_comp_graphAutomorphismPoints: its naturality in the value ring, which makes it commute with Frobenius.
• TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_sq: its pointwise order-two relation.
• TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_graphAutomorphismPoints: the corresponding simp-normal pointwise involution.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V.
• 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 signed symmetry of the doubled module

def TauCeti.E6DoubledMinuscule.graphRootPerm : Equiv.Perm (Fin 6 ⊕ Fin 6)

The type-E₆ diagram involution on both the positive and negative simple-root indices.

Equations

• TauCeti.E6DoubledMinuscule.graphRootPerm = Equiv.sumCongr TauCeti.graphPermE6 TauCeti.graphPermE6

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphRootPerm_inl (i : Fin 6) : graphRootPerm (Sum.inl i) = Sum.inl (graphPermE6 i)

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphRootPerm_inr (i : Fin 6) : graphRootPerm (Sum.inr i) = Sum.inr (graphPermE6 i)

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphRootPerm_graphRootPerm (k : Fin 6 ⊕ Fin 6) : graphRootPerm (graphRootPerm k) = k

def TauCeti.E6DoubledMinuscule.basisSign (a : Fin 27 ⊕ Fin 27) : ℤ

The sign of a doubled minuscule basis vector, given by parity of its weight height.

Equations

• TauCeti.E6DoubledMinuscule.basisSign a = ↑(TauCeti.E6DoubledMinuscule.basisHeight✝ a).negOnePow

@[simp]

theorem TauCeti.E6DoubledMinuscule.basisSign_sq (a : Fin 27 ⊕ Fin 27) : basisSign a * basisSign a = 1

@[simp]

theorem TauCeti.E6DoubledMinuscule.basisSign_graphPerm (a : Fin 27 ⊕ Fin 27) : basisSign (DynkinType.e6DoubledMinusculeGraphPerm a) = basisSign a

def TauCeti.E6DoubledMinuscule.graphModuleEquiv : (Fin 27 ⊕ Fin 27 → ℚ) ≃ₗ[ℚ] Fin 27 ⊕ Fin 27 → ℚ

The signed monomial lift of the type-E₆ diagram involution to V(ϖ₁) ⊕ V(ϖ₆).

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphModuleEquiv_apply (v : Fin 27 ⊕ Fin 27 → ℚ) (a : Fin 27 ⊕ Fin 27) : graphModuleEquiv v a = ↑(basisSign a) * v (DynkinType.e6DoubledMinusculeGraphPerm a)

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphModuleEquiv_apply_apply (v : Fin 27 ⊕ Fin 27 → ℚ) : graphModuleEquiv (graphModuleEquiv v) = v

theorem TauCeti.E6DoubledMinuscule.graphModuleEquiv_mem_lattice_iff (v : Fin 27 ⊕ Fin 27 → ℚ) : graphModuleEquiv v ∈ lattice ↔ v ∈ lattice

The signed graph symmetry preserves the integral coordinate lattice.

def TauCeti.E6DoubledMinuscule.graphMatrixPerm : Equiv.Perm (Fin 54)

The coordinate permutation of the signed graph symmetry in the Fin 54 matrix basis.

Equations

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

def TauCeti.E6DoubledMinuscule.graphMatrixScale (i : Fin 54) : ℤ

The integral scale of the signed graph symmetry in the Fin 54 matrix basis.

Equations

• TauCeti.E6DoubledMinuscule.graphMatrixScale i = TauCeti.E6DoubledMinuscule.basisSign (TauCeti.E6DoubledMinuscule.matrixIndexEquiv.symm i)

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphMatrixPerm_apply_apply (i : Fin 54) : graphMatrixPerm (graphMatrixPerm i) = i

theorem TauCeti.E6DoubledMinuscule.graphModuleEquiv_matrixBasis (i : Fin 54) : graphModuleEquiv ↑(matrixBasis i) = ↑(graphMatrixScale i • matrixBasis (graphMatrixPerm i))

The signed graph symmetry acts monomially on the matrix-coordinate lattice basis.

@[simp]

theorem TauCeti.E6DoubledMinuscule.matrixWeight_graphMatrixPerm (i : Fin 54) (k : Fin 6) : matrixWeight (graphMatrixPerm i) (graphPermE6 k) = matrixWeight i k

The coordinate permutation of the signed graph symmetry relabels the matrix weights by the type-E₆ diagram involution.

The graph automorphism of the carrier

noncomputable def TauCeti.E6DoubledMinuscule.graphAutomorphism : CategoryTheory.Aut groupScheme

The graph automorphism of the doubled type-E₆ minuscule carrier, characterized on the numbered simple-root subgroups and represented weight torus.

Equations

• TauCeti.E6DoubledMinuscule.graphAutomorphism = TauCeti.E6DoubledMinuscule.toralGraphAutomorphism✝

@[simp]

theorem TauCeti.E6DoubledMinuscule.rootSubgroup_comp_graphAutomorphism_hom (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) graphAutomorphism.hom = rootSubgroup (graphRootPerm k)

The graph automorphism renumbers each positive and negative numbered simple-root subgroup by the type-E₆ diagram involution, without changing its additive parameter.

@[simp]

theorem TauCeti.E6DoubledMinuscule.rootSubgroup_comp_graphAutomorphism_hom_assoc (k : Fin 6 ⊕ Fin 6) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 54) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) (CategoryTheory.CategoryStruct.comp graphAutomorphism.hom h) = CategoryTheory.CategoryStruct.comp (rootSubgroup (graphRootPerm k)) h

The graph automorphism renumbers each positive and negative numbered simple-root subgroup by the type-E₆ diagram involution, without changing its additive parameter.

theorem TauCeti.E6DoubledMinuscule.eq_graphAutomorphism_hom_of_rootSubgroup (φ : groupScheme ⟶ groupScheme) (hroot : ∀ (k : Fin 6 ⊕ Fin 6), CategoryTheory.CategoryStruct.comp (rootSubgroup k) φ = rootSubgroup (graphRootPerm k)) : φ = graphAutomorphism.hom

The type-E₆ diagram involution has exactly one realization on the carrier. An endomorphism of the carrier carrying each numbered simple-root subgroup to the one at the image node, with the same additive parameter, is the graph 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.E6DoubledMinuscule.eq_graphAutomorphism_of_rootSubgroup (γ : CategoryTheory.Aut groupScheme) (hroot : ∀ (k : Fin 6 ⊕ Fin 6), CategoryTheory.CategoryStruct.comp (rootSubgroup k) γ.hom = rootSubgroup (graphRootPerm k)) : γ = graphAutomorphism

The graph automorphism is the unique automorphism of the carrier realizing the type-E₆ diagram involution on the numbered simple-root subgroups.

@[simp]

theorem TauCeti.E6DoubledMinuscule.weightTorus_comp_graphAutomorphism_hom : CategoryTheory.CategoryStruct.comp weightTorus graphAutomorphism.hom = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ graphPermE6) weightTorus

The graph automorphism relabels the represented split weight torus by the type-E₆ diagram involution.

@[simp]

theorem TauCeti.E6DoubledMinuscule.weightTorus_comp_graphAutomorphism_hom_assoc {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 54) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp weightTorus (CategoryTheory.CategoryStruct.comp graphAutomorphism.hom h) = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ graphPermE6) (CategoryTheory.CategoryStruct.comp weightTorus h)

The graph automorphism relabels the represented split weight torus by the type-E₆ diagram involution.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphism_sq : graphAutomorphism ^ 2 = 1

The graph automorphism is an involution.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphism_hom_comp_self : CategoryTheory.CategoryStruct.comp graphAutomorphism.hom graphAutomorphism.hom = CategoryTheory.CategoryStruct.id groupScheme

Applying the graph automorphism twice is the identity on the doubled type-E₆ carrier.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphism_hom_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 ℤ 54) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp graphAutomorphism.hom (CategoryTheory.CategoryStruct.comp graphAutomorphism.hom h) = h

Applying the graph automorphism twice is the identity on the doubled type-E₆ carrier.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphism_inv : graphAutomorphism.inv = graphAutomorphism.hom

The inverse leg of the doubled type-E₆ graph automorphism is its forward leg.

The graph automorphism on matrix-valued points

noncomputable def TauCeti.E6DoubledMinuscule.graphAutomorphismMatrix (A : Type v) [CommRing A] : GL (Fin 54) A

The signed monomial matrix inducing the graph automorphism on points.

Equations

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

theorem TauCeti.E6DoubledMinuscule.coe_graphAutomorphismMatrix_apply (A : Type v) [CommRing A] (i j : Fin 54) : ↑(graphAutomorphismMatrix A) i j = if i = graphMatrixPerm j then (algebraMap ℤ A) (graphMatrixScale j) else 0

The graph-automorphism matrix has the signed monomial entry formula determined by graphMatrixPerm and graphMatrixScale.

@[simp]

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

The graph-automorphism matrix commutes with extension of the value ring.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphismMatrix_sq (A : Type v) [CommRing A] : graphAutomorphismMatrix A ^ 2 = 1

The signed graph-automorphism matrix is an involution over every commutative ring.

theorem TauCeti.E6DoubledMinuscule.map_points_conj_graphAutomorphismMatrix (A : Type v) [CommRing A] : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (graphAutomorphismMatrix A))) (points A) = points A

Conjugation by the signed graph-automorphism matrix preserves the doubled carrier's point subgroup.

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

The graph automorphism on matrix-valued points of the doubled carrier, given by conjugation by its signed monomial matrix.

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.coe_graphAutomorphismPoints (A : Type v) [CommRing A] (g : ↥(points A)) : ↑((graphAutomorphismPoints A) g) = graphAutomorphismMatrix A * ↑g * (graphAutomorphismMatrix A)⁻¹

On matrices, the graph automorphism of points is conjugation by its signed monomial matrix.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_rootSubgroupPoints (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) (u : Multiplicative A) : (graphAutomorphismPoints A) ((rootSubgroupPoints k A) u) = (rootSubgroupPoints (graphRootPerm k) A) u

The graph automorphism on points renumbers every numbered positive and negative simple-root subgroup without changing its additive parameter.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_weightTorusPoints (A : Type v) [CommRing A] (s : Fin 6 → Aˣ) : (graphAutomorphismPoints A) ((weightTorusPoints A) s) = (weightTorusPoints A) fun (k : Fin 6) => s (graphPermE6 k)

The graph automorphism relabels the coordinates of a represented split-torus point by the type-E₆ diagram involution.

theorem TauCeti.E6DoubledMinuscule.schemePointsMulEquiv_graphAutomorphism_comp_carrierι (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ groupScheme.X) : (GeneralLinear.schemePointsMulEquiv 54 A) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp graphAutomorphism.hom carrierι).hom.hom) = graphAutomorphismMatrix A * (GeneralLinear.schemePointsMulEquiv 54 A) (CategoryTheory.CategoryStruct.comp p carrierι.hom.hom) * (graphAutomorphismMatrix A)⁻¹

The automorphism on matrix-valued points is the map induced by the carrier automorphism. After inclusion into GL₅₄, composing a scheme-valued point with graphAutomorphism is conjugation by graphAutomorphismMatrix.

theorem TauCeti.E6DoubledMinuscule.map_comp_graphAutomorphismPoints {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) : ((pointsPresentation A).map (pointsPresentation B) f).comp (MulEquiv.toMonoidHom (graphAutomorphismPoints A)) = (MulEquiv.toMonoidHom (graphAutomorphismPoints B)).comp ((pointsPresentation A).map (pointsPresentation B) f)

The graph automorphism on points is natural in the value ring. In particular, it commutes with every iterated Frobenius map.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_sq (A : Type v) [CommRing A] : graphAutomorphismPoints A ^ 2 = 1

The graph automorphism on matrix-valued points is an involution.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_graphAutomorphismPoints (A : Type v) [CommRing A] (g : ↥(points A)) : (graphAutomorphismPoints A) ((graphAutomorphismPoints A) g) = g

Applying the graph automorphism twice to a matrix-valued point is the identity.

@[simp]

theorem TauCeti.E6DoubledMinuscule.graphAutomorphismPoints_symm (A : Type v) [CommRing A] : MulEquiv.symm (graphAutomorphismPoints A) = graphAutomorphismPoints A

The graph automorphism on matrix-valued points is its own inverse.