The unipotent radical of the upper-triangular group

The standard upper-triangular group is the dynamic parabolic for the injective weights i ↦ n - 1 - i. Its weight-unipotent subgroup consists exactly of upper-unitriangular matrices. Specializing the injective-weight calculation therefore identifies this subgroup with the unipotent radical of the upper-triangular affine group.

Main declaration

• TauCeti.GeneralLinear.UpperTriangular.mem_upperUnitriangularPointsSubgroup_iff: the relative weight-unipotent ideal cuts out exactly the existing upper-unitriangular matrix group over every commutative value algebra.
• TauCeti.GeneralLinear.UpperTriangular. unipotentRadicalDefiningIdeal_finiteTypeCoordinateHopfAlgebra: after identifying the finite-type package's object with the upper-triangular coordinate algebra, the relative upper-unitriangular Hopf ideal is the unipotent-radical defining ideal.

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.UpperTriangular.mem_upperUnitriangularPointsSubgroup_iff (R : Type u) [CommRing R] (n : ℕ) {A : Type v} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : f ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R n) (Dynamic.weightUnipotentInParabolicHopfIdeal R (weights n)) ↧A ↔ ↑((pointsMulEquiv R n) f) ∈ upperUnitriangularGroup (Fin n) A

The relative weight-unipotent ideal cuts out exactly the existing upper-unitriangular matrix group, compatibly with the upper-triangular inclusion into GL_n.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.unipotentRadicalDefiningIdeal_finiteTypeCoordinateHopfAlgebra (k : Type u) [Field k] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra k n).unipotentRadicalDefiningIdeal.comapOfSurjective (CommHopfAlgCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ⋯ = Dynamic.weightUnipotentInParabolicHopfIdeal k (weights n)

The unipotent radical of the standard upper-triangular group is its upper-unitriangular subgroup. The relative ideal is identified pointwise by mem_upperUnitriangularPointsSubgroup_iff; the pullback presents the finite-type radical in that relative coordinate algebra.