Parabolic subgroups in Hopf coordinates

A closed subgroup P of an affine group G of finite type over a field k is parabolic when it is smooth and its base change to an algebraic closure contains a Borel subgroup of the geometric fibre. For smooth G this is the classical characterization of the smooth closed subgroups P for which G/P is proper, and it is the notion of parabolic k-subgroup used in the structure theory of reductive groups over arbitrary fields. Containment of a Borel subgroup is taken as the definition because it is stated purely in terms of closed subgroups, without a represented quotient G/P.

Smoothness is imposed explicitly: in positive characteristic a closed subgroup scheme containing a Borel subgroup need not be reduced. As for Borel subgroups, Hopf ideals reverse inclusion, so the subgroup cut out by I contains the Borel subgroup cut out by J exactly when I ≤ J.

Over an algebraically closed field, conjugacy of Borel subgroups shows that every parabolic subgroup is conjugate to one containing a prescribed Borel subgroup. The parabolic subgroups are therefore exactly the smooth closed subgroups having a conjugate that contains that Borel.

Main declarations

• TauCeti.HopfIdeal.IsParabolicOverAlgClosed: the parabolic-subgroup predicate over an algebraically closed field.
• TauCeti.HopfIdeal.IsBorelOverAlgClosed.isParabolicOverAlgClosed: Borel subgroups are parabolic.
• TauCeti.HopfIdeal.IsParabolicOverAlgClosed.of_le: a smooth closed subgroup containing a parabolic subgroup is parabolic.
• TauCeti.HopfIdeal.isParabolicOverAlgClosed_bot_iff: the whole group is parabolic in itself exactly when it is smooth.
• TauCeti.HopfIdeal.IsParabolicOverAlgClosed.comapOfIso_iff: parabolicity is invariant under an ambient Hopf-algebra isomorphism.
• TauCeti.HopfIdeal.isParabolicOverAlgClosed_conjugate_iff: parabolicity is invariant under conjugation by a rational point.
• TauCeti.HopfIdeal.IsParabolicOverAlgClosed.exists_conjugate_le and TauCeti.HopfIdeal.isParabolicOverAlgClosed_iff_exists_conjugate_le: every parabolic subgroup has a conjugate containing a prescribed Borel subgroup, and this characterizes parabolics among smooth closed subgroups.
• TauCeti.HopfIdeal.IsParabolic: the parabolic-subgroup predicate over an arbitrary field, tested after base change to an algebraic closure.
• TauCeti.HopfIdeal.isParabolic_iff: a closed subgroup is parabolic exactly when it is smooth over the base field and its base change to an algebraic closure contains a Borel subgroup.
• TauCeti.HopfIdeal.IsBorel.isParabolic, TauCeti.HopfIdeal.IsParabolic.smooth, TauCeti.HopfIdeal.IsParabolic.exists_le_isBorelOverAlgClosed, TauCeti.HopfIdeal.IsParabolic.of_le, TauCeti.HopfIdeal.isParabolic_bot_iff, TauCeti.HopfIdeal.IsParabolic.comapOfIso_iff and TauCeti.HopfIdeal.isParabolic_conjugate_iff: the corresponding statements over an arbitrary field.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §11.2.
• J. S. Milne, Algebraic Groups (2017), §17.c.
• B. Conrad, Reductive Group Schemes (2014), §5.2.

