Dimensions of closed subgroups

A proper closed subgroup of a reduced geometrically connected affine group of finite type has strictly smaller dimension. In coordinate rings, a nonzero Hopf ideal I satisfies dim (H ⧸ I) + 1 ≤ dim H. The subgroup may be disconnected or non-smooth. Reducedness of the ambient group matters: a proper infinitesimal subgroup can have the same dimension.

For smooth ambient groups and smooth closed subgroups, group dimension equals Lie dimension, so the dimension drop is an inequality of natural numbers. This provides a measure for induction through proper smooth closed subgroups, including reduced identity components of closed subgroups. The connectedness assumption is only on the ambient group, and no perfectness assumption on the field is needed.

The proof uses irreducibility of geometrically connected affine groups and Mathlib's ringKrullDim_succ_le_of_surjective: a nonzero function in the defining ideal is a non-zero-divisor in the ambient coordinate domain.

A smooth closed subgroup has the dimension of its Lie algebra, computed inside the Lie algebra of the ambient group (TauCeti.HopfIdeal.ringKrullDim_quotient_eq_finrank_lieSubalgebra_of_smooth). Over a field of characteristic zero every closed subgroup of a finite-type affine group is smooth, by Cartier's theorem, so this applies to all of them (TauCeti.HopfIdeal.ringKrullDim_quotient_eq_finrank_lieSubalgebra). This turns dimensions of stabilizers and centralizers into linear algebra.

References

• A. Borel, Linear Algebraic Groups, §11.1 (induction on dimension for Borel conjugacy).
• J. S. Milne, Algebraic Groups (2017), §§1 and 2 (connected groups and dimension).

theorem TauCeti.HopfIdeal.ringKrullDim_quotient_add_one_le {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) [IsReduced ↑H] (hH : geometricallyConnectedCommHopfAlgProperty k H) (hI : I ≠ ⊥) : ringKrullDim (↑H ⧸ I.toIdeal) + 1 ≤ ringKrullDim ↑H

A proper closed subgroup of a reduced geometrically connected affine group has dimension at least one less than the ambient group. The subgroup need not be smooth or connected.

theorem TauCeti.HopfIdeal.finrank_quotientLie_lt {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) [Algebra.Smooth k ↑H] [Algebra.Smooth k (↑H ⧸ I.toIdeal)] (hH : geometricallyConnectedCommHopfAlgProperty k H) (hI : I ≠ ⊥) : Module.finrank k (Derivation k (↑H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (↑H ⧸ I.toIdeal) k)) < Module.finrank k (Derivation k (↑H) (Bialgebra.CounitAlgebra k (↑H) k))

A proper smooth closed subgroup of a smooth geometrically connected affine group has strictly smaller Lie dimension. The closed subgroup may be disconnected, and the base field may be imperfect.

theorem TauCeti.HopfIdeal.ringKrullDim_quotient_eq_finrank_lieSubalgebra_of_smooth {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) [Algebra.Smooth k (H ⧸ I.toIdeal)] : ringKrullDim (H ⧸ I.toIdeal) = ↑(Module.finrank k ↥I.lieSubalgebra)

A smooth closed subgroup of an affine group has the dimension of its Lie algebra, viewed inside the Lie algebra of the ambient group.

theorem TauCeti.HopfIdeal.ringKrullDim_quotient_eq_finrank_lieSubalgebra {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [CharZero k] (I : HopfIdeal k H) : ringKrullDim (H ⧸ I.toIdeal) = ↑(Module.finrank k ↥I.lieSubalgebra)

The dimension of a closed subgroup in characteristic zero. Over a field of characteristic zero, every closed subgroup of a finite-type affine group has the dimension of its Lie algebra, viewed inside the Lie algebra of the ambient group. The closed subgroup need not be connected.