Unipotent points of an affine group

Let H be a Hopf algebra over a commutative semiring k and let K be a commutative k-algebra. A K-valued point g : H →ₐ[k] K acts on the scalar extension of every finitely generated H-comodule. Over a field, these are the finite-dimensional representations relevant to the geometric definition. This file calls g unipotent when every one of those linear automorphisms is unipotent, meaning that its difference from the identity is nilpotent.

For the commutative coordinate Hopf algebra of an affine group scheme, taking K to be an algebraic closure of k is precisely the representation-theoretic definition of a geometric unipotent element. The quantification over all finitely generated comodules is essential: testing nilpotence in the reduced coordinate ring would instead give the vacuous condition warned against in the ReductiveGroups roadmap.

The predicate is immediately exercised by its basic group-theoretic API. The identity is unipotent, as are inverses and natural or integer powers of unipotent points. Products are unipotent when the points commute, and unipotence is invariant under conjugation. These statements follow because every comodule point action is a group homomorphism and the corresponding closure properties hold in the general linear group. Unipotence is also preserved by precomposition along bialgebra morphisms, and hence invariant under bialgebra isomorphisms.

Main declarations

• TauCeti.HopfAlgebra.IsUnipotentPoint: a point acts unipotently in every finitely generated comodule.
• TauCeti.HopfAlgebra.isUnipotentPoint_iff_forall_isNilpotent_endOfPoint_sub_one: the equivalent nilpotence formulation using the underlying comodule action endomorphisms.
• TauCeti.HopfAlgebra.IsUnipotentPoint.inv, .mul_of_commute, .pow, and .zpow: closure under inversion, commuting products, and natural or integer powers.
• TauCeti.HopfAlgebra.isUnipotentPoint_inv_iff: a point is unipotent exactly when its inverse is.
• TauCeti.HopfAlgebra.isUnipotentPoint_conj_iff: invariance under conjugation.
• TauCeti.HopfAlgebra.IsUnipotentPoint.mapDomain: functoriality under precomposition by a bialgebra morphism.
• TauCeti.HopfAlgebra.isUnipotentPoint_mapDomain_iff: invariance under a bialgebra isomorphism of the coordinate algebra.

References

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

This is the elementwise definition required by Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. It uses the representation--comodule dictionary built in Layer 1.

def TauCeti.HopfAlgebra.IsUnipotentPoint {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : Prop

A point of a Hopf algebra valued in a commutative algebra is unipotent when it acts by a unipotent linear automorphism on the scalar extension of every finitely generated comodule.

When k is a field, these comodules are the finite-dimensional representations. Thus, when H is the commutative coordinate Hopf algebra of an affine group over k and K is an algebraic closure, this is the standard representation-theoretic definition of a geometric unipotent element.

Equations

• TauCeti.HopfAlgebra.IsUnipotentPoint g = ∀ (M : TauCeti.FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((TauCeti.Comodule.pointsAction ↑M) g)).IsUnipotent

theorem TauCeti.HopfAlgebra.isUnipotentPoint_def {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsUnipotentPoint g ↔ ∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).IsUnipotent

Unfolding the definition of a unipotent point gives unipotence of its action on every finite comodule.

theorem TauCeti.HopfAlgebra.isUnipotentPoint_iff_forall_isNilpotent_endOfPoint_sub_one {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsUnipotentPoint g ↔ ∀ (M : FGComoduleCat k H), IsNilpotent (Comodule.endOfPoint (↑M) g.ofConv - 1)

A point is unipotent exactly when each underlying point-action endomorphism minus the identity is nilpotent.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.mapDomain {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] {H' : Type w} [Semiring H'] [HopfAlgebra k H'] {g : WithConv (H' →ₐ[k] K)} (hg : IsUnipotentPoint g) (f : H →ₐc[k] H') : IsUnipotentPoint ((AlgHom.mapDomain f) g)

Precomposing a unipotent point with a bialgebra morphism gives a unipotent point.

theorem TauCeti.HopfAlgebra.isUnipotentPoint_mapDomain_iff {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] {H' : Type w} [Semiring H'] [HopfAlgebra k H'] (e : H ≃ₐc[k] H') (g : WithConv (H' →ₐ[k] K)) : IsUnipotentPoint ((AlgHom.mapDomain ↑e) g) ↔ IsUnipotentPoint g

Unipotence of a point is invariant under precomposition by a bialgebra isomorphism.

@[simp]

theorem TauCeti.HopfAlgebra.isUnipotentPoint_one {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] : IsUnipotentPoint 1

The identity point is unipotent.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.inv {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] {g : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) : IsUnipotentPoint g⁻¹

The inverse of a unipotent point is unipotent.

@[simp]

theorem TauCeti.HopfAlgebra.isUnipotentPoint_inv_iff {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsUnipotentPoint g⁻¹ ↔ IsUnipotentPoint g

A point is unipotent if and only if its inverse is unipotent.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.mul_of_commute {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] {g h : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) (hh : IsUnipotentPoint h) (hcomm : Commute g h) : IsUnipotentPoint (g * h)

The product of two commuting unipotent points is unipotent.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.pow {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] {g : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) (n : ℕ) : IsUnipotentPoint (g ^ n)

Every natural power of a unipotent point is unipotent.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.zpow {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] {g : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) (n : ℤ) : IsUnipotentPoint (g ^ n)

Every integer power of a unipotent point is unipotent.

@[simp]

theorem TauCeti.HopfAlgebra.isUnipotentPoint_conj_iff {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] (g h : WithConv (H →ₐ[k] K)) : IsUnipotentPoint (h * g * h⁻¹) ↔ IsUnipotentPoint g

Unipotence of points is invariant under conjugation.