The special linear group over a ring and its split maximal torus

SL_n is a reductive affine group scheme over every commutative ring. The determinant-one diagonal matrices give a chosen split maximal torus of SL_{r+1} of rank r, in the fundamental-weight coordinates of type A_r.

The integral smoothness theorem and the base-change comparison with the field-valued special-linear coordinate algebra supply reductivity over the base. The existing diagonal-torus coordinate morphism, its surjectivity, and its maximality over fields supply the torus data. In particular these give an integral example over ℤ together with all its geometric fibers.

The chosen torus is compatible with base change: base-changing the torus over R to an R-algebra S and transporting it along the base-change isomorphism of coordinate Hopf algebras gives the chosen torus over S (splitMaximalTorus_baseChange_comapOfIso). It lies in the upper-triangular subgroup (UpperTriangular.definingHopfIdeal_le_splitMaximalTorus_definingIdeal), which is a Borel subgroup of SL_{r+1} over every commutative ring (TauCeti.SpecialLinear.UpperTriangular.isBorelOver_definingHopfIdeal), so the two form a torus contained in a Borel subgroup over the base.

References

• B. Conrad, Reductive Group Schemes (2014), Definitions 3.1.1 and 3.2.1.
• J. S. Milne, Algebraic Groups (2017), Chapters 12 and 21.

theorem TauCeti.SpecialLinear.reductiveCommHopfAlgPropertyOver_finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : reductiveCommHopfAlgPropertyOver R (finiteTypeCoordinateHopfAlgebra R n)

The special linear group is reductive over every commutative base ring.

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

The determinant-one diagonal torus, parametrized in fundamental-weight coordinates, is a chosen split maximal torus of SL_{r+1} over every commutative base ring.

Equations

• TauCeti.SpecialLinear.splitMaximalTorus R r = { coordinateMap := TauCeti.SpecialLinear.diagonalTorusCoordinateMap r R, surjective := ⋯, maximal := ⋯ }

@[simp]

theorem TauCeti.SpecialLinear.splitMaximalTorus_coordinateMap (R : Type u) [CommRing R] (r : ℕ) : (splitMaximalTorus R r).coordinateMap = diagonalTorusCoordinateMap r R

The chosen split maximal torus has the standard diagonal-torus coordinate morphism.

@[simp]

theorem TauCeti.SpecialLinear.splitMaximalTorus_definingIdeal (R : Type u) [CommRing R] (r : ℕ) : (splitMaximalTorus R r).definingIdeal = diagonalTorusDefiningIdeal r R

The chosen split maximal torus has the standard diagonal-torus defining ideal.

theorem TauCeti.SpecialLinear.splitMaximalTorus_baseChange_comapOfIso (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] (r : ℕ) : (SplitMaximalTorus.baseChange S (splitMaximalTorus R r)).comapOfIso (coordinateHopfAlgebraBaseChangeIso R S (r + 1)).symm = splitMaximalTorus S r

The chosen split maximal torus of SL_{r+1} is compatible with base change: base-changing the torus over R to S and transporting it along the base-change isomorphism of special-linear coordinate Hopf algebras gives the chosen torus over S.

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_le_splitMaximalTorus_definingIdeal (R : Type u) [CommRing R] (r : ℕ) : definingHopfIdeal R (r + 1) ≤ (splitMaximalTorus R r).definingIdeal

The chosen split maximal torus of SL_{r+1} lies in the upper-triangular subgroup, over every commutative base ring. The order of Hopf ideals reverses inclusion of closed subgroups.