Unipotence of the dynamic unipotent subgroup

For a cocharacter l : 𝔾ₘ → G, the dynamic subgroup U(l) consists of the points whose conjugates by l(t) extend to t = 0 with limit one. This file proves that these points are unipotent in the representation-theoretic sense: they act unipotently in every finite-dimensional comodule.

The proof applies a representation to the extending polynomial family. Over the Laurent polynomials the family is conjugate to the original action, so its characteristic polynomial is constant. At the origin the family is the identity, hence that constant is (X - 1) ^ n.

Main declarations

• TauCeti.Cocharacter.isUnipotentPoint_of_mem_unipotent: every point of the dynamic unipotent subgroup is a unipotent point.
• TauCeti.Cocharacter.isUnipotentPoint_quotient_of_le_unipotent: every point of a Hopf-ideal quotient whose cut-out subgroup lies in a dynamic unipotent subgroup is unipotent.

References

• G. R. Kempf, Instability in invariant theory, Annals of Mathematics 108 (1978), §2.
• B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, §2.1.

This completes the pointwise unipotence assertion implicit in the dynamic route to parabolic and Levi subgroups in Layer 7 of the ReductiveGroups roadmap, using the representation-theoretic definition from Layer 5.

theorem TauCeti.Cocharacter.isUnipotentPoint_of_mem_unipotent {R : Type u} {H : Type v} {A : Type w} [Field R] [Semiring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) {g : WithConv (H →ₐ[R] A)} (hg : g ∈ unipotent A l) : HopfAlgebra.IsUnipotentPoint g

Every point of the dynamic unipotent subgroup attached to a cocharacter is unipotent in every finite-dimensional representation.

theorem TauCeti.Cocharacter.isUnipotentPoint_quotient_of_le_unipotent {R : Type u} [Field R] (B : CommHopfAlgCat R) (I : HopfIdeal R ↑B) (l : ↑B →ₐc[R] LaurentPolynomial R) (L : Type u) [Field L] [Algebra R L] [PerfectField L] (hI : CommHopfAlgCat.quotientPointsSubgroup B I ↧L ≤ unipotent (↑↧L) l) (g : ↑(HopfAlgebra.points ↧L)) : HopfAlgebra.IsUnipotentPoint g

Every point of a Hopf-ideal quotient is unipotent when its ambient cut-out subgroup lies in a dynamic unipotent subgroup.