The root datum of the symplectic group relative to its diagonal torus

The paired diagonal torus diag(t₀, …, tₘ₋₁, t₀⁻¹, …, tₘ₋₁⁻¹) of Sp₂ₘ has character lattice X*(T) = ULift (Fin m) →₀ ℤ and cocharacter lattice X_*(T) = ULift (Fin m) → ℤ. This file equips these lattices with the root datum of type Cₘ, indexed by the standard symplectic root subgroups themselves. Writing eᵢ for the coordinate vectors, its roots are

2eᵢ,  -2eᵢ,  eᵢ - eⱼ,  eᵢ + eⱼ,  -eᵢ - eⱼ,

with coroots eᵢ, -eᵢ on the long roots and the same vectors as the roots on the short ones, and its pairing is the split-torus dot pairing.

The datum is obtained by transporting the pinned simply connected datum TauCeti.DynkinType.typeCSimplyConnectedRootDatum with RootPairing.map along the classical coordinates TauCeti.DynkinType.TypeC.classicalWeightEquiv and TauCeti.DynkinType.TypeC.classicalCoweightEquiv. What ties it to the group is TauCeti.Symplectic.charOfPoint_ofAdd_diagonalRootDatum_root: the root indexed by a root subgroup is exactly the character through which the diagonal torus rescales that subgroup.

Main definitions

• TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex: the symplectic root subgroups are indexed by the type C root indices.
• TauCeti.Symplectic.diagonalRootDatum: the type Cₘ root datum on the lattices of the diagonal torus.

Main results

• TauCeti.Symplectic.diagonalRootDatum_toLinearMap: its pairing is the split-torus dot pairing.
• TauCeti.Symplectic.diagonalRootDatum_pairing_apply: the Cartan pairing in coordinates.
• TauCeti.Symplectic.diagonalRootDatum_reflection_apply and TauCeti.Symplectic.diagonalRootDatum_coreflection_apply: the reflection formulas in coordinates.
• TauCeti.Symplectic.diagonalRootDatum_reflectionPerm and TauCeti.Symplectic.diagonalReflectionIndex_eq_iff: the induced action on root-subgroup indices and its characterization through the roots.
• TauCeti.Symplectic.diagonalRootDatum_root_positiveLong and its companions: the roots in coordinates.
• TauCeti.Symplectic.diagonalRootDatum_coroot_positiveLong and its companions: the coroots in coordinates.
• TauCeti.Symplectic.diagonalRootDatum_reflection_positiveLong_apply and its companions: each reflection is a signed permutation of the coordinates.
• TauCeti.Symplectic.diagonalRootDatum_coreflection_positiveLong_apply and its companions: each coreflection is the same signed permutation of the coordinates.
• TauCeti.Symplectic.charOfPoint_ofAdd_diagonalRootDatum_root: the roots are the characters of the diagonal torus on the root subgroups.
• TauCeti.Symplectic.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 (the symplectic groups).
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3 and §27.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.

def TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex (m : ℕ) : RootSubgroupIndex m ≃ DynkinType.TypeCIndex m

The symplectic root subgroups are indexed by the type C root indices. A root subgroup with root (-1) ^ s * (e_a ± e_b) is sent to (a, b, s), in the normalization of TauCeti.DynkinType.TypeCIndex.

Equations

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

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_positiveLong {m : ℕ} (i : Fin m) : (equivTypeCIndex m) (positiveLong i) = (i, i, false)

The long root 2eᵢ has type C index (i, i, false).

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_negativeLong {m : ℕ} (i : Fin m) : (equivTypeCIndex m) (negativeLong i) = (i, i, true)

The long root -2eᵢ has type C index (i, i, true).

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_difference_of_lt {m : ℕ} {i j : Fin m} (h : i < j) : (equivTypeCIndex m) (difference i j ⋯) = (i, j, false)

For i < j, the short root eᵢ - eⱼ has type C index (i, j, false).

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_difference_of_gt {m : ℕ} {i j : Fin m} (h : j < i) : (equivTypeCIndex m) (difference i j ⋯) = (j, i, true)

For j < i, the short root eᵢ - eⱼ = -(eⱼ - eᵢ) has type C index (j, i, true).

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_positiveSum {m : ℕ} {i j : Fin m} (h : i < j) : (equivTypeCIndex m) (positiveSum i j h) = (j, i, false)

For i < j, the short root eᵢ + eⱼ has type C index (j, i, false).

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_negativeSum {m : ℕ} {i j : Fin m} (h : i < j) : (equivTypeCIndex m) (negativeSum i j h) = (j, i, true)

