Representability of dynamic weight Levis

The weight-Levi subgroup scheme of GL_N represents the dynamic Levi 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.

The construction and its naturality follow the representing interface for the weight parabolic in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Dynamic.Weight.Parabolic.Basic, with the Levi cut out as the intersection of the two opposite weight parabolics.

Main declarations

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

theorem TauCeti.GeneralLinear.Dynamic.mem_weightLeviDefiningPointsSubgroup_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) (weightLeviDefiningHopfIdeal R w) ↧A ↔ g ∈ Cocharacter.levi (↑↧A) (weightCocharacter w)

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

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

The weight-Levi coordinate Hopf algebra represents the dynamic Levi 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_weightLeviPointsIso_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 ((weightLeviPointsIso R w).hom.app ↧A)) f)) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w) ↧A)) f

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

@[simp]

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

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