Smoothness of the symplectic isotropic flag subgroup

The standard complete isotropic flag stabilizer in Sp₂ₘ is smooth over every commutative ring. Its matrix points lift across square-zero quotients by lifting the upper-triangular Levi factor and the symmetric upper-unipotent block. Finite presentation follows from the finite set of flag equations in the smooth symplectic coordinate algebra.

This gives the smoothness condition needed to recognize the flag stabilizer as a Borel subgroup and to use it in a symplectic pinning. Characteristic two requires no exception.

The infinitesimal criterion follows the organization of TauCeti.Algebra.AlgebraicGroup.Symplectic.Smooth.

References

• SGA 3, Exposé XXII, for the split symplectic group and its Borel subgroups.
• J. S. Milne, Algebraic Groups (2017), §24.6.

instance TauCeti.Symplectic.IsotropicFlag.instSmoothCoordinateHopfAlgebra (R : Type u) [CommRing R] (m : ℕ) : Algebra.Smooth R ↑(coordinateHopfAlgebra R m)

The coordinate algebra of the standard complete isotropic flag stabilizer in Sp₂ₘ is smooth over every commutative base ring, in every rank.

theorem TauCeti.Symplectic.IsotropicFlag.smoothCommHopfAlgProperty_coordinateHopfAlgebra (R : Type u) [CommRing R] (m : ℕ) : smoothCommHopfAlgProperty R (coordinateHopfAlgebra R m)

The commutative Hopf algebra representing the standard complete isotropic flag stabilizer in Sp₂ₘ satisfies the smoothness object property over every commutative base ring.