The pinned graph automorphism of the type-A standard carrier

The signed reverse-inverse-transpose automorphism of GL_{r+1} preserves the full-weight type-A_r Chevalley carrier. This file descends it to an automorphism of TauCeti.SlStd.groupScheme r. On the chosen pinning it reverses the Bourbaki numbering without changing root-subgroup parameters, and on the split torus it reverses the coordinates.

The proof first recovers the ambient coordinate Hopf-algebra automorphism from its natural action on matrix points. The root subgroups are permuted among themselves and the weight torus is carried to itself up to relabelling, so the largest Hopf ideal killed by all those coordinate maps is invariant. The automorphism therefore descends to the quotient.

Main declarations

• TauCeti.SlStd.graphRootPerm: reversal on the positive and negative simple-root indices.
• TauCeti.SlStd.graphAutomorphism: the pinned graph automorphism of the standard carrier.
• TauCeti.SlStd.graphAutomorphismPoints: its induced automorphism on algebra-valued matrix points.
• TauCeti.SlStd.generalLinearSchemePointsMulEquiv_graphAutomorphism_comp_carrierι: its signed reverse-inverse-transpose formula on arbitrary carrier points.
• TauCeti.SlStd.graphAutomorphism_hom_comp_self and TauCeti.SlStd.graphAutomorphismPoints_graphAutomorphismPoints: its involutivity, on the carrier and on points.
• TauCeti.SlStd.rootSubgroup_comp_graphAutomorphism_hom: its action on root subgroups.
• TauCeti.SlStd.eq_graphAutomorphism_hom_of_rootSubgroup and TauCeti.SlStd.eq_graphAutomorphism_of_rootSubgroup: that action determines it, among endomorphisms and among automorphisms of the carrier.
• TauCeti.SlStd.weightTorus_comp_graphAutomorphism_hom: its action on the split torus.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15.
• R. Steinberg, Lectures on Chevalley Groups, §10.

This advances the Pinnings and Chevalley--Demazure construction targets in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. It supplies the graph part of the Steinberg map needed by milestone L1 of TauCetiRoadmap/CFSGStatement/README.md for the twisted family ²A_r(q).

def TauCeti.SlStd.graphRootPerm (r : ℕ) : Equiv.Perm (Fin r ⊕ Fin r)

Reversal of the Bourbaki node on both the positive and negative simple-root indices.

Equations

• TauCeti.SlStd.graphRootPerm r = Equiv.sumCongr Fin.revPerm Fin.revPerm

@[simp]

theorem TauCeti.SlStd.graphRootPerm_inl (r : ℕ) (i : Fin r) : (graphRootPerm r) (Sum.inl i) = Sum.inl i.rev

@[simp]

theorem TauCeti.SlStd.graphRootPerm_inr (r : ℕ) (i : Fin r) : (graphRootPerm r) (Sum.inr i) = Sum.inr i.rev

@[simp]

theorem TauCeti.SlStd.graphRootPerm_graphRootPerm (r : ℕ) (k : Fin r ⊕ Fin r) : (graphRootPerm r) ((graphRootPerm r) k) = k

Descent to the standard carrier

noncomputable def TauCeti.SlStd.graphAutomorphism (r : ℕ) : CategoryTheory.Aut (groupScheme r)

The pinned graph automorphism of the full-weight type-A_r standard carrier.

Equations

• TauCeti.SlStd.graphAutomorphism r = (AlgebraicGeometry.hopfSpec ↧ℤ).mapIso (TauCeti.SlStd.graphCoordinateIso✝ r).op

theorem TauCeti.SlStd.generalLinearSchemePointsMulEquiv_graphAutomorphism_comp_carrierι (r : ℕ) {A : Type} [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (groupScheme r).X) : (GeneralLinear.schemePointsMulEquiv (r + 1) A) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (graphAutomorphism r).hom.hom.hom (carrierι r).hom.hom)) = (typeAGraphAutomorphism r A) ((GeneralLinear.schemePointsMulEquiv (r + 1) A) (CategoryTheory.CategoryStruct.comp p (carrierι r).hom.hom))

On every algebra-valued carrier point, the graph automorphism is signed reverse-inverse-transpose after the canonical inclusion into GL_{r+1}.

theorem TauCeti.SlStd.typeAGraphAutomorphism_mem_points (r : ℕ) {A : Type} [CommRing A] (g : GL (Fin (r + 1)) A) (hg : g ∈ points r A) : (typeAGraphAutomorphism r A) g ∈ points r A

Signed reverse-inverse-transpose preserves the matrix points of the standard carrier.

noncomputable def TauCeti.SlStd.graphAutomorphismPoints (r : ℕ) (A : Type) [CommRing A] : ↥(points r A) ≃* ↥(points r A)

The pinned graph automorphism on algebra-valued points of the standard carrier.

Equations

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

@[simp]

theorem TauCeti.SlStd.coe_graphAutomorphismPoints (r : ℕ) {A : Type} [CommRing A] (g : ↥(points r A)) : ↑((graphAutomorphismPoints r A) g) = (typeAGraphAutomorphism r A) ↑g

