Representability of dynamic parabolic subgroups

For a cocharacter of an affine group scheme, universal conjugation has values in the Laurent polynomials over its coordinate algebra. Its negative coefficients generate the ideal cutting out those points whose conjugation extends over the origin. These points are exactly the dynamic parabolic, over every value algebra, including nonreduced ones.

The pointwise subgroup criterion makes this ideal a Hopf ideal. Thus the dynamic parabolic is represented by a closed affine subgroup scheme, without a smoothness, finite-type, field, or reductivity assumption. For a finite-type ambient group its coordinate algebra is again of finite type. This does not assert smoothness or properness of the homogeneous space, nor that the dynamic unipotent subgroup is the unipotent radical.

References

• B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, §2.1.

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

Universal conjugation by a cocharacter, evaluated at the identity algebra homomorphism (the universal point of the ambient group, not its identity element).

theorem TauCeti.Cocharacter.coeff_conjugate {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 : WithConv (H →ₐ[R] A)) (h : H) (n : ℤ) : (((conjugate A l) g).ofConv h).coeff n = g.ofConv (((conjugationAlgHom l) h).coeff n)

The coefficients of conjugation at any point are evaluations of the universal coefficients.

@[simp]

theorem TauCeti.Cocharacter.coeff_conjugationAlgHom_coeff {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (h : H) (m n : ℤ) : ((conjugationAlgHom l) (((conjugationAlgHom l) h).coeff n)).coeff m = if m = n then ((conjugationAlgHom l) h).coeff n else 0

The coefficients of universal conjugation are weight vectors. Conjugating the n-th coefficient of h produces only the monomial of degree n, whose coefficient is that same coefficient.

theorem TauCeti.Cocharacter.conjugate_ofConv_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 : WithConv (H →ₐ[R] A)) (h : H) (n : ℤ) : ((conjugate A l) g).ofConv (((conjugationAlgHom l) h).coeff n) = LaurentPolynomial.C (g.ofConv (((conjugationAlgHom l) h).coeff n)) * LaurentPolynomial.T n

Conjugation by the generic point sends the n-th coefficient of universal conjugation to a monomial of degree n.

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

The defining Hopf ideal of the dynamic parabolic, generated by the negative coefficients of universal conjugation.

@[simp]

theorem TauCeti.Cocharacter.parabolicDefiningHopfIdeal_toIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : (parabolicDefiningHopfIdeal l).toIdeal = Ideal.span {x : H | ∃ (h : H), ∃ n < 0, ((conjugationAlgHom l) h).coeff n = x}

The ideal defining the dynamic parabolic is generated by the negative Laurent coefficients.

@[simp]

theorem TauCeti.Cocharacter.mem_parabolicDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (x : H) : x ∈ parabolicDefiningHopfIdeal l ↔ x ∈ Ideal.span {x : H | ∃ (h : H), ∃ n < 0, ((conjugationAlgHom l) h).coeff n = x}

Membership in the defining Hopf ideal is membership in the span of the negative coefficients.

theorem TauCeti.Cocharacter.coeff_conjugationAlgHom_mem_parabolicDefiningHopfIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (h : H) {n : ℤ} (hn : n < 0) : ((conjugationAlgHom l) h).coeff n ∈ parabolicDefiningHopfIdeal l

All negative coefficients of universal conjugation vanish on the dynamic parabolic.

@[simp]

theorem TauCeti.Cocharacter.quotientPointsSubgroup_parabolicDefiningHopfIdeal {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) : CommHopfAlgCat.quotientPointsSubgroup (↧H) (parabolicDefiningHopfIdeal l) ↧A = parabolic A l

The dynamic parabolic is represented by the closed subgroup defined by its coefficient ideal.

theorem TauCeti.Cocharacter.parabolicDefiningHopfIdeal_le_iff {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (I : HopfIdeal R H) : parabolicDefiningHopfIdeal l ≤ I ↔ ∀ (h : H), ∀ n < 0, ((conjugationAlgHom l) h).coeff n ∈ I

The coefficient ideal is the smallest Hopf ideal containing all the negative coefficients.

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

The quotient by the negative-coefficient ideal represents the dynamic parabolic functor.

@[simp]

theorem TauCeti.Cocharacter.coe_parabolicPointsIso_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 ((parabolicPointsIso l).hom.app A)) f) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (parabolicDefiningHopfIdeal l) A)) f

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

@[simp]

theorem TauCeti.Cocharacter.quotientPointsHom_parabolicPointsIso_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 : ↥(parabolic (↑A) l)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (parabolicDefiningHopfIdeal l) A)) ((CategoryTheory.ConcreteCategory.hom ((parabolicPointsIso l).inv.app A)) g) = ↑g

Factoring a parabolic point through its representing algebra recovers its ambient point.

theorem BialgHom.parabolic_eq_top_of_parabolicDefiningHopfIdeal_eq_bot {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (hl : TauCeti.Cocharacter.parabolicDefiningHopfIdeal l = ⊥) (A : Type u_3) [CommRing A] [Algebra R A] : TauCeti.Cocharacter.parabolic A l = ⊤

If the dynamic parabolic of a cocharacter is the whole group, then its points over every value algebra are all the points.