Representability of dynamic unipotent subgroups

For a cocharacter l of an affine group, the dynamic unipotent subgroup consists of points whose conjugation family extends over the origin with value the identity. It is cut out by the negative coefficients of universal conjugation, together with the differences between its constant coefficients and the counit. These equations represent the subgroup over every commutative value algebra, including nonreduced algebras.

The quotient by this coefficient ideal represents the dynamic unipotent functor. In particular it is a closed affine subgroup of the ambient group, without finite-type, smoothness, field, or reductivity assumptions. This is the unipotent factor in the dynamic Levi decomposition; no identification with the unipotent radical is asserted.

The construction uses the universal conjugation coefficients and parabolic representing ideal from Dynamic.Representability, and the pointwise Hopf-ideal criterion and natural quotient-points isomorphism from HopfIdeal.Points.

The main constructions are BialgHom.unipotentDefiningHopfIdeal and BialgHom.unipotentPointsIso. Their coefficient and evaluation lemmas characterize both the defining equations and the representing isomorphism.

References

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

theorem BialgHom.limit_eq_one_iff_coeff_conjugationAlgHom {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {A : Type w} [CommRing A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(TauCeti.Cocharacter.parabolic A l)) : (TauCeti.Cocharacter.limit A l) g = 1 ↔ ∀ (h : H), (↑g).ofConv (((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0 - (algebraMap R H) (CoalgebraStruct.counit h)) = 0

A parabolic point has trivial dynamic limit exactly when it annihilates the differences between the universal constant coefficients and the counit.

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

The defining Hopf ideal of the dynamic unipotent subgroup: the parabolic equations, together with the equations setting the dynamic limit equal to the identity.

@[simp]

theorem BialgHom.unipotentDefiningHopfIdeal_toIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : l.unipotentDefiningHopfIdeal.toIdeal = (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l).toIdeal ⊔ Ideal.span {x : H | ∃ (h : H), ((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0 - (algebraMap R H) (CoalgebraStruct.counit h) = x}

The underlying ideal is generated by the parabolic ideal and the constant-coefficient differences from the counit.

@[simp]

theorem BialgHom.mem_unipotentDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (x : H) : x ∈ l.unipotentDefiningHopfIdeal ↔ x ∈ (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l).toIdeal ⊔ Ideal.span {x : H | ∃ (h : H), ((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0 - (algebraMap R H) (CoalgebraStruct.counit h) = x}

Membership in the unipotent defining ideal is membership in its coefficient ideal.

theorem BialgHom.parabolicDefiningHopfIdeal_le_unipotentDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : TauCeti.Cocharacter.parabolicDefiningHopfIdeal l ≤ l.unipotentDefiningHopfIdeal

The dynamic unipotent defining ideal contains the parabolic defining ideal.

theorem BialgHom.coeff_conjugationAlgHom_sub_counit_mem_unipotentDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (h : H) : ((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0 - (algebraMap R H) (CoalgebraStruct.counit h) ∈ l.unipotentDefiningHopfIdeal

The constant coefficient of universal conjugation equals the counit on the dynamic unipotent subgroup.

theorem BialgHom.unipotentDefiningHopfIdeal_le_iff {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (I : TauCeti.HopfIdeal R H) : l.unipotentDefiningHopfIdeal ≤ I ↔ TauCeti.Cocharacter.parabolicDefiningHopfIdeal l ≤ I ∧ ∀ (h : H), ((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0 - (algebraMap R H) (CoalgebraStruct.counit h) ∈ I

The unipotent ideal is the smallest Hopf ideal containing the parabolic ideal and all constant-coefficient differences from the counit.

@[simp]

theorem BialgHom.quotientPointsSubgroup_unipotentDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {A : Type w} [CommRing A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : TauCeti.CommHopfAlgCat.quotientPointsSubgroup (↧H) l.unipotentDefiningHopfIdeal ↧A = TauCeti.Cocharacter.unipotent A l

The points cut out by the coefficient ideal are exactly the dynamic unipotent subgroup.

theorem BialgHom.isNormal_unipotentDefiningHopfIdeal_of_parabolicDefiningHopfIdeal_eq_bot {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (hl : TauCeti.Cocharacter.parabolicDefiningHopfIdeal l = ⊥) : l.unipotentDefiningHopfIdeal.IsNormal

If the dynamic parabolic of a cocharacter is the whole group, then the dynamic unipotent subgroup is a normal closed subgroup of the whole group.

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

The coefficient Hopf quotient represents the dynamic unipotent functor.

@[simp]

theorem BialgHom.coe_unipotentPointsIso_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 : ↑(TauCeti.HopfAlgebra.points A)) : ↑((CategoryTheory.ConcreteCategory.hom (l.unipotentPointsIso.hom.app A)) f) = (CategoryTheory.ConcreteCategory.hom (TauCeti.CommHopfAlgCat.quotientPointsHom (↧H) l.unipotentDefiningHopfIdeal A)) f

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

@[simp]

theorem BialgHom.quotientPointsHom_unipotentPointsIso_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 : ↥(TauCeti.Cocharacter.unipotent (↑A) l)) : (CategoryTheory.ConcreteCategory.hom (TauCeti.CommHopfAlgCat.quotientPointsHom (↧H) l.unipotentDefiningHopfIdeal A)) ((CategoryTheory.ConcreteCategory.hom (l.unipotentPointsIso.inv.app A)) g) = ↑g

Factoring a dynamic unipotent point through the representing algebra recovers its ambient point.