Representability of dynamic Levi subgroups

For a cocharacter λ of an affine group scheme, its dynamic Levi Z(λ) is represented by the quotient by the sum of the defining Hopf ideals of P(λ) and P(−λ). Thus it is the scheme-theoretic intersection of the two opposite dynamic parabolics. The natural representing isomorphism identifies quotient points with their ambient points, over every commutative value algebra, including nonreduced ones.

No field, smoothness, reductivity, or finite-type hypothesis is needed. When the ambient coordinate algebra is of finite type, its Levi quotient is of finite type by the existing Hopf-ideal quotient API. This supplies the affine subgroup needed for the scheme-theoretic Levi decomposition; it makes no claim that a dynamic parabolic has proper homogeneous quotient.

References

• B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, §2.1.
• J. S. Milne, Algebraic Groups (2017), Chapter 13.

The representing isomorphism uses the same quotient-points construction as TauCeti.Cocharacter.parabolicPointsIso.

noncomputable def TauCeti.Cocharacter.leviDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : HopfIdeal R H

The Hopf ideal cutting out the dynamic Levi, the scheme-theoretic intersection of the parabolics of a cocharacter and its opposite.

theorem TauCeti.Cocharacter.leviDefiningHopfIdeal_def {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : leviDefiningHopfIdeal l = parabolicDefiningHopfIdeal l ⊔ parabolicDefiningHopfIdeal l.oppositeCocharacter

The Levi defining ideal is the sum of the two opposite parabolic defining ideals.

@[simp]

theorem TauCeti.Cocharacter.leviDefiningHopfIdeal_oppositeCocharacter {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : leviDefiningHopfIdeal l.oppositeCocharacter = leviDefiningHopfIdeal l

Opposite cocharacters define the same closed Levi subgroup scheme.

@[simp]

theorem TauCeti.Cocharacter.quotientPointsSubgroup_leviDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) : CommHopfAlgCat.quotientPointsSubgroup (↧H) (leviDefiningHopfIdeal l) A = levi (↑A) l

The subgroup cut out by the Levi ideal is exactly the dynamic Levi, over every value algebra.

noncomputable def TauCeti.Cocharacter.leviPointsIso {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : HopfAlgebra.pointsFunctor ≅ leviFunctor l

The quotient by the Levi defining Hopf ideal represents the dynamic Levi functor.

@[simp]

theorem TauCeti.Cocharacter.coe_leviPointsIso_hom_app_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : ↑((CategoryTheory.ConcreteCategory.hom ((leviPointsIso l).hom.app A)) f) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (leviDefiningHopfIdeal l) A)) f

The representing isomorphism sends a quotient point to its ambient point.

@[simp]

theorem TauCeti.Cocharacter.quotientPointsHom_leviPointsIso_inv_app_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) (g : ↥(levi (↑A) l)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (leviDefiningHopfIdeal l) A)) ((CategoryTheory.ConcreteCategory.hom ((leviPointsIso l).inv.app A)) g) = ↑g

Factoring a Levi point through the representing quotient recovers its ambient point.