Lifting symplectic matrices

A symplectic matrix lifts across a quotient by a square-zero ideal. Starting with arbitrary lifts of its entries, the failure to preserve the standard alternating form is an alternating matrix with entries in the ideal. Its strict upper triangle gives an integral solution of the linearized symplectic equation; this avoids division by two and therefore works in characteristic two. The quadratic correction terms vanish because the ideal is square-zero.

Main declaration

• TauCeti.GLSymplectic.map_quotient_mk_surjective_of_sq_eq_bot: entrywise reduction modulo a square-zero ideal is surjective on symplectic groups.

References

• The Stacks Project, Tag 00TH, for the infinitesimal lifting criterion for formal smoothness.
• SGA 3, Exposé XXII, for the smooth split symplectic group scheme over ℤ.

This is the infinitesimal lifting input for the smoothness of the symplectic group scheme, a prerequisite for the Sp_{2n} reductivity example in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.GLSymplectic.map_quotient_mk_surjective_of_sq_eq_bot {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] (I : Ideal R) (hI : I ^ 2 = ⊥) : Function.Surjective ⇑(map l (Ideal.Quotient.mk I))

Every symplectic matrix modulo a square-zero ideal lifts to a symplectic matrix.

The result is valid over an arbitrary commutative ring, in every characteristic, and for the zero-dimensional symplectic group.