The root datum of the special linear group relative to its diagonal torus

The diagonal torus of SL_{r+1} is the rank-r split torus embedded through the standard weights ε₀, …, ε_r, written in fundamental-weight coordinates by TauCeti.SpecialLinear.diagonalTorusWeight. Its character lattice is X*(T) = ULift (Fin r) →₀ ℤ in the fundamental-weight basis, and its cocharacter lattice is X_*(T) = ULift (Fin r) → ℤ in the dual basis, which is the basis of simple coroots. This file equips these lattices with the root datum of type A_r, indexed by the ordered pairs (a, b) of distinct matrix indices, that is, by the root subgroups x_{ab} of SL_{r+1}. The root indexed by (a, b) is ε_a - ε_b, its coroot is e_a - e_b, and the pairing is the split-torus dot pairing.

The datum is obtained by transporting the pinned simply connected datum TauCeti.DynkinType.typeASimplyConnectedRootDatum with RootPairing.map along the universe lift of both lattices, the roots being reindexed by TauCeti.DynkinType.typeAIndexEquiv. Consequently its coroots span the cocharacter lattice: SL_{r+1} has the simply connected root datum of type A_r. What ties the datum to the group is TauCeti.SpecialLinear.charOfPoint_ofAdd_diagonalRootDatum_root: the root indexed by (a, b) is exactly the character through which the diagonal torus rescales the root subgroup x_{ab}.

Main definitions

• TauCeti.SpecialLinear.diagonalRootDatum: the type A_r root datum on the lattices of the diagonal torus of SL_{r+1}.
• TauCeti.SpecialLinear.diagonalRootDatumEquiv: the identification with the pinned simply connected type-A_r datum, allowing its base to be transported to these lattices.

Main results

• TauCeti.SpecialLinear.diagonalRootDatum_toLinearMap: its pairing is the split-torus dot pairing.
• TauCeti.SpecialLinear.diagonalRootDatum_root_apply and TauCeti.SpecialLinear.diagonalRootDatum_coroot_apply: the roots ε_a - ε_b and coroots e_a - e_b in coordinates.
• TauCeti.SpecialLinear.diagonalRootDatum_pairing_apply: the Cartan integers.
• TauCeti.SpecialLinear.diagonalRootDatum_reflectionPerm: reflections act on root indices by transposing matrix indices.
• TauCeti.SpecialLinear.diagonalRootDatum_coroot_castSucc_succ: the simple coroots are the standard basis, and TauCeti.SpecialLinear.corootSpan_diagonalRootDatum_eq_top: the coroots span the cocharacter lattice.
• TauCeti.SpecialLinear.charOfPoint_ofAdd_diagonalRootDatum_root: the roots are the characters of the diagonal torus on the root subgroups.
• TauCeti.SpecialLinear.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv_eq_root: the pinning equation, with the scaling character given by diagonalRootDatum.

References

• J. S. Milne, Algebraic Groups (2017), §21 and Example 21.2.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3 and §27.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate I.
• The construction follows TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.RootDatum.

noncomputable def TauCeti.SpecialLinear.diagonalRootDatum (r : ℕ) : RootDatum (SplitTorus.CoordinateRootIndex (Fin (r + 1))) (ULift.{u, 0} (Fin r) →₀ ℤ) (ULift.{u, 0} (Fin r) → ℤ)

The root datum of SL_{r+1} relative to its diagonal torus. It is the pinned simply connected datum of type A_r, written on the character and cocharacter lattices of the diagonal torus and indexed by the ordered pairs of distinct matrix indices.

Equations

• TauCeti.SpecialLinear.diagonalRootDatum r = RootPairing.map (TauCeti.DynkinType.typeAIndexEquiv r).symm (TauCeti.SpecialLinear.characterEquiv✝ r) (TauCeti.SpecialLinear.cocharacterEquiv✝ r)

noncomputable def TauCeti.SpecialLinear.diagonalRootDatumEquiv (r : ℕ) : RootPairing.Equiv (DynkinType.typeASimplyConnectedRootDatum r) (diagonalRootDatum r)

The identification of the pinned simply connected type-A datum with the root datum on the diagonal torus lattices of SL_{r+1}.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatumEquiv_indexEquiv (r : ℕ) : (↑(diagonalRootDatumEquiv r)).indexEquiv = (DynkinType.typeAIndexEquiv r).symm

The root indices are transported by the ordered-pair enumeration.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatumEquiv_weightMap_apply {r : ℕ} (x : Fin r → ℤ) (i : ULift.{u, 0} (Fin r)) : ((↑(diagonalRootDatumEquiv r)).weightMap x) i = x i.down

The weight map writes a weight in the universe-lifted fundamental-weight coordinates.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatumEquiv_coweightMap_apply {r : ℕ} (y : ULift.{u, 0} (Fin r) → ℤ) (i : Fin r) : (↑(diagonalRootDatumEquiv r)).coweightMap y i = y { down := i }

The contravariant coweight map removes the universe lift on simple-coroot coordinates.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatum_toLinearMap (r : ℕ) : (diagonalRootDatum r).toLinearMap = SplitTorus.dotPairing

