Recognition of symplectic root lines by matrix support

A symplectic Lie matrix supported at the positions of a standard root matrix is a unique scalar multiple of that matrix. For short roots, the symplectic equation forces the two entries to have the prescribed relative sign. The support is tested on the integral matrix, so the criterion remains valid in characteristic two and over rings with nilpotents. It is the matrix recognition step in identifying adjoint root spaces with the images of root-subgroup differentials.

The normalization is GLSymplecticFin.RootSubgroupIndex.tangentMatrix; the block criterion is Matrix.mem_symplecticLieAlgebra_iff.

References

• J. S. Milne, Algebraic Groups (2017), §§21.1 and 24.6.
• R. W. Carter, Simple Groups of Lie Type (1972), §11.3.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_apply_eq_zero_of_int_eq_zero {m : ℕ} {R : Type u_1} [CommRing R] (root : RootSubgroupIndex m) (c : R) (a b : Fin m ⊕ Fin m) (h : root.tangentMatrix 1 a b = 0) : root.tangentMatrix c a b = 0

Every scalar multiple of a root matrix vanishes outside its integral support.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.existsUnique_eq_tangentMatrix_iff {m : ℕ} {R : Type u_1} [CommRing R] (root : 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), root.tangentMatrix 1 a b = 0 → A a b = 0

A symplectic Lie matrix lies on a root line exactly when it vanishes outside the corresponding integral support. The scalar parameter is unique over every ring.