For i < j, the short root -eᵢ - eⱼ has type C index (j, i, true).

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_symm_diagonal_false {m : ℕ} (i : Fin m) : (equivTypeCIndex m).symm (i, i, false) = positiveLong i

A diagonal type C index with positive sign corresponds to the long root 2eᵢ.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_symm_diagonal_true {m : ℕ} (i : Fin m) : (equivTypeCIndex m).symm (i, i, true) = negativeLong i

A diagonal type C index with negative sign corresponds to the long root -2eᵢ.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_symm_of_lt_false {m : ℕ} {a b : Fin m} (h : a < b) : (equivTypeCIndex m).symm (a, b, false) = difference a b ⋯

For a < b, the unsigned type C index (a, b, false) corresponds to e_a - e_b.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_symm_of_lt_true {m : ℕ} {a b : Fin m} (h : a < b) : (equivTypeCIndex m).symm (a, b, true) = difference b a ⋯

For a < b, the signed type C index (a, b, true) corresponds to e_b - e_a.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_symm_of_gt_false {m : ℕ} {a b : Fin m} (h : b < a) : (equivTypeCIndex m).symm (a, b, false) = positiveSum b a h

For b < a, the unsigned type C index (a, b, false) corresponds to e_b + e_a.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.equivTypeCIndex_symm_of_gt_true {m : ℕ} {a b : Fin m} (h : b < a) : (equivTypeCIndex m).symm (a, b, true) = negativeSum b a h

For b < a, the signed type C index (a, b, true) corresponds to -e_b - e_a.

noncomputable def TauCeti.Symplectic.diagonalRootDatum (m : ℕ) : RootDatum (GLSymplecticFin.RootSubgroupIndex m) (ULift.{u, 0} (Fin m) →₀ ℤ) (ULift.{u, 0} (Fin m) → ℤ)

The root datum of Sp₂ₘ relative to its diagonal torus. It is the pinned simply connected datum of type Cₘ, written on the character and cocharacter lattices of the diagonal torus and indexed by the standard symplectic root subgroups.

Equations

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

instance TauCeti.Symplectic.instIsReducedDiagonalRootDatum (m : ℕ) : RootPairing.IsReduced (diagonalRootDatum m)

The root datum of the symplectic diagonal torus is reduced.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_toLinearMap (m : ℕ) : (diagonalRootDatum m).toLinearMap = SplitTorus.dotPairing

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

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_pairing_apply {m : ℕ} (p q : GLSymplecticFin.RootSubgroupIndex m) : RootPairing.pairing (diagonalRootDatum m) p q = ((diagonalRootDatum m).root p).sum fun (i : ULift.{u, 0} (Fin m)) (c : ℤ) => c * (diagonalRootDatum m).coroot q i

Closed coordinate formula for the Cartan pairing of the symplectic diagonal root datum.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflection_apply {m : ℕ} (p : GLSymplecticFin.RootSubgroupIndex m) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (a : ULift.{u, 0} (Fin m)) : ((RootPairing.reflection (diagonalRootDatum m) p) x) a = x a - (x.sum fun (i : ULift.{u, 0} (Fin m)) (c : ℤ) => c * (diagonalRootDatum m).coroot p i) * ((diagonalRootDatum m).root p) a

Reflection in a root acts on characters by subtracting their pairing with its coroot.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coreflection_apply {m : ℕ} (p : GLSymplecticFin.RootSubgroupIndex m) (x : ULift.{u, 0} (Fin m) → ℤ) (a : ULift.{u, 0} (Fin m)) : (RootPairing.coreflection (diagonalRootDatum m) p) x a = x a - (((diagonalRootDatum m).root p).sum fun (i : ULift.{u, 0} (Fin m)) (c : ℤ) => c * x i) * (diagonalRootDatum m).coroot p a

Coreflection in a root acts on cocharacters by subtracting their pairing with its root.

noncomputable def TauCeti.Symplectic.diagonalReflectionIndex {m : ℕ} (p q : GLSymplecticFin.RootSubgroupIndex m) : GLSymplecticFin.RootSubgroupIndex m

The index obtained by reflecting one symplectic root subgroup in another, transported from the pinned type C root datum.

Equations

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

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflectionPerm {m : ℕ} (p q : GLSymplecticFin.RootSubgroupIndex m) : ((diagonalRootDatum m).reflectionPerm p) q = diagonalReflectionIndex p q

Reflection in a root induces diagonalReflectionIndex on root-subgroup indices.

