Smooth unipotent affine groups

A smooth finite-type affine group over a field is unipotent when every point over an algebraic closure is a unipotent element. On coordinate Hopf algebras, a geometric point is an algebra map H →ₐ[k] AlgebraicClosure k, and its action on every finite-dimensional comodule supplies the representation-theoretic test for unipotence. Smoothness is included explicitly because geometric points alone do not detect infinitesimal structure in nonreduced group schemes.

This file packages the geometric-point criterion as an object property on commutative Hopf algebras, separately from smoothness, and combines the two properties for the finite-type smooth case. It also packages the smooth conjunction as a full subcategory. The equivalent nilpotence and Jordan-factor characterizations make the pointwise property usable without unfolding it.

This pointwise criterion is not offered as a definition for nonreduced group schemes: for example, both αₚ and μₚ have only the identity as an algebraic-closure-valued point in characteristic p, although only αₚ is unipotent scheme-theoretically. A future scheme-theoretic definition must instead detect infinitesimal points.

Main declarations

• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty: the property that every geometric point is unipotent; this is used together with smoothness.
• TauCeti.smoothUnipotentCommHopfAlgProperty: the geometric unipotence property for smooth finite-type commutative Hopf algebras over a field.
• geometricallyUnipotentPointsCommHopfAlgProperty_iff_forall_isNilpotent_endOfPoint_sub_one: the criterion that every geometric point acts with nilpotent difference from the identity.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_forall_unipotentPart_eq_self and TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_forall_semisimplePart_eq_one: the pointwise Jordan characterizations.
• TauCeti.SmoothUnipotentCommHopfAlgCat: the full subcategory of smooth unipotent coordinate Hopf algebras.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.

This supplies the smooth case of the geometric definition required by Layer 5, "Unipotent groups", of the ReductiveGroups roadmap.

def TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (CommHopfAlgCat k)

The object property asserting that every algebraic-closure-valued point acts unipotently in every finite-dimensional representation.

This geometric-point criterion is kept separate from smoothness, as required by the roadmap. It is not by itself a definition of unipotence for nonreduced group schemes, whose infinitesimal structure is invisible to algebraic-closure-valued points.

Equations

• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty k H = ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), TauCeti.HopfAlgebra.IsUnipotentPoint g

@[simp]

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyUnipotentPointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), HopfAlgebra.IsUnipotentPoint g

Membership in the geometric-point unipotence property means that every algebraic-closure-valued point acts unipotently in every finite-dimensional representation.

instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatGeometricallyUnipotentPointsCommHopfAlgProperty (k : Type u) [Field k] : (geometricallyUnipotentPointsCommHopfAlgProperty k).IsClosedUnderIsomorphisms

The geometric-point unipotence property is invariant under isomorphisms of commutative Hopf algebras.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_forall_isNilpotent_endOfPoint_sub_one (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyUnipotentPointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)) (M : FGComoduleCat k ↑H), IsNilpotent (Comodule.endOfPoint (↑M) g.ofConv - 1)

Every geometric point is unipotent exactly when every such point acts with nilpotent difference from the identity in every finite-dimensional comodule.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_forall_unipotentPart_eq_self (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyUnipotentPointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), HopfAlgebra.Point.unipotentPart k (↑H) (AlgebraicClosure k) g = g

Every geometric point is unipotent exactly when its unipotent part is the point itself.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_forall_semisimplePart_eq_one (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyUnipotentPointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), HopfAlgebra.Point.semisimplePart k (↑H) (AlgebraicClosure k) g = 1

Every geometric point is unipotent exactly when its semisimple part is the identity.

def TauCeti.smoothUnipotentCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat k)

The object property selecting smooth finite-type affine groups whose every geometric point is unipotent.

The point predicate tests the action on every finitely generated comodule, which over a field is the finite-dimensional representation-theoretic definition. The smoothness condition excludes the infinitesimal nonreduced obstruction that algebraic-closure-valued points cannot detect.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.smoothUnipotentCommHopfAlgProperty_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : smoothUnipotentCommHopfAlgProperty k H ↔ Algebra.Smooth k ↑H.obj ∧ ∀ (g : WithConv (↑H.obj →ₐ[k] AlgebraicClosure k)), HopfAlgebra.IsUnipotentPoint g

Membership in the smooth unipotent property means smoothness together with every algebraic-closure-valued point acting unipotently in every finite-dimensional representation.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatSmoothUnipotentCommHopfAlgProperty (k : Type u) [Field k] : (smoothUnipotentCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Smooth geometric-point unipotence is invariant under isomorphisms of finite-type commutative Hopf algebras.

@[reducible, inline]

abbrev TauCeti.SmoothUnipotentCommHopfAlgCat (k : Type u) [Field k] : Type (max u (u_1 + 1))

The category of smooth finite-type unipotent coordinate Hopf algebras over a field.

Equations

• TauCeti.SmoothUnipotentCommHopfAlgCat k = (TauCeti.smoothUnipotentCommHopfAlgProperty k).FullSubcategory