Tangent equations of symplectic weight-parabolic intersections

Intersecting the symplectic group with a general-linear weight parabolic cuts out the filtration-preserving symplectic tangent matrices. The equations are stated in paired coordinates, so the same criterion can be used for self-dual flag orders rather than mistakenly imposing upper triangularity in the original paired basis order.

On coordinate rings the intersection is the image of the general-linear parabolic's Hopf ideal under the symplectic quotient map. The calculation uses HopfIdeal.lieSubalgebra_map and the general-linear weight-parabolic tangent criterion. It requires neither smoothness of the intersection nor a reduced coefficient ring. These tangent equations determine containment of adjoint root spaces in flag stabilizers.

References

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

theorem TauCeti.Symplectic.mem_lieSubalgebra_map_weightParabolicDefiningHopfIdeal_iff {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : ℕ} (w : Fin (m + m) → ℤ) (d : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B)) : d ∈ ((GeneralLinear.weightParabolicDefiningHopfIdeal R w).map (CommHopfAlgCat.Hom.hom (coordinateMap R m))).lieSubalgebra ↔ (↑((tangentMatrix m) d)).BlockTriangular (⇑OrderDual.toDual ∘ w ∘ ⇑finSumFinEquiv)

A symplectic tangent vector belongs to the inverse image of a general-linear weight parabolic precisely when its paired matrix preserves the induced weight filtration. The weights can encode any order, including the complete self-dual flag order.