The represented dynamic limit

For a cocharacter l of an affine group, the dynamic limit on its parabolic subgroup is a morphism of affine groups. Its coordinate morphism sends a function to the constant Laurent coefficient of universal conjugation, restricted to the parabolic. Its scheme-theoretic kernel is the dynamic unipotent subgroup, including on nonreduced value algebras. Restriction to the Levi subgroup recovers its ambient inclusion.

The coordinate formula computes the limit of any parabolic point over a commutative value algebra in an arbitrary universe. The kernel identity identifies the quotient of the parabolic coordinate algebra defining the fibre over the identity with the coordinate algebra of the dynamic unipotent subgroup. The isomorphism BialgHom.parabolicLimitKernelIso realizes this identification as an isomorphism of group schemes over the base, compatible with their inclusions into the parabolic.

References

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

noncomputable def BialgHom.parabolicLimitCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : ↧H ⟶ (↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)

The coordinate morphism of the dynamic limit P(l) → G. Its direction is O(G) → O(P(l)), opposite to the morphism of affine groups.

theorem BialgHom.parabolicLimitCoordinateMap_apply {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (h : H) : (CommHopfAlgCat.Hom.hom l.parabolicLimitCoordinateMap) h = (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l))) (((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0)

The dynamic limit coordinate morphism evaluates the universal constant coefficient on the parabolic quotient.

theorem BialgHom.mapPointsFunctor_parabolicLimitCoordinateMap_app {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) (g : ↑(TauCeti.HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.Hom.mapPointsFunctor l.parabolicLimitCoordinateMap).app A)) g = (TauCeti.Cocharacter.limit (↑A) l) ((CategoryTheory.ConcreteCategory.hom ((TauCeti.Cocharacter.parabolicPointsIso l).hom.app A)) g)

On every commutative value algebra, precomposition by the coordinate morphism is exactly the dynamic limit of the represented parabolic point.

@[simp]

theorem BialgHom.parabolicLimitCoordinateMap_comp_quotientMapOfLe {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : CategoryTheory.CategoryStruct.comp l.parabolicLimitCoordinateMap ((↧H).quotientMapOfLe ⋯) = (↧H).mkQuotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l)

Restricting the represented limit to the Levi subgroup gives its ambient inclusion.

theorem BialgHom.kernelHopfIdeal_parabolicLimitCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : TauCeti.CommHopfAlgCat.kernelHopfIdeal l.parabolicLimitCoordinateMap = l.unipotentDefiningHopfIdeal.map (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)))

The scheme-theoretic kernel of the dynamic limit is the dynamic unipotent subgroup. The ideal is written in the parabolic coordinate algebra by mapping the ambient unipotent ideal through the parabolic quotient.

noncomputable def BialgHom.parabolicLimitKernelIso {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : TauCeti.CommHopfAlgCat.kernelSpec l.parabolicLimitCoordinateMap ≅ TauCeti.CommHopfAlgCat.quotientSpec (↧H) l.unipotentDefiningHopfIdeal

The scheme-theoretic kernel of the dynamic limit is canonically the group scheme represented by the dynamic unipotent Hopf quotient.

@[simp]

theorem BialgHom.parabolicLimitKernelIso_hom_comp_quotientSpecMapOfLe {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : CategoryTheory.CategoryStruct.comp l.parabolicLimitKernelIso.hom (TauCeti.CommHopfAlgCat.quotientSpecMapOfLe ↧H ⋯) = TauCeti.CommHopfAlgCat.kernelSpecι l.parabolicLimitCoordinateMap

Under the kernel identification, the unipotent inclusion into the parabolic is the canonical kernel inclusion.