Smooth closed subgroups with the full Lie algebra

Let G be a smooth connected affine group of finite type over an algebraically closed field, and H ≤ G a smooth closed subgroup with Lie(H) = Lie(G). Then H = G.

The subgroup H need not be connected, so the comparison of smooth connected closed subgroups by their Lie algebras does not apply to it directly. Its identity component H° is smooth and connected, and has the same Lie algebra as H: a tangent vector at the identity kills every idempotent, in particular the one cutting out H°. The coordinate map O(G) → O(H°) is then surjective with surjective differential, so it is injective.

Main declarations

• TauCeti.HopfIdeal.lieSubalgebra_identityComponentHopfIdeal_eq_top: the identity component has the same Lie algebra as the group.
• TauCeti.HopfIdeal.eq_bot_of_lieSubalgebra_eq_top: a smooth closed subgroup of a smooth connected group with the full Lie algebra is the whole group.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 10.
• J. E. Humphreys, Linear Algebraic Groups, §13.

theorem TauCeti.HopfIdeal.lieSubalgebra_identityComponentHopfIdeal_eq_top {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} : HopfAlgebra.identityComponentHopfIdeal.lieSubalgebra = ⊤

The identity component of a finite-type affine group over an algebraically closed field has the same Lie algebra as the group.

theorem TauCeti.HopfIdeal.eq_bot_of_lieSubalgebra_eq_top {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [Algebra.Smooth k ↑H.obj] [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : HopfIdeal k ↑H.obj) [Algebra.Smooth k (↑H.obj ⧸ I.toIdeal)] (hI : I.lieSubalgebra = ⊤) : I = ⊥

A smooth closed subgroup of a smooth connected affine group over an algebraically closed field is the whole group as soon as its Lie algebra is the whole Lie algebra.

The order on Hopf ideals reverses inclusion of closed subgroups, so I = ⊥ says that the closed subgroup cut out by I is everything.