Representability of dynamic weight-unipotent subgroups

The weight-unipotent subgroup scheme of GL_N represents the dynamic unipotent subgroup attached to the cocharacter t ↦ diag(t ^ w i). On points, both descriptions say that the matrix is block triangular for the weight filtration and acts as the identity on every associated-graded weight space.

Together with the weight-parabolic and weight-Levi representing isomorphisms, this supplies all three scheme-level pieces attached to an arbitrary diagonal weight cocharacter.

Main declarations

• TauCeti.GeneralLinear.Dynamic.mem_weightUnipotentDefiningPointsSubgroup_iff: membership in the Hopf-ideal cut-out agrees with dynamic-unipotent membership.
• TauCeti.GeneralLinear.Dynamic.weightUnipotentPointsIso: the natural representing isomorphism.

References

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

This completes representability of the parabolic, Levi, and unipotent functors attached to a weight cocharacter in the dynamic route of Layer 7, "Structure theory", of the ReductiveGroups roadmap.

theorem TauCeti.GeneralLinear.Dynamic.mem_weightUnipotentDefiningPointsSubgroup_iff (R : Type u) [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : ↑(HopfAlgebra.points (CommAlgCat.of R A))) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w) (CommAlgCat.of R A) ↔ g ∈ Cocharacter.unipotent (↑(CommAlgCat.of R A)) (weightCocharacter w)

The Hopf-ideal cut-out is exactly the dynamic unipotent subgroup of the weight cocharacter.

noncomputable def TauCeti.GeneralLinear.Dynamic.weightUnipotentPointsIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : HopfAlgebra.pointsFunctor ≅ Cocharacter.unipotentFunctor (weightCocharacter w)

The weight-unipotent coordinate Hopf algebra represents the dynamic unipotent functor of the weight cocharacter, naturally in the commutative value algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.coe_weightUnipotentPointsIso_hom_app_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {A : Type v} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points (CommAlgCat.of R A))) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((weightUnipotentPointsIso R w).hom.app (CommAlgCat.of R A))) f)) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w) (CommAlgCat.of R A))) f

The ambient point underlying the represented dynamic-unipotent point is induced by the quotient coordinate map.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.quotientPointsHom_weightUnipotentPointsIso_inv_app_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {A : Type v} [CommRing A] [Algebra R A] (g : ↥(Cocharacter.unipotent (↑(CommAlgCat.of R A)) (weightCocharacter w))) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w) (CommAlgCat.of R A))) ((CategoryTheory.ConcreteCategory.hom ((weightUnipotentPointsIso R w).inv.app (CommAlgCat.of R A))) g) = ↑g

Applying the quotient inclusion to the inverse representing isomorphism recovers the ambient dynamic-unipotent point.