theorem TauCeti.Symplectic.diagonalReflectionIndex_eq_iff {m : ℕ} {p q r : GLSymplecticFin.RootSubgroupIndex m} : diagonalReflectionIndex p q = r ↔ (diagonalRootDatum m).root r = (RootPairing.reflection (diagonalRootDatum m) p) ((diagonalRootDatum m).root q)

diagonalReflectionIndex p q is the root subgroup whose root is the reflection of the root of q in the root of p. Together with the signed-coordinate formulas for the reflections below, this determines its constructor.

The roots in coordinates

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_root_positiveLong {m : ℕ} (i : Fin m) : (diagonalRootDatum m).root (GLSymplecticFin.RootSubgroupIndex.positiveLong i) = Finsupp.single { down := i } 2

The root of the positive long root subgroup is 2eᵢ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_root_negativeLong {m : ℕ} (i : Fin m) : (diagonalRootDatum m).root (GLSymplecticFin.RootSubgroupIndex.negativeLong i) = -Finsupp.single { down := i } 2

The root of the negative long root subgroup is -2eᵢ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_root_difference {m : ℕ} {i j : Fin m} (hij : i ≠ j) : (diagonalRootDatum m).root (GLSymplecticFin.RootSubgroupIndex.difference i j hij) = Finsupp.single { down := i } 1 - Finsupp.single { down := j } 1

The root of the difference root subgroup is eᵢ - eⱼ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_root_positiveSum {m : ℕ} {i j : Fin m} (hij : i < j) : (diagonalRootDatum m).root (GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij) = Finsupp.single { down := i } 1 + Finsupp.single { down := j } 1

The root of the positive sum root subgroup is eᵢ + eⱼ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_root_negativeSum {m : ℕ} {i j : Fin m} (hij : i < j) : (diagonalRootDatum m).root (GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij) = -(Finsupp.single { down := i } 1 + Finsupp.single { down := j } 1)

The root of the negative sum root subgroup is -(eᵢ + eⱼ).

The coroots in coordinates

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coroot_positiveLong {m : ℕ} (i : Fin m) : (diagonalRootDatum m).coroot (GLSymplecticFin.RootSubgroupIndex.positiveLong i) = Pi.single { down := i } 1

The coroot of the long root 2eᵢ is the halved cocharacter eᵢ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coroot_negativeLong {m : ℕ} (i : Fin m) : (diagonalRootDatum m).coroot (GLSymplecticFin.RootSubgroupIndex.negativeLong i) = -Pi.single { down := i } 1

The coroot of the long root -2eᵢ is -eᵢ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coroot_difference {m : ℕ} {i j : Fin m} (hij : i ≠ j) : (diagonalRootDatum m).coroot (GLSymplecticFin.RootSubgroupIndex.difference i j hij) = Pi.single { down := i } 1 - Pi.single { down := j } 1

The coroot of the short root eᵢ - eⱼ is the cocharacter eᵢ - eⱼ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coroot_positiveSum {m : ℕ} {i j : Fin m} (hij : i < j) : (diagonalRootDatum m).coroot (GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij) = Pi.single { down := i } 1 + Pi.single { down := j } 1

The coroot of the short root eᵢ + eⱼ is the cocharacter eᵢ + eⱼ.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coroot_negativeSum {m : ℕ} {i j : Fin m} (hij : i < j) : (diagonalRootDatum m).coroot (GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij) = -(Pi.single { down := i } 1 + Pi.single { down := j } 1)

The coroot of the short root -(eᵢ + eⱼ) is the cocharacter -(eᵢ + eⱼ).

The reflections in coordinates

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflection_positiveLong_apply {m : ℕ} (i : Fin m) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (a : ULift.{u, 0} (Fin m)) : ((RootPairing.reflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveLong i)) x) a = if a = { down := i } then -x a else x a

Reflection in the long root 2eᵢ negates the i-th coordinate.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflection_negativeLong_apply {m : ℕ} (i : Fin m) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (a : ULift.{u, 0} (Fin m)) : ((RootPairing.reflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.negativeLong i)) x) a = if a = { down := i } then -x a else x a

Reflection in the long root -2eᵢ negates the i-th coordinate.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflection_difference_apply {m : ℕ} {i j : Fin m} (hij : i ≠ j) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (a : ULift.{u, 0} (Fin m)) : ((RootPairing.reflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.difference i j hij)) x) a = x ((Equiv.swap { down := i } { down := j }) a)

