Extensions of smooth unipotent affine groups

Let f : H ⟶ K be a morphism of commutative Hopf algebras over a field k. In the contravariant affine-group dictionary it represents a homomorphism Spec K ⟶ Spec H. This file proves the pointwise extension principle: a point of Spec K is unipotent when its image in Spec H is unipotent and every point in the kernel of the homomorphism is unipotent.

The proof uses Jordan decomposition rather than a chosen representation. Naturality sends the semisimple part of the original point to the semisimple part of its unipotent image, hence to the identity. The semisimple part therefore belongs to the kernel closed subgroup. If every kernel point is unipotent, this semisimple point is both semisimple and unipotent, so it is the identity.

On coordinate rings, the kernel closed subgroup has algebra

K / K·f(H⁺),

implemented as CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f). The resulting object-property theorem says that geometric-point unipotence of Spec K is equivalent to that of the kernel whenever Spec H is geometrically unipotent. The final statements combine this with the explicit smoothness hypothesis used by smoothUnipotentCommHopfAlgProperty.

Main declarations

• TauCeti.HopfAlgebra.IsUnipotentPoint.of_mapDomain_of_kernel: the pointwise extension principle.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_of_kernel: geometric-point unipotence is closed under extensions.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_kernel: when the target is geometrically unipotent, the source is geometrically unipotent exactly when its kernel is.
• TauCeti.smoothUnipotentCommHopfAlgProperty_iff_smooth_and_kernel: the corresponding characterization for a smooth finite-type source.

References

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

This supplies the extension-closure step in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. Together with closed-subgroup and product closure, it is part of the subgroup calculus needed to construct and compare connected normal unipotent closed subgroups in the unipotent radical.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.of_mapDomain_of_kernel {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [CommRing K] [HopfAlgebra k K] [Field L] [Algebra k L] [PerfectField L] (f : H →ₐc[k] K) (g : WithConv (K →ₐ[k] L)) (himage : IsUnipotentPoint ((AlgHom.mapDomain f) g)) (hkernel : ∀ (s : WithConv (K →ₐ[k] L)), (AlgHom.mapDomain f) s = 1 → IsUnipotentPoint s) : IsUnipotentPoint g

A point is unipotent when its image is unipotent and every point in the kernel of the coordinate morphism is unipotent.

Here the kernel hypothesis is expressed pointwise: it applies to precisely those K-points whose precomposition along f is the identity H-point. The object-level results below identify this condition with points of the quotient by CommHopfAlgCat.kernelHopfIdeal.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_of_kernel (k : Type u) [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hH : geometricallyUnipotentPointsCommHopfAlgProperty k H) (hkernel : geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f))) : geometricallyUnipotentPointsCommHopfAlgProperty k K

Geometric-point unipotence is closed under extensions.

For the group homomorphism represented by f : H ⟶ K, assume that the target Spec H and the kernel Spec (K / K·f(H⁺)) have only unipotent geometric points. Then every geometric point of the source Spec K is unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty_iff_kernel (k : Type u) [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hH : geometricallyUnipotentPointsCommHopfAlgProperty k H) : geometricallyUnipotentPointsCommHopfAlgProperty k K ↔ geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f))

If the target of a homomorphism is geometrically unipotent, then its source is geometrically unipotent exactly when its kernel is.

The forward implication is closure under closed subgroups, applied to the quotient coordinate map. The reverse implication is the extension theorem above.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty_iff_smooth_and_kernel (k : Type u) [Field k] {H K : FiniteTypeCommHopfAlgCat k} (f : H ⟶ K) (hH : geometricallyUnipotentPointsCommHopfAlgProperty k H.obj) : smoothUnipotentCommHopfAlgProperty k K ↔ Algebra.Smooth k ↑K.obj ∧ geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient K.obj (CommHopfAlgCat.kernelHopfIdeal f.hom))

A smooth finite-type affine group with geometrically unipotent target is smooth unipotent exactly when the geometric points of its kernel are unipotent.

Smoothness of the source remains explicit. This theorem proves the unipotence part of extension closure; it does not assert smoothness of the middle group from exactness hypotheses that are not present in the coordinate morphism alone.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty_of_kernel (k : Type u) [Field k] {H K : FiniteTypeCommHopfAlgCat k} (f : H ⟶ K) (hH : geometricallyUnipotentPointsCommHopfAlgProperty k H.obj) (hkernel : geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient K.obj (CommHopfAlgCat.kernelHopfIdeal f.hom))) (hK : Algebra.Smooth k ↑K.obj) : smoothUnipotentCommHopfAlgProperty k K

A smooth finite-type source of a homomorphism is smooth unipotent when its target and kernel have only unipotent geometric points.