def TauCeti.HopfIdeal.IsParabolicOverAlgClosed (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : Prop

Over an algebraically closed field, a Hopf ideal defines a parabolic subgroup when its quotient coordinate algebra is smooth and the closed subgroup it cuts out contains a Borel subgroup. In the contravariant Hopf-ideal order, containing the Borel subgroup cut out by J is the inequality I ≤ J.

@[simp]

theorem TauCeti.HopfIdeal.isParabolicOverAlgClosed_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : IsParabolicOverAlgClosed k H I ↔ IsAlgClosed k ∧ smoothCommHopfAlgProperty k (H.quotient I).obj ∧ ∃ (J : HopfIdeal k ↑H.obj), IsBorelOverAlgClosed k H J ∧ I ≤ J

The algebraically-closed-field parabolic condition asserts algebraic closedness, smoothness, and containment of a Borel subgroup.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.isAlgClosed {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsParabolicOverAlgClosed k H I) : IsAlgClosed k

The base field of a parabolic subgroup in the algebraically closed formulation is algebraically closed.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.smooth {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsParabolicOverAlgClosed k H I) : smoothCommHopfAlgProperty k (H.quotient I).obj

A parabolic subgroup is smooth.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.exists_le_isBorelOverAlgClosed {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsParabolicOverAlgClosed k H I) : ∃ (J : HopfIdeal k ↑H.obj), IsBorelOverAlgClosed k H J ∧ I ≤ J

A parabolic subgroup contains a Borel subgroup.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.of_le {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsParabolicOverAlgClosed k H I) {J : HopfIdeal k ↑H.obj} (hJI : J ≤ I) (hJ : smoothCommHopfAlgProperty k (H.quotient J).obj) : IsParabolicOverAlgClosed k H J

A smooth closed subgroup containing a parabolic subgroup is parabolic.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.comapOfIso {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} {J : HopfIdeal k ↑L.obj} (hJ : IsParabolicOverAlgClosed k L J) (e : H ≅ L) : IsParabolicOverAlgClosed k H (J.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯)

Pulling a parabolic subgroup back across an ambient Hopf-algebra isomorphism gives a parabolic subgroup in the source.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.comapOfIso_iff {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} (e : H ≅ L) (J : HopfIdeal k ↑L.obj) : IsParabolicOverAlgClosed k H (J.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯) ↔ IsParabolicOverAlgClosed k L J

Over an algebraically closed field, parabolicity is invariant under pulling the defining ideal back across an ambient Hopf-algebra isomorphism.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.isParabolicOverAlgClosed {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) : IsParabolicOverAlgClosed k H I

Over an algebraically closed field, a Borel subgroup is parabolic.

theorem TauCeti.HopfIdeal.isParabolicOverAlgClosed_bot_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : IsParabolicOverAlgClosed k H ⊥ ↔ IsAlgClosed k ∧ smoothCommHopfAlgProperty k H.obj

Over an algebraically closed field, the whole group is a parabolic subgroup of itself exactly when it is smooth. The whole group is cut out by the zero Hopf ideal.

This is not a simp lemma: isParabolicOverAlgClosed_iff unfolds IsParabolicOverAlgClosed on the left-hand side, so the statement is never in simp-normal form.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.conjugate {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {I : HopfIdeal k H} (hI : IsParabolicOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I) (g : WithConv (H →ₐ[k] k)) : IsParabolicOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) (I.conjugate g)

Over an algebraically closed field, the conjugate of a parabolic subgroup by a rational point is parabolic.

theorem TauCeti.HopfIdeal.isParabolicOverAlgClosed_conjugate_iff {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (I : HopfIdeal k H) (g : WithConv (H →ₐ[k] k)) : IsParabolicOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) (I.conjugate g) ↔ IsParabolicOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I

The algebraically closed parabolic property is invariant under conjugation by a rational point.

This is not a simp lemma: isParabolicOverAlgClosed_iff unfolds IsParabolicOverAlgClosed on the left-hand side, so the statement is never in simp-normal form.

theorem TauCeti.HopfIdeal.IsParabolicOverAlgClosed.exists_conjugate_le {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {I J : HopfIdeal k H} (hI : IsParabolicOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I) (hJ : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) J) : ∃ (g : WithConv (H →ₐ[k] k)), I.conjugate g ≤ J

Every parabolic subgroup has a conjugate containing a prescribed Borel subgroup. Over an algebraically closed field, if I cuts out a parabolic subgroup and J a Borel subgroup, some rational point conjugates the parabolic to a subgroup containing the Borel.

theorem TauCeti.HopfIdeal.isParabolicOverAlgClosed_iff_exists_conjugate_le {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {I J : HopfIdeal k H} (hJ : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) J) : IsParabolicOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I ↔ smoothCommHopfAlgProperty k ((FiniteTypeCommHopfAlgCat.of k H).quotient I).obj ∧ ∃ (g : WithConv (H →ₐ[k] k)), I.conjugate g ≤ J

Parabolic subgroups relative to a fixed Borel subgroup. Over an algebraically closed field, a closed subgroup is parabolic exactly when it is smooth and one of its conjugates by a rational point contains the prescribed Borel subgroup.

def TauCeti.HopfIdeal.IsParabolic (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : Prop

A Hopf ideal defines a parabolic subgroup when its base change to an algebraic closure defines a smooth closed subgroup of the geometric fibre containing a Borel subgroup.

The order is contravariant: I ≤ J says that the subgroup cut out by I contains the subgroup cut out by J.

theorem TauCeti.HopfIdeal.isParabolic_iff_isParabolicOverAlgClosed_baseChange (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : let K := AlgebraicClosure k; let H' := FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }; have I' := CommHopfAlgCat.baseChangeHopfIdeal I; IsParabolic k H I ↔ IsParabolicOverAlgClosed K H' I'

The general-field parabolic predicate is the algebraically-closed-field parabolic predicate after base change to an algebraic closure.

theorem TauCeti.HopfIdeal.IsBorel.isParabolic {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) : IsParabolic k H I

A Borel subgroup over an arbitrary field is parabolic.

theorem TauCeti.HopfIdeal.IsParabolic.comapOfIso {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑L.obj} (hI : IsParabolic k L.obj I) (e : H ≅ L) : IsParabolic k H.obj (I.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯)

Pulling a parabolic subgroup back across an ambient Hopf-algebra isomorphism gives a parabolic subgroup in the source.

theorem TauCeti.HopfIdeal.IsParabolic.comapOfIso_iff {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} (e : H ≅ L) (I : HopfIdeal k ↑L.obj) : IsParabolic k H.obj (I.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯) ↔ IsParabolic k L.obj I

Parabolicity is invariant under pulling the defining ideal back across an ambient Hopf-algebra isomorphism.

theorem TauCeti.HopfIdeal.IsParabolic.smooth {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsParabolic k H I) : smoothCommHopfAlgProperty k (H.quotient I)

A parabolic subgroup over an arbitrary field is smooth over that field. Smoothness of its geometric fibre descends along the faithfully flat extension to an algebraic closure.

theorem TauCeti.HopfIdeal.IsParabolic.exists_le_isBorelOverAlgClosed {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsParabolic k H I) : ∃ (J : HopfIdeal (AlgebraicClosure k) ↑(FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }).obj), IsBorelOverAlgClosed (AlgebraicClosure k) (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }) J ∧ CommHopfAlgCat.baseChangeHopfIdeal I ≤ J

The base change of a parabolic subgroup to an algebraic closure contains a Borel subgroup of the geometric fibre.

theorem TauCeti.HopfIdeal.IsParabolic.of_le {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsParabolic k H I) {J : HopfIdeal k ↑H} (hJI : J ≤ I) (hJ : smoothCommHopfAlgProperty k (H.quotient J)) : IsParabolic k H J

A closed subgroup that is smooth over the base field and contains a parabolic subgroup is parabolic.

@[simp]

theorem TauCeti.HopfIdeal.isParabolic_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : let K := AlgebraicClosure k; let H' := FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }; have I' := CommHopfAlgCat.baseChangeHopfIdeal I; IsParabolic k H I ↔ smoothCommHopfAlgProperty k (H.quotient I) ∧ ∃ (J : HopfIdeal K ↑H'.obj), IsBorelOverAlgClosed K H' J ∧ I' ≤ J

The Hopf-ideal criterion for a parabolic subgroup: it is smooth over the base field, and its base change to an algebraic closure contains a Borel subgroup of the geometric fibre.

theorem TauCeti.HopfIdeal.isParabolic_bot_iff {k : Type u} [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : IsParabolic k H ⊥ ↔ smoothCommHopfAlgProperty k H

The whole group is a parabolic subgroup of itself exactly when it is smooth. The whole group is cut out by the zero Hopf ideal.

This is not a simp lemma: isParabolic_iff unfolds IsParabolic on the left-hand side, so the statement is never in simp-normal form.

theorem TauCeti.HopfIdeal.IsParabolic.conjugate {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {I : HopfIdeal k H} (hI : IsParabolic k (↧H) I) (g : WithConv (H →ₐ[k] k)) : IsParabolic k (↧H) (I.conjugate g)

The conjugate of a parabolic subgroup by a rational point is parabolic.

theorem TauCeti.HopfIdeal.isParabolic_conjugate_iff {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (I : HopfIdeal k H) (g : WithConv (H →ₐ[k] k)) : IsParabolic k (↧H) (I.conjugate g) ↔ IsParabolic k (↧H) I

Parabolicity is invariant under conjugation by a rational point.

This is not a simp lemma: isParabolic_iff unfolds IsParabolic on the left-hand side, so the statement is never in simp-normal form.