Reflection in the short root eᵢ - eⱼ transposes the i-th and j-th coordinates.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflection_positiveSum_apply {m : ℕ} {i j : Fin m} (hij : i < j) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (a : ULift.{u, 0} (Fin m)) : ((RootPairing.reflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij)) x) a = if a = { down := i } ∨ a = { down := j } then -x ((Equiv.swap { down := i } { down := j }) a) else x a

Reflection in the short root eᵢ + eⱼ transposes the i-th and j-th coordinates and negates both.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_reflection_negativeSum_apply {m : ℕ} {i j : Fin m} (hij : i < j) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (a : ULift.{u, 0} (Fin m)) : ((RootPairing.reflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij)) x) a = if a = { down := i } ∨ a = { down := j } then -x ((Equiv.swap { down := i } { down := j }) a) else x a

Reflection in the short root -(eᵢ + eⱼ) agrees with reflection in eᵢ + eⱼ.

The coreflections in coordinates

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coreflection_positiveLong_apply {m : ℕ} (i : Fin m) (x : ULift.{u, 0} (Fin m) → ℤ) (a : ULift.{u, 0} (Fin m)) : (RootPairing.coreflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveLong i)) x a = if a = { down := i } then -x a else x a

Coreflection in the long root 2eᵢ negates the i-th coordinate.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coreflection_negativeLong_apply {m : ℕ} (i : Fin m) (x : ULift.{u, 0} (Fin m) → ℤ) (a : ULift.{u, 0} (Fin m)) : (RootPairing.coreflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.negativeLong i)) x a = if a = { down := i } then -x a else x a

Coreflection in the long root -2eᵢ negates the i-th coordinate.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coreflection_difference_apply {m : ℕ} {i j : Fin m} (hij : i ≠ j) (x : ULift.{u, 0} (Fin m) → ℤ) (a : ULift.{u, 0} (Fin m)) : (RootPairing.coreflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.difference i j hij)) x a = x ((Equiv.swap { down := i } { down := j }) a)

Coreflection in the short root eᵢ - eⱼ transposes the i-th and j-th coordinates.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coreflection_positiveSum_apply {m : ℕ} {i j : Fin m} (hij : i < j) (x : ULift.{u, 0} (Fin m) → ℤ) (a : ULift.{u, 0} (Fin m)) : (RootPairing.coreflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij)) x a = if a = { down := i } ∨ a = { down := j } then -x ((Equiv.swap { down := i } { down := j }) a) else x a

Coreflection in the short root eᵢ + eⱼ transposes the i-th and j-th coordinates and negates both.

@[simp]

theorem TauCeti.Symplectic.diagonalRootDatum_coreflection_negativeSum_apply {m : ℕ} {i j : Fin m} (hij : i < j) (x : ULift.{u, 0} (Fin m) → ℤ) (a : ULift.{u, 0} (Fin m)) : (RootPairing.coreflection (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij)) x a = if a = { down := i } ∨ a = { down := j } then -x ((Equiv.swap { down := i } { down := j }) a) else x a

Coreflection in the short root -(eᵢ + eⱼ) agrees with coreflection in eᵢ + eⱼ.

The roots as characters of the diagonal torus

theorem TauCeti.Symplectic.charOfPoint_ofAdd_diagonalRootDatum_root {m : ℕ} {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (r : GLSymplecticFin.RootSubgroupIndex m) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)) →ₐ[R] A)) : (DiagonalizableGroup.charOfPoint t.ofConv) (Multiplicative.ofAdd ((diagonalRootDatum m).root r)) = r.character (GeneralLinear.diagonalTorusCoordinates (SplitTorus.pointsMulEquiv t))

The roots are the characters of the diagonal torus on the root subgroups. Evaluated at a point of the diagonal torus, the root of diagonalRootDatum indexed by a root subgroup is the character by which conjugation by that point rescales the subgroup.

theorem TauCeti.Symplectic.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv_eq_root {m : ℕ} {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (r : GLSymplecticFin.RootSubgroupIndex m) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)) →ₐ[R] A)) (c : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : diagonalTorusPoints t * (rootSubgroupPoints r) c * (diagonalTorusPoints t)⁻¹ = (rootSubgroupPoints r) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑((DiagonalizableGroup.charOfPoint t.ofConv) (Multiplicative.ofAdd ((diagonalRootDatum m).root r))) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv c))))

The symplectic pinning equation, with the roots of diagonalRootDatum. Conjugation by a point of the diagonal torus scales the parameter of each root subgroup by the value of its root.