Smooth connected closed subgroups with equal tangent spaces

A surjective map of coordinate Hopf algebras represents a closed immersion of affine groups. When both groups are smooth and connected, surjectivity on tangent spaces forces this closed immersion to be an isomorphism.

The proof uses the conormal module of the surjection. Smoothness makes it finite projective over the target. Its fibre at the identity is zero, because its split injection into the relative cotangent space is zero there. Projective-module rank is locally constant, so connectedness of the target makes the conormal module vanish globally. The kernel is then idempotent; connectedness of the source and the counit condition force it to be zero.

Main declaration

• TauCeti.HopfIdeal.ker_eq_bot_of_smooth_of_connected_of_conormalSubspace_eq_bot: a surjective Hopf map between smooth connected affine groups is injective when its conormal space vanishes.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 5.a and 10.a.
• A. Borel, Linear Algebraic Groups, Section 11.21.

This is the global equality step in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. It upgrades the infinitesimal equality supplied by the maximal-dimension construction to equality of closed subgroups.

theorem TauCeti.HopfIdeal.ker_eq_bot_of_smooth_of_connected_of_conormalSubspace_eq_bot {k H K : Type u} [Field k] [CommRing H] [CommRing K] [HopfAlgebra k H] [HopfAlgebra k K] [Algebra.FiniteType k H] (f : H →ₐc[k] K) (hf : Function.Surjective ⇑f) (hH_smooth : smoothCommHopfAlgProperty k ↧H) (hH_connected : ConnectedSpace (PrimeSpectrum H)) (hK_smooth : smoothCommHopfAlgProperty k ↧K) (hK_connected : ConnectedSpace (PrimeSpectrum K)) (hconormal : (ker f).conormalSubspace = ⊥) : ker f = ⊥

A surjective Hopf map between smooth connected affine groups is injective if its conormal space at the identity vanishes.

Equivalently, a smooth connected closed affine subgroup whose differential is surjective is the whole ambient group.