The point-group graph automorphism is signed reverse-inverse-transpose on matrices.

@[simp]

theorem TauCeti.SlStd.graphAutomorphismPoints_graphAutomorphismPoints (r : ℕ) {A : Type} [CommRing A] (g : ↥(points r A)) : (graphAutomorphismPoints r A) ((graphAutomorphismPoints r A) g) = g

The point-group graph automorphism is an involution. This is the relation γ² = 1 read on algebra-valued points, where TauCeti.SlStd.graphAutomorphism_hom_comp_self reads it on the carrier itself.

@[simp]

theorem TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPoints (r : ℕ) {A : Type} [CommRing A] (i : Fin r ⊕ Fin r) (u : Multiplicative A) : (graphAutomorphismPoints r A) ((rootSubgroupPoints r i A) u) = (rootSubgroupPoints r ((graphRootPerm r) i) A) u

The point-group graph automorphism reverses the numbered root subgroups.

@[simp]

theorem TauCeti.SlStd.graphAutomorphismPoints_weightTorusPoints (r : ℕ) {A : Type} [CommRing A] (s : Fin r → Aˣ) : (graphAutomorphismPoints r A) ((weightTorusPoints r A) s) = (weightTorusPoints r A) fun (i : Fin r) => s i.rev

The point-group graph automorphism reverses the coordinates of the split weight torus.

@[simp]

theorem TauCeti.SlStd.rootSubgroup_comp_graphAutomorphism_hom (r : ℕ) (k : Fin r ⊕ Fin r) : CategoryTheory.CategoryStruct.comp (rootSubgroup r k) (graphAutomorphism r).hom = rootSubgroup r ((graphRootPerm r) k)

The graph automorphism reverses the Bourbaki numbering of every positive and negative simple root subgroup, without changing its additive parameter.

@[simp]

theorem TauCeti.SlStd.rootSubgroup_comp_graphAutomorphism_hom_assoc (r : ℕ) (k : Fin r ⊕ Fin r) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r))))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rootSubgroup r k) (CategoryTheory.CategoryStruct.comp (graphAutomorphism r).hom h) = CategoryTheory.CategoryStruct.comp (rootSubgroup r ((graphRootPerm r) k)) h

The graph automorphism reverses the Bourbaki numbering of every positive and negative simple root subgroup, without changing its additive parameter.

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

The reversal of the type-A_r diagram has exactly one realization on the carrier. An endomorphism of the carrier carrying each numbered raising and lowering root subgroup to the one at the reversed 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.SlStd.eq_graphAutomorphism_of_rootSubgroup (r : ℕ) (γ : CategoryTheory.Aut (groupScheme r)) (hroot : ∀ (k : Fin r ⊕ Fin r), CategoryTheory.CategoryStruct.comp (rootSubgroup r k) γ.hom = rootSubgroup r ((graphRootPerm r) k)) : γ = graphAutomorphism r

The graph automorphism is the unique automorphism of the carrier reversing the Bourbaki numbering of the parametrized simple-root subgroups while preserving their additive parameters.

@[simp]

theorem TauCeti.SlStd.weightTorus_comp_graphAutomorphism_hom (r : ℕ) : CategoryTheory.CategoryStruct.comp (weightTorus r) (graphAutomorphism r).hom = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ Fin.revPerm) (weightTorus r)

The graph automorphism normalizes the split torus and reverses its Bourbaki-numbered coordinates.

@[simp]

theorem TauCeti.SlStd.weightTorus_comp_graphAutomorphism_hom_assoc (r : ℕ) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r))))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (weightTorus r) (CategoryTheory.CategoryStruct.comp (graphAutomorphism r).hom h) = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ Fin.revPerm) (CategoryTheory.CategoryStruct.comp (weightTorus r) h)

The graph automorphism normalizes the split torus and reverses its Bourbaki-numbered coordinates.

@[simp]

theorem TauCeti.SlStd.graphAutomorphism_hom_comp_self (r : ℕ) : CategoryTheory.CategoryStruct.comp (graphAutomorphism r).hom (graphAutomorphism r).hom = CategoryTheory.CategoryStruct.id (groupScheme r)

Applying the graph automorphism twice is the identity on the standard carrier.

@[simp]

theorem TauCeti.SlStd.graphAutomorphism_hom_comp_self_assoc (r : ℕ) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))} (h : (AlgebraicGeometry.algSpec ↧ℤ).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat ℤ).functor.leftOp.obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r))))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (graphAutomorphism r).hom (CategoryTheory.CategoryStruct.comp (graphAutomorphism r).hom h) = h

Applying the graph automorphism twice is the identity on the standard carrier.

@[simp]

theorem TauCeti.SlStd.graphAutomorphism_inv (r : ℕ) : (graphAutomorphism r).inv = (graphAutomorphism r).hom

The inverse leg of the graph automorphism is its forward leg.