Symplectic root lines and the characters of matrix entries

An entry of a normalized symplectic root matrix is nonzero exactly when the difference of its two paired standard weights is that root of the diagonal root datum. The test uses the integral matrix, so its support remains meaningful in characteristic two. Consequently a symplectic Lie matrix with entries only of a specified root character is a unique scalar multiple of the corresponding normalized root matrix, over every commutative coefficient ring.

This identifies the character-based root lines with the support-based root lines used by root-subgroup differentials. Together with an entrywise adjoint-weight criterion it recognizes the root spaces which a symplectic pinning must trivialize.

References

• J. S. Milne, Algebraic Groups (2017), §§21.1 and 24.6.
• B. Conrad, Reductive Group Schemes (2014), §5.1.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.

The scalar-multiple recognition uses TauCeti.GLSymplecticFin.RootSubgroupIndex.existsUnique_eq_tangentMatrix_iff.

noncomputable def TauCeti.Symplectic.pairedCoordinateWeight {m : ℕ} : Fin m ⊕ Fin m → ULift.{u, 0} (Fin m) →₀ ℤ

The integral character of a paired coordinate of the standard symplectic representation. The two halves have weights eᵢ and -eᵢ; a matrix entry (a, b) has character pairedCoordinateWeight a - pairedCoordinateWeight b.

Equations

• TauCeti.Symplectic.pairedCoordinateWeight = Sum.elim (fun (i : Fin m) => Finsupp.single { down := i } 1) fun (i : Fin m) => Finsupp.single { down := i } (-1)

@[simp]

theorem TauCeti.Symplectic.pairedCoordinateWeight_inl {m : ℕ} (i : Fin m) : pairedCoordinateWeight (Sum.inl i) = Finsupp.single { down := i } 1

A coordinate in the first half has the positive standard weight.

@[simp]

theorem TauCeti.Symplectic.pairedCoordinateWeight_inr {m : ℕ} (i : Fin m) : pairedCoordinateWeight (Sum.inr i) = Finsupp.single { down := i } (-1)

A coordinate in the second half has the negative standard weight.

theorem TauCeti.Symplectic.tangentMatrix_apply_ne_zero_iff_root_eq {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) (a b : Fin m ⊕ Fin m) : root.tangentMatrix 1 a b ≠ 0 ↔ (diagonalRootDatum m).root root = pairedCoordinateWeight a - pairedCoordinateWeight b

The integral support of a normalized root matrix consists exactly of the entries whose paired-weight difference is that root of the symplectic diagonal root datum.

theorem TauCeti.Symplectic.tangentMatrix_apply_eq_zero_iff_root_ne {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) (a b : Fin m ⊕ Fin m) : root.tangentMatrix 1 a b = 0 ↔ (diagonalRootDatum m).root root ≠ pairedCoordinateWeight a - pairedCoordinateWeight b

A normalized integral root matrix vanishes exactly at entries whose paired-weight difference is not its root of the symplectic diagonal root datum.

theorem TauCeti.Symplectic.existsUnique_eq_tangentMatrix_iff {m : ℕ} {R : Type u_1} [CommRing R] (root : GLSymplecticFin.RootSubgroupIndex m) {A : Matrix (Fin m ⊕ Fin m) (Fin m ⊕ Fin m) R} (hA : A ∈ LieAlgebra.Symplectic.sp (Fin m) R) : (∃! c : R, A = root.tangentMatrix c) ↔ ∀ (a b : Fin m ⊕ Fin m), (diagonalRootDatum m).root root ≠ pairedCoordinateWeight a - pairedCoordinateWeight b → A a b = 0

A symplectic Lie matrix has entries only of a given root character exactly when it is a unique scalar multiple of that root's normalized matrix. This holds over arbitrary commutative rings, including in characteristic two.