Representability of dynamic weight parabolics

The weight-parabolic subgroup scheme of GL_N represents the dynamic parabolic attached to the cocharacter t ↦ diag(t ^ w i). On points, both descriptions say exactly that the (i,j) entry vanishes whenever w i < w j.

Main declarations

• TauCeti.GeneralLinear.Dynamic.mem_weightParabolicDefiningPointsSubgroup_iff: membership in the Hopf-ideal cut-out agrees with dynamic-parabolic membership.
• TauCeti.GeneralLinear.Dynamic.weightParabolicPointsIso: 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 weight-cocharacter parabolic in the dynamic route of Layer 7, "Structure theory", of the ReductiveGroups roadmap.

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

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

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

The weight-parabolic coordinate Hopf algebra represents the dynamic parabolic 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_weightParabolicPointsIso_hom_app_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {A : Type v} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((weightParabolicPointsIso R w).hom.app ↧A)) f)) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightParabolicDefiningHopfIdeal R w) ↧A)) f

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

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.quotientPointsHom_weightParabolicPointsIso_inv_app_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {A : Type v} [CommRing A] [Algebra R A] (g : ↥(Cocharacter.parabolic (↑↧A) (weightCocharacter w))) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightParabolicDefiningHopfIdeal R w) ↧A)) ((CategoryTheory.ConcreteCategory.hom ((weightParabolicPointsIso R w).inv.app ↧A)) g) = ↑g

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