The pairing of diagonalRootDatum is the split-torus dot pairing.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatum_root_apply {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (i : ULift.{u, 0} (Fin r)) : ((diagonalRootDatum r).root p) i = diagonalTorusWeight r (↑p).1 i - diagonalTorusWeight r (↑p).2 i

The roots are the differences of standard weights. The root indexed by (a, b) is ε_a - ε_b, written in fundamental-weight coordinates.

@[simp]

theorem TauCeti.SpecialLinear.weightCharacter_diagonalTorusWeight_sub_eq_root_iff {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (a b : Fin (r + 1)) : SplitTorus.weightCharacter (diagonalTorusWeight r a - diagonalTorusWeight r b) = Multiplicative.ofAdd ((diagonalRootDatum r).root p) ↔ a = (↑p).1 ∧ b = (↑p).2

A difference of standard weights is a specified root character exactly at that root's ordered pair of matrix indices. This comparison takes place in the integral character lattice, independently of the coefficient ring.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatum_coroot_apply {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (i : ULift.{u, 0} (Fin r)) : (diagonalRootDatum r).coroot p i = (if (↑p).1 ≤ i.down.castSucc then 1 else 0) - if (↑p).2 ≤ i.down.castSucc then 1 else 0

The coroots in simple-coroot coordinates. The coroot indexed by (a, b) is e_a - e_b, whose i-th simple-coroot coordinate is [a ≤ i] - [b ≤ i].

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatum_pairing_apply {r : ℕ} (p q : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : RootPairing.pairing (diagonalRootDatum r) p q = ((if (↑p).1 = (↑q).1 then 1 else 0) - if (↑p).1 = (↑q).2 then 1 else 0) - ((if (↑p).2 = (↑q).1 then 1 else 0) - if (↑p).2 = (↑q).2 then 1 else 0)

The Cartan integers. The pairing of the root ε_a - ε_b with the coroot e_c - e_d is [a = c] - [a = d] - ([b = c] - [b = d]).

theorem TauCeti.SpecialLinear.diagonalRootDatum_pairing_comm {r : ℕ} (p q : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : RootPairing.pairing (diagonalRootDatum r) p q = RootPairing.pairing (diagonalRootDatum r) q p

The root--coroot pairing of the diagonal root datum is symmetric.

instance TauCeti.SpecialLinear.isReduced_diagonalRootDatum (r : ℕ) : RootPairing.IsReduced (diagonalRootDatum r)

The root datum of the diagonal torus of SL_{r+1} is reduced.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootDatum_reflectionPerm {r : ℕ} (p q : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : ((diagonalRootDatum r).reflectionPerm p) q = (SplitTorus.coordinatePermRootIndex (Equiv.swap (↑p).1 (↑p).2)) q

Reflections transpose matrix indices. The reflection in the root indexed by (a, b) sends the root indexed by (c, d) to the one indexed by (s c, s d), where s is the transposition of a and b.

theorem TauCeti.SpecialLinear.diagonalRootDatum_coroot_castSucc_succ {r : ℕ} (i : Fin r) : (diagonalRootDatum r).coroot ⟨(i.castSucc, i.succ), ⋯⟩ = Pi.single { down := i } 1

The simple coroots are the standard basis. The coroot of the simple root ε_i - ε_{i+1} is the i-th basis vector of the cocharacter lattice.

theorem TauCeti.SpecialLinear.corootSpan_diagonalRootDatum_eq_top (r : ℕ) : RootPairing.corootSpan (diagonalRootDatum r) ℤ = ⊤

The root datum of SL_{r+1} is simply connected: its coroots span the cocharacter lattice of the diagonal torus.

The roots as characters of the diagonal torus

theorem TauCeti.SpecialLinear.charOfPoint_ofAdd_diagonalRootDatum_root {r : ℕ} {R : Type u} [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)) →ₐ[R] A)) : (DiagonalizableGroup.charOfPoint t.ofConv) (Multiplicative.ofAdd ((diagonalRootDatum r).root p)) = torusCharacter (SplitTorus.pointsMulEquiv t) (diagonalTorusWeight r (↑p).1) / torusCharacter (SplitTorus.pointsMulEquiv t) (diagonalTorusWeight r (↑p).2)

The roots are characters of the diagonal torus. Evaluated at a point of the split torus, the root ε_a - ε_b of diagonalRootDatum is the quotient of the values of the standard weights ε_a and ε_b.

theorem TauCeti.SpecialLinear.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv_eq_root {r : ℕ} {R : Type u} [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)) →ₐ[R] A)) (c : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : (diagonalTorusPoints r R A) t * (rootSubgroupPoints ⋯) c * ((diagonalTorusPoints r R A) t)⁻¹ = (rootSubgroupPoints ⋯) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑((DiagonalizableGroup.charOfPoint t.ofConv) (Multiplicative.ofAdd ((diagonalRootDatum r).root p))) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv c))))

The pinning equation of SL_{r+1}, with the roots of diagonalRootDatum. Conjugation by a point of the diagonal torus scales the parameter of the root subgroup x_{ab} by the value of the root indexed by (a, b).