The diagonal torus in the symplectic group

For a family of units t : Fin m → Rˣ, the block-diagonal matrix

diag(t₀, …, tₘ₋₁, t₀⁻¹, …, tₘ₋₁⁻¹)

preserves the standard alternating form. This file packages these matrices as the homomorphism TauCeti.GLSymplecticFin.diagonal into Sp₂ₘ(R) and computes conjugation on every standard symplectic root subgroup. A symplectic matrix belongs to this image exactly when its underlying matrix is diagonal.

The five root characters are tᵢ², tᵢ⁻², tᵢtⱼ⁻¹, tᵢtⱼ, and (tᵢtⱼ)⁻¹ for the roots 2eᵢ, -2eᵢ, eᵢ-eⱼ, eᵢ+eⱼ, and -eᵢ-eⱼ, respectively. The uniform theorem TauCeti.GLSymplecticFin.diagonal_mul_rootSubgroup_mul_inv records the corresponding pinning equation.

Main declarations

• TauCeti.GLSymplecticFin.diagonal: the diagonal split-torus homomorphism into the symplectic matrix group.
• TauCeti.GLSymplecticFin.diagonalTorus: the subgroup of paired diagonal matrices, with membership characterized by TauCeti.GLSymplecticFin.mem_diagonalTorus_iff.
• TauCeti.GLSymplecticFin.RootSubgroupIndex.character: the character of the diagonal torus belonging to a root.
• TauCeti.GLSymplecticFin.diagonal_mul_rootSubgroup_mul_inv: conjugation scales a root parameter by its root character.

References

• J. S. Milne, Algebraic Groups (2017), §23 and §24.6.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3.

These conjugation calculations supply the root-action equations used in the standard type-C pinning.

def TauCeti.GLSymplecticFin.diagonalCoordinates {m : ℕ} {R : Type u} [Monoid R] (t : Fin m → Rˣ) (k : Fin (m + m)) : Rˣ

The diagonal entries of a standard symplectic torus element in Fin (m + m) coordinates: t i on the first block and (t i)⁻¹ on the second.

Equations

• TauCeti.GLSymplecticFin.diagonalCoordinates t k = Sum.elim t (fun (i : Fin m) => (t i)⁻¹) (finSumFinEquiv.symm k)

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalCoordinates_castAdd {m : ℕ} {R : Type u} [Monoid R] (t : Fin m → Rˣ) (i : Fin m) : diagonalCoordinates t (Fin.castAdd m i) = t i

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalCoordinates_addNat {m : ℕ} {R : Type u} [Monoid R] (t : Fin m → Rˣ) (i : Fin m) : diagonalCoordinates t (i.addNat m) = (t i)⁻¹

noncomputable def TauCeti.GLSymplecticFin.diagonal {m : ℕ} {R : Type u} [CommRing R] : (Fin m → Rˣ) →* ↥(GLSymplecticFin m R)

The diagonal split torus in the standard symplectic matrix group. It sends t to the diagonal matrix with entries t i on the first block and (t i)⁻¹ on the second.

Equations

• TauCeti.GLSymplecticFin.diagonal = TauCeti.GLSymplecticFin.leviHom.comp TauCeti.diagGL

@[simp]

theorem TauCeti.GLSymplecticFin.coe_diagonal {m : ℕ} {R : Type u} [CommRing R] (t : Fin m → Rˣ) : ↑(diagonal t) = diagGL (diagonalCoordinates t)

The underlying general-linear matrix of a symplectic diagonal element.

theorem TauCeti.GLSymplecticFin.diagonal_injective {m : ℕ} {R : Type u} [CommRing R] : Function.Injective ⇑diagonal

The symplectic diagonal homomorphism is injective.

noncomputable def TauCeti.GLSymplecticFin.diagonalTorus (R : Type u) [CommRing R] (m : ℕ) : Subgroup ↥(GLSymplecticFin m R)

The paired diagonal torus in the symplectic group: the image of the diagonal homomorphism.

Equations

• TauCeti.GLSymplecticFin.diagonalTorus R m = TauCeti.GLSymplecticFin.diagonal.range

theorem TauCeti.GLSymplecticFin.mem_diagonalTorus_iff_exists_diagonal {m : ℕ} {R : Type u} [CommRing R] {g : ↥(GLSymplecticFin m R)} : g ∈ diagonalTorus R m ↔ ∃ (t : Fin m → Rˣ), diagonal t = g

A symplectic matrix belongs to the diagonal torus exactly when it is a paired diagonal matrix for some family of units.

instance TauCeti.GLSymplecticFin.instIsMulCommutativeDiagonalTorus {m : ℕ} {R : Type u} [CommRing R] : IsMulCommutative ↥(diagonalTorus R m)

