Unipotence of represented weight-cocharacter subgroups

Let w : Fin N → ℤ and let λ_w be the corresponding diagonal cocharacter of GL_N. The dynamic subgroup U(λ_w)(A) consists of the matrices which are block triangular for the weight filtration and induce the identity on its associated graded. The coordinate Hopf algebra GeneralLinear.weightUnipotentCoordinateHopfAlgebra k w represents this subgroup.

This file proves that every point of that coordinate Hopf algebra over a same-universe perfect extension field is unipotent in the representation-theoretic sense. The defining Hopf ideal cuts out the dynamic unipotent subgroup, so the general quotient-point theorem applies.

Smoothness and geometric connectedness of the represented subgroup require an explicit description of its coordinate ring and are not asserted here.

Main declarations

• TauCeti.GeneralLinear.Dynamic.isUnipotentPoint_weightUnipotentCoordinateHopfAlgebra: every perfect-extension-valued point of a represented weight-unipotent subgroup is unipotent.
• geometricallyUnipotentPointsCommHopfAlgProperty_weightUnipotentCoordinateHopfAlgebra: the represented subgroup has geometrically unipotent points.

References

• G. R. Kempf, Instability in invariant theory, Annals of Mathematics 108 (1978), §2.
• J. S. Milne, Algebraic Groups (2017), Chapter 13.

This advances the dynamic parabolic and Levi route in Layer 7, "Structure theory", of the ReductiveGroups roadmap by proving the unipotence property of the represented unipotent factor.

theorem TauCeti.GeneralLinear.Dynamic.isUnipotentPoint_weightUnipotentCoordinateHopfAlgebra {k : Type u} [Field k] {N : ℕ} (w : Fin N → ℤ) (L : Type u) [Field L] [Algebra k L] [PerfectField L] (g : ↑(HopfAlgebra.points ↧L)) : HopfAlgebra.IsUnipotentPoint g

Every point of the weight-unipotent coordinate Hopf algebra over a perfect extension field is unipotent in every finite-dimensional representation.

theorem TauCeti.GeneralLinear.Dynamic.geometricallyUnipotentPointsCommHopfAlgProperty_weightUnipotentCoordinateHopfAlgebra {k : Type u} [Field k] {N : ℕ} (w : Fin N → ℤ) : geometricallyUnipotentPointsCommHopfAlgProperty k (weightUnipotentCoordinateHopfAlgebra k w)

The represented weight-unipotent subgroup has geometrically unipotent points.