Recognition of symplectic root-subgroup tangent images

A tangent vector belongs to the image of a represented symplectic root subgroup exactly when its matrix entries of every different weight character vanish. This turns an entrywise adjoint-weight calculation into membership in the actual scheme-theoretic root-subgroup differential, over arbitrary coefficient algebras. The root characters are integral, so the criterion distinguishes them even in characteristic two.

The construction combines Symplectic.existsUnique_eq_tangentMatrix_iff with Symplectic.range_derivationCompLieHom_rootSubgroup_eq_span. Its normalization is the existing Symplectic.rootVector, rather than a separately chosen Lie vector.

References

• J. S. Milne, Algebraic Groups (2017), §§21.1 and 24.6.
• B. Conrad, Reductive Group Schemes (2014), §5.1.

theorem TauCeti.Symplectic.mem_range_derivationCompLieHom_rootSubgroup_iff {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) (d : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B)) : d ∈ (derivationCompLieHom (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap root))).range ↔ ∀ (a b : Fin m ⊕ Fin m), (diagonalRootDatum m).root root ≠ pairedCoordinateWeight a - pairedCoordinateWeight b → ↑((tangentMatrix m) d) a b = 0

The root-subgroup tangent image is cut out by vanishing of entries with a different weight character, without any restriction on characteristic or reducedness.