The represented type-A graph involution of the special linear group

Signed reverse inverse transpose defines an automorphism of the special linear group scheme over every commutative ring. Its square is the identity, and it carries each positive or negative simple-root subgroup to the subgroup at the reversed node, with parameter unchanged. These coordinate identities hold over the base ring itself, so they retain the scheme structure in positive characteristic and over nonreduced rings.

The construction recovers the coordinate automorphism from the natural matrix involution using TauCeti.CommHopfAlgCat.pointsFunctor. It uses the determinant-one presentation of SLₙ, independently of a presentation by generators of a Kostant carrier.

References

• R. W. Carter, Simple Groups of Lie Type, Chapter 12.
• R. Steinberg, Lectures on Chevalley Groups, §3.
• The matrix normalization is Matrix.SpecialLinearGroup.typeAGraphAutomorphism. The represented construction follows the Yoneda approach of TauCeti.Algebra.AlgebraicGroup.GeneralLinear.GraphAutomorphism.

noncomputable def TauCeti.SpecialLinear.typeAGraphCoordinateIso (R : Type u) [CommRing R] (r : ℕ) : coordinateHopfAlgebra R (r + 1) ≅ coordinateHopfAlgebra R (r + 1)

The coordinate Hopf-algebra automorphism of SL_{r+1} induced by signed reverse inverse transpose. It is defined over every commutative base ring.

Equations

• TauCeti.SpecialLinear.typeAGraphCoordinateIso R r = (TauCeti.CommHopfAlgCat.pointsFunctor.preimageIso (TauCeti.SpecialLinear.typeAGraphPointsNatIso✝ R r)).unop

@[simp]

theorem TauCeti.SpecialLinear.pointsMulEquiv_comp_typeAGraphCoordinateIso (R : Type u) [CommRing R] (r : ℕ) (A : Type w) [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R (r + 1)) →ₐ[R] A)) : (pointsMulEquiv R (r + 1)) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (typeAGraphCoordinateIso R r).hom))) = (Matrix.SpecialLinearGroup.typeAGraphAutomorphism r A) ((pointsMulEquiv R (r + 1)) f)

Precomposition with the coordinate graph automorphism realizes the signed matrix graph automorphism on points over an algebra in any universe.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphCoordinateIso_hom_comp_self (R : Type u) [CommRing R] (r : ℕ) : CategoryTheory.CategoryStruct.comp (typeAGraphCoordinateIso R r).hom (typeAGraphCoordinateIso R r).hom = CategoryTheory.CategoryStruct.id (coordinateHopfAlgebra R (r + 1))

The coordinate graph automorphism is involutive over the base ring.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphCoordinateIso_inv (R : Type u) [CommRing R] (r : ℕ) : (typeAGraphCoordinateIso R r).inv = (typeAGraphCoordinateIso R r).hom

The inverse coordinate graph automorphism equals its forward morphism.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphCoordinateIso_hom_comp_rootSubgroupCoordinateMap (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) : CategoryTheory.CategoryStruct.comp (typeAGraphCoordinateIso R r).hom (rootSubgroupCoordinateMap ⋯) = rootSubgroupCoordinateMap ⋯

The graph automorphism reverses the positive simple-root maps with their parameters unchanged. This is an equality of coordinate morphisms over the base ring.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphCoordinateIso_hom_comp_rootSubgroupCoordinateMap_assoc (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) {Z : CommHopfAlgCat R} (h : AdditiveGroup.coordinateHopfAlgebra R ⟶ Z) : CategoryTheory.CategoryStruct.comp (typeAGraphCoordinateIso R r).hom (CategoryTheory.CategoryStruct.comp (rootSubgroupCoordinateMap ⋯) h) = CategoryTheory.CategoryStruct.comp (rootSubgroupCoordinateMap ⋯) h

