Krull dimension and Lie dimension of an affine group

For an affine group of finite type over an algebraically closed field, translation identifies the heights of all maximal ideals with the height of the augmentation ideal. Thus the dimension of the group is its local dimension at the identity. Krull's height theorem bounds this by the dimension of its Lie algebra, with equality exactly when the local ring at the identity is regular. No reducedness, smoothness, or connectedness is assumed.

These are the dimension comparisons underlying the tangent-space criterion for smoothness.

References

• J. S. Milne, Algebraic Groups (2017), §10.a.
• M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Chapter 11.

theorem TauCeti.HopfAlgebra.ringKrullDim_eq_height_augmentation {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] : ringKrullDim H = ↑(Bialgebra.AugmentationIdeal k H).height

The dimension of an affine group over an algebraically closed field equals the height of its augmentation ideal.

@[simp]

theorem TauCeti.HopfAlgebra.ringKrullDim_augmentationStalk {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] : ringKrullDim ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (Bialgebra.augmentationPoint k H)) = ringKrullDim H

The local ring at the identity of a finite-type affine group over an algebraically closed field has the same dimension as the group.

theorem TauCeti.HopfAlgebra.ringKrullDim_le_finrank_lie {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] : ringKrullDim H ≤ ↑(Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k)))

The dimension of a finite-type affine group over an algebraically closed field is at most the dimension of its Lie algebra. This includes non-reduced group schemes.

theorem TauCeti.HopfAlgebra.isRegularLocalRing_augmentationStalk_iff {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] : IsRegularLocalRing ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (Bialgebra.augmentationPoint k H)) ↔ ↑(Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k))) = ringKrullDim H

Lie dimension equals group dimension exactly when the local ring at the identity is regular, for a finite-type affine group over an algebraically closed field.