Comparing smooth connected closed subgroups by Lie dimension

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. A closed subgroup is encoded contravariantly by a Hopf ideal, so I ≤ J says that the subgroup cut out by I contains the one cut out by J. Lie dimension is antitone in the defining ideal, and this file proves that it detects equality among smooth connected closed subgroups: an inclusion which does not drop the Lie dimension is an equality.

The proof is the conormal-sequence argument. The quotient-to-quotient coordinate map is surjective, and equality of tangent-space dimensions makes it bijective on tangent Lie algebras, hence its conormal space vanishes; smoothness and connectedness then upgrade the infinitesimal statement to equality of Hopf ideals.

Two consequences follow formally. A member of maximal Lie dimension in a family of smooth connected closed subgroups is a maximal member of that family, and every nonempty such family has a maximal member. No closure hypothesis on the family is needed: unlike the product argument used for the unipotent and solvable radicals, this gives maximality rather than a greatest element.

Main declarations

• TauCeti.HopfIdeal.eq_of_le_of_finrank_quotientLie_le: an inclusion of smooth connected closed subgroups which does not drop the Lie dimension is an equality.
• TauCeti.HopfIdeal.minimal_of_finrank_quotientLie_maximal: a maximal-dimensional member of a family of smooth connected closed subgroups is a maximal member.
• TauCeti.HopfIdeal.exists_minimal_of_smooth_of_connected: every nonempty family of smooth connected closed subgroups has a maximal member.

References

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

theorem TauCeti.HopfIdeal.eq_of_le_of_finrank_quotientLie_le {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hIJ : I ≤ J) (hI_smooth : smoothCommHopfAlgProperty k ↧(↑H.obj ⧸ I.toIdeal)) (hI_connected : ConnectedSpace (PrimeSpectrum (↑H.obj ⧸ I.toIdeal))) (hJ_smooth : smoothCommHopfAlgProperty k ↧(↑H.obj ⧸ J.toIdeal)) (hJ_connected : ConnectedSpace (PrimeSpectrum (↑H.obj ⧸ J.toIdeal))) (hfinrank : Module.finrank k (Derivation k (↑H.obj ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (↑H.obj ⧸ I.toIdeal) k)) ≤ Module.finrank k (Derivation k (↑H.obj ⧸ J.toIdeal) (Bialgebra.CounitAlgebra k (↑H.obj ⧸ J.toIdeal) k))) : I = J

An inclusion of smooth connected closed subgroups which does not drop the Lie dimension is an equality.

The order on Hopf ideals reverses inclusion of the represented closed subgroups, so I ≤ J says that the subgroup cut out by I contains the one cut out by J, and the dimension hypothesis is the reverse of the automatic inequality.

theorem TauCeti.HopfIdeal.minimal_of_finrank_quotientLie_maximal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (P : HopfIdeal k ↑H.obj → Prop) (smooth : ∀ {K : HopfIdeal k ↑H.obj}, P K → smoothCommHopfAlgProperty k ↧(↑H.obj ⧸ K.toIdeal)) (connected : ∀ {K : HopfIdeal k ↑H.obj}, P K → ConnectedSpace (PrimeSpectrum (↑H.obj ⧸ K.toIdeal))) (hI : P I) (hmax : ∀ (K : HopfIdeal k ↑H.obj), P K → K ≤ I → Module.finrank k (Derivation k (↑H.obj ⧸ K.toIdeal) (Bialgebra.CounitAlgebra k (↑H.obj ⧸ K.toIdeal) k)) ≤ Module.finrank k (Derivation k (↑H.obj ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (↑H.obj ⧸ I.toIdeal) k))) : Minimal P I

A member of maximal Lie dimension in a family of smooth connected closed subgroups is a maximal member of that family.

Only the members contained in the given one need to be dimension-dominated by it, which is what makes the statement usable for families cut out by an auxiliary containment condition.

theorem TauCeti.HopfIdeal.exists_minimal_of_smooth_of_connected {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (P : HopfIdeal k ↑H.obj → Prop) (smooth : ∀ {K : HopfIdeal k ↑H.obj}, P K → smoothCommHopfAlgProperty k ↧(↑H.obj ⧸ K.toIdeal)) (connected : ∀ {K : HopfIdeal k ↑H.obj}, P K → ConnectedSpace (PrimeSpectrum (↑H.obj ⧸ K.toIdeal))) (hP : ∃ (I : HopfIdeal k ↑H.obj), P I) : ∃ (I : HopfIdeal k ↑H.obj), Minimal P I

Every nonempty family of smooth connected closed subgroups has a maximal member.

Maximality of the represented closed subgroup is minimality of its defining Hopf ideal. The Lie dimensions attained by the family form a nonempty set of natural numbers bounded by the Lie dimension of the ambient group, so a maximal-dimensional member exists and is maximal.