The diagonal torus of the special linear group #

The determinant-one diagonal matrices of SL_{r+1} form a split torus of rank r. This file parametrizes it in fundamental-weight coordinates: a point s = (s₀, …, s_{r-1}) of the split torus goes to

diag(s₀, s₁ s₀⁻¹, …, s_{r-1} s_{r-2}⁻¹, s_{r-1}⁻¹),

whose k-th entry is the value of the standard weight ε_k of sl_{r+1}, written in the basis of fundamental weights as TauCeti.SlStd.weight r k. These are the coordinates of the pinned simply connected root datum of type A_r, in which the simple roots are the rows of the Cartan matrix.

The coordinate morphism O(SL_{r+1}) ⟶ R[X*(T)] is obtained by factoring the general-linear weight torus TauCeti.GeneralLinear.weightTorusCoordinateMap through the determinant-one quotient: the standard weights sum to zero, so the generic determinant restricts to one. Since the standard weights span the character lattice, the coordinate morphism is surjective over every commutative base ring; contravariantly, the torus is a closed subgroup of SL_{r+1}.

Main declarations #

TauCeti.SpecialLinear.diagonalTorusWeight: the standard weights, indexed by the universe-lifted torus coordinates.
TauCeti.SpecialLinear.diagonalTorusCoordinateMap: the coordinate morphism of the diagonal torus of SL_{r+1}.
TauCeti.SpecialLinear.coordinateMap_comp_diagonalTorusCoordinateMap: its composite with the quotient O(GL_{r+1}) ⟶ O(SL_{r+1}) is the general-linear weight torus.
TauCeti.SpecialLinear.diagonalTorusCoordinateMap_surjective: the coordinate morphism is surjective.
TauCeti.SpecialLinear.toGL_pointsMulEquiv_mapPointsFunctor_diagonalTorusCoordinateMap: on algebra-valued points it is the diagonal matrix of the standard weight characters.
TauCeti.SpecialLinear.diagonalTorusPoints and TauCeti.SpecialLinear.toGL_pointsMulEquiv_diagonalTorusPoints: the resulting homomorphism of convolution groups of points, and its diagonal matrices.
TauCeti.SpecialLinear.diagonalTorusCoordinateMap_baseChange: compatibility with scalar extension.

References #

J. S. Milne, Algebraic Groups (2017), Chapters 12 and 21.
J. E. Humphreys, Linear Algebraic Groups (1975), §§15.3 and 26.3.
The construction follows the diagonal torus of TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.Basic.

source

def TauCeti.SpecialLinear.diagonalTorusWeight (r : ℕ) (k : Fin (r + 1)) :

ULift.{u, 0} (Fin r) → ℤ

The standard weight ε_k of sl_{r+1} in fundamental-weight coordinates, indexed by the universe-lifted coordinates of the rank-r split torus.

Equations

TauCeti.SpecialLinear.diagonalTorusWeight r k i = TauCeti.SlStd.weight r k i.down

Instances For

source

@[simp]

theorem TauCeti.SpecialLinear.diagonalTorusWeight_apply (r : ℕ) (k : Fin (r + 1)) (i : ULift.{u, 0} (Fin r)) :

diagonalTorusWeight r k i = SlStd.weight r k i.down

source

theorem TauCeti.SpecialLinear.sum_diagonalTorusWeight_eq_zero (r : ℕ) :

∑ k : Fin (r + 1), diagonalTorusWeight r k = 0

The standard weights sum to zero.

source

theorem TauCeti.SpecialLinear.span_range_diagonalTorusWeight_eq_top (r : ℕ) :

Submodule.span ℤ (Set.range (diagonalTorusWeight r)) = ⊤

The standard weights span the character lattice of the rank-r split torus.

source

@[simp]

theorem TauCeti.SpecialLinear.torusCharacter_diagonalTorusWeight (r : ℕ) {A : Type w} [CommRing A] (s : ULift.{u, 0} (Fin r) → Aˣ) (k : Fin (r + 1)) :

torusCharacter s (diagonalTorusWeight r k) = torusCharacter (fun (i : Fin r) => s { down := i }) (SlStd.weight r k)

A split-torus character of a standard weight, read in the original torus coordinates.

source

noncomputable def TauCeti.SpecialLinear.diagonalTorusCoordinateMap (r : ℕ) (R : Type u) [CommRing R] :

coordinateHopfAlgebra R (r + 1) ⟶ (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))).obj

The coordinate morphism of the diagonal torus of SL_{r+1}. It restricts functions on SL_{r+1} to the rank-r split torus embedded through the standard weights. Its direction is opposite to the represented group-scheme morphism.

Equations

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

Instances For

source

@[simp]

theorem TauCeti.SpecialLinear.coordinateMap_comp_diagonalTorusCoordinateMap (r : ℕ) (R : Type u) [CommRing R] :

CategoryTheory.CategoryStruct.comp (coordinateMap R (r + 1)) (diagonalTorusCoordinateMap r R) = GeneralLinear.weightTorusCoordinateMap (diagonalTorusWeight r)

Restricting from GL_{r+1} to SL_{r+1} and then to the diagonal torus is the general-linear weight torus of the standard weights.

source

theorem TauCeti.SpecialLinear.diagonalTorusCoordinateMap_surjective (r : ℕ) (R : Type u) [CommRing R] :

Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R))

The coordinate morphism of the diagonal torus of SL_{r+1} is surjective over every commutative base ring.

source

theorem TauCeti.SpecialLinear.toGL_pointsMulEquiv_mapPointsFunctor_diagonalTorusCoordinateMap (r : ℕ) (R : Type u) [CommRing R] (A : Type w) [CommRing A] [Algebra R A] (p : ↑(HopfAlgebra.points ↧A)) :

Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R (r + 1)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (diagonalTorusCoordinateMap r R)).app ↧A)) p)) = diagGL fun (k : Fin (r + 1)) => torusCharacter (SplitTorus.pointsMulEquiv p) (diagonalTorusWeight r k)

The diagonal torus of SL_{r+1} on algebra-valued points. A point s of the split torus goes to the diagonal matrix whose k-th entry is the character of the standard weight ε_k.

source

noncomputable def TauCeti.SpecialLinear.diagonalTorusPoints (r : ℕ) (R : Type u) [CommRing R] (A : Type w) [CommRing A] [Algebra R A] :

WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R (r + 1)) →ₐ[R] A)

The diagonal-torus homomorphism on A-points: the component at A of the point map of diagonalTorusCoordinateMap, viewed between the convolution groups of algebra maps.

Equations