The paired diagonal torus is commutative, as the image of the coordinatewise units.

noncomputable def TauCeti.GLSymplecticFin.diagonalTorusEquiv (R : Type u) [CommRing R] (m : ℕ) : (Fin m → Rˣ) ≃* ↥(diagonalTorus R m)

The paired diagonal torus is the group of coordinatewise units.

Equations

• TauCeti.GLSymplecticFin.diagonalTorusEquiv R m = MonoidHom.ofInjective ⋯

@[simp]

theorem TauCeti.GLSymplecticFin.coe_diagonalTorusEquiv_apply {m : ℕ} {R : Type u} [CommRing R] (t : Fin m → Rˣ) : ↑((diagonalTorusEquiv R m) t) = diagonal t

The torus element attached to a family of units is its paired diagonal matrix.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_diagonalTorusEquiv_symm_apply {m : ℕ} {R : Type u} [CommRing R] (g : ↥(diagonalTorus R m)) (i : Fin m) : ↑((diagonalTorusEquiv R m).symm g i) = ↑↑↑g (Fin.castAdd m i) (Fin.castAdd m i)

The i-th coordinate of a torus element is its i-th diagonal entry in the first block.

@[simp]

theorem TauCeti.GLSymplecticFin.mem_diagonalTorus_iff {m : ℕ} {R : Type u} [CommRing R] {g : ↥(GLSymplecticFin m R)} : g ∈ diagonalTorus R m ↔ (↑↑g).IsDiag

A symplectic matrix belongs to the paired diagonal torus exactly when it is diagonal.

@[simp]

theorem TauCeti.GLSymplecticFin.map_diagonal {m : ℕ} {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (t : Fin m → Rˣ) : (map m R f) (diagonal t) = diagonal fun (i : Fin m) => (Units.map ↑f) (t i)

The diagonal symplectic matrix commutes with change of coefficient ring.

def TauCeti.GLSymplecticFin.RootSubgroupIndex.character {m : ℕ} {R : Type u} [CommMonoid R] (root : RootSubgroupIndex m) : (Fin m → Rˣ) →* Rˣ

The character of the standard symplectic diagonal torus belonging to a root.

Equations

• (TauCeti.GLSymplecticFin.RootSubgroupIndex.positiveLong i).character = { toFun := fun (t : Fin m → Rˣ) => t i * t i, map_one' := ⋯, map_mul' := ⋯ }
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.negativeLong i).character = { toFun := fun (t : Fin m → Rˣ) => (t i * t i)⁻¹, map_one' := ⋯, map_mul' := ⋯ }
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.difference i j hij).character = { toFun := fun (t : Fin m → Rˣ) => t i * (t j)⁻¹, map_one' := ⋯, map_mul' := ⋯ }
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij).character = { toFun := fun (t : Fin m → Rˣ) => t i * t j, map_one' := ⋯, map_mul' := ⋯ }
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij).character = { toFun := fun (t : Fin m → Rˣ) => (t i * t j)⁻¹, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.character_positiveLong {m : ℕ} {R : Type u} [CommMonoid R] (i : Fin m) (t : Fin m → Rˣ) : (positiveLong i).character t = t i * t i

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.character_negativeLong {m : ℕ} {R : Type u} [CommMonoid R] (i : Fin m) (t : Fin m → Rˣ) : (negativeLong i).character t = (t i * t i)⁻¹

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.character_difference {m : ℕ} {R : Type u} [CommMonoid R] (i j : Fin m) (hij : i ≠ j) (t : Fin m → Rˣ) : (difference i j hij).character t = t i * (t j)⁻¹

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.character_positiveSum {m : ℕ} {R : Type u} [CommMonoid R] (i j : Fin m) (hij : i < j) (t : Fin m → Rˣ) : (positiveSum i j hij).character t = t i * t j

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.character_negativeSum {m : ℕ} {R : Type u} [CommMonoid R] (i j : Fin m) (hij : i < j) (t : Fin m → Rˣ) : (negativeSum i j hij).character t = (t i * t j)⁻¹

theorem TauCeti.GLSymplecticFin.diagonal_mul_rootSubgroup_mul_inv {m : ℕ} {R : Type u} [CommRing R] (root : RootSubgroupIndex m) (t : Fin m → Rˣ) (c : Multiplicative R) : diagonal t * root.hom c * (diagonal t)⁻¹ = root.hom (Multiplicative.ofAdd (↑(root.character t) * Multiplicative.toAdd c))

Conjugation by a diagonal symplectic matrix acts on each root subgroup through its root character.