Unipotent radicals of injective-weight parabolics

For an injective weight w : Fin N → ℤ, the dynamic parabolic P(w) has diagonal-torus Levi quotient and weight-unipotent kernel U(w). This file identifies that kernel with the unipotent radical of P(w).

The normality and kernel calculation come from the represented dynamic Levi decomposition. The weight-unipotent coordinate algebra is polynomial, hence smooth and geometrically connected, and its points are unipotent. The general diagonalizable-quotient criterion then gives the claimed equality of Hopf ideals.

Main declaration

• TauCeti.GeneralLinear. unipotentRadicalDefiningIdeal_weightParabolicFiniteTypeCoordinateHopfAlgebra: after identifying the finite-type package's object with the weight-parabolic coordinate algebra, the unipotent radical is its weight-unipotent kernel.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 13 and 17.
• T. A. Springer, Linear Algebraic Groups, Sections 6.2--6.3.

@[simp]

theorem TauCeti.GeneralLinear.unipotentRadicalDefiningIdeal_weightParabolicFiniteTypeCoordinateHopfAlgebra {N : ℕ} (k : Type u) [Field k] (w : Fin N → ℤ) (hw : Function.Injective w) : (weightParabolicFiniteTypeCoordinateHopfAlgebra k w).unipotentRadicalDefiningIdeal.comapOfSurjective (CommHopfAlgCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ⋯ = Dynamic.weightUnipotentInParabolicHopfIdeal k w

The unipotent radical of an injective-weight parabolic is its weight-unipotent subgroup. The pullback along the displayed object equality presents the result in the coordinate algebra where the canonical weight-unipotent ideal is defined.