The graph automorphism reverses the positive simple-root maps with their parameters unchanged. This is an equality of coordinate morphisms over the base ring.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphCoordinateIso_hom_comp_rootSubgroupCoordinateMap_lower (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) : CategoryTheory.CategoryStruct.comp (typeAGraphCoordinateIso R r).hom (rootSubgroupCoordinateMap ⋯) = rootSubgroupCoordinateMap ⋯

The graph automorphism also reverses the negative simple-root maps without a sign.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphCoordinateIso_hom_comp_rootSubgroupCoordinateMap_lower_assoc (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) {Z : CommHopfAlgCat R} (h : AdditiveGroup.coordinateHopfAlgebra R ⟶ Z) : CategoryTheory.CategoryStruct.comp (typeAGraphCoordinateIso R r).hom (CategoryTheory.CategoryStruct.comp (rootSubgroupCoordinateMap ⋯) h) = CategoryTheory.CategoryStruct.comp (rootSubgroupCoordinateMap ⋯) h

The graph automorphism also reverses the negative simple-root maps without a sign.

noncomputable def TauCeti.SpecialLinear.typeAGraphIso (R : Type u) [CommRing R] (r : ℕ) : groupScheme R (r + 1) ≅ groupScheme R (r + 1)

The signed type-A graph automorphism as an isomorphism of special-linear group schemes over the base ring.

Equations

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

theorem TauCeti.SpecialLinear.typeAGraphIso_hom (R : Type u) [CommRing R] (r : ℕ) : (typeAGraphIso R r).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (typeAGraphCoordinateIso R r).hom.op) (CategoryTheory.eqToHom ⋯))

The group-scheme graph automorphism is relative spectrum of the coordinate automorphism.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphIso_hom_comp_self (R : Type u) [CommRing R] (r : ℕ) : CategoryTheory.CategoryStruct.comp (typeAGraphIso R r).hom (typeAGraphIso R r).hom = CategoryTheory.CategoryStruct.id (groupScheme R (r + 1))

The represented group-scheme graph automorphism is involutive.

@[simp]

theorem TauCeti.SpecialLinear.typeAGraphIso_inv (R : Type u) [CommRing R] (r : ℕ) : (typeAGraphIso R r).inv = (typeAGraphIso R r).hom

The inverse group-scheme graph automorphism equals its forward morphism.

@[simp]

theorem TauCeti.SpecialLinear.rootSubgroup_comp_typeAGraphIso_hom (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) : CategoryTheory.CategoryStruct.comp (rootSubgroup ⋯) (typeAGraphIso R r).hom = rootSubgroup ⋯

The group-scheme graph automorphism reverses positive simple-root subgroups, with the additive parameter unchanged.

@[simp]

theorem TauCeti.SpecialLinear.rootSubgroup_comp_typeAGraphIso_hom_assoc (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (h : groupScheme R (r + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rootSubgroup ⋯) (CategoryTheory.CategoryStruct.comp (typeAGraphIso R r).hom h) = CategoryTheory.CategoryStruct.comp (rootSubgroup ⋯) h

The group-scheme graph automorphism reverses positive simple-root subgroups, with the additive parameter unchanged.

@[simp]

theorem TauCeti.SpecialLinear.rootSubgroup_comp_typeAGraphIso_hom_lower (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) : CategoryTheory.CategoryStruct.comp (rootSubgroup ⋯) (typeAGraphIso R r).hom = rootSubgroup ⋯

The group-scheme graph automorphism also reverses negative simple-root subgroups without changing their parameters.

@[simp]

theorem TauCeti.SpecialLinear.rootSubgroup_comp_typeAGraphIso_hom_lower_assoc (R : Type u) [CommRing R] (r : ℕ) (i : Fin r) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (h : groupScheme R (r + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rootSubgroup ⋯) (CategoryTheory.CategoryStruct.comp (typeAGraphIso R r).hom h) = CategoryTheory.CategoryStruct.comp (rootSubgroup ⋯) h

The group-scheme graph automorphism also reverses negative simple-root subgroups without changing their parameters.