Borel subgroups inside closed subgroups

A Borel subgroup of an affine group that is contained in a closed subgroup is also a Borel subgroup of that closed subgroup. More generally, a closed subgroup containing every smooth connected solvable subgroup has exactly the same Borel subgroups as the ambient group. This allows maximality arguments to pass to smaller ambient groups.

Coordinate morphisms of closed immersions are surjective. The candidate comparison uses CommHopfAlgCat.Hom.quotientIsoOfSurjective, and the maximality comparison uses the image/inverse-image correspondence for Hopf ideals.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §11.1.
• J. S. Milne, Algebraic Groups (2017), §17.a.

theorem TauCeti.HopfIdeal.isBorelCandidate_comapOfSurjective_iff {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Surjective ⇑(FiniteTypeCommHopfAlgCat.toBialgHom f)) (J : HopfIdeal k ↑K.obj) : IsBorelCandidate k H (J.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom f) hf) ↔ IsBorelCandidate k K J

A closed subgroup of a closed subgroup is smooth, geometrically connected, and geometrically solvable exactly when it has these properties in the ambient group.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.of_comapOfSurjective {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Surjective ⇑(FiniteTypeCommHopfAlgCat.toBialgHom f)) {J : HopfIdeal k ↑K.obj} (hJ : IsBorelOverAlgClosed k H (J.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom f) hf)) : IsBorelOverAlgClosed k K J

Restricting the ambient group of a Borel subgroup to a closed subgroup containing it preserves the Borel property.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.map_of_le {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hJ : IsBorelOverAlgClosed k H J) (hIJ : I ≤ J) : IsBorelOverAlgClosed k (H.quotient I) (J.map (Bialgebra.Quotient.mkBialgHom I.toIdeal))

A Borel subgroup contained in the subgroup cut out by I is Borel in that subgroup. Hopf ideal order reverses inclusion of the represented subgroups.

theorem TauCeti.HopfIdeal.isBorelOverAlgClosed_comapOfSurjective_iff {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Surjective ⇑(FiniteTypeCommHopfAlgCat.toBialgHom f)) (hker : ∀ (I : HopfIdeal k ↑H.obj), IsBorelCandidate k H I → kerOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom f) hf ≤ I) (J : HopfIdeal k ↑K.obj) : IsBorelOverAlgClosed k H (J.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom f) hf) ↔ IsBorelOverAlgClosed k K J

If a closed subgroup contains every Borel candidate of the ambient group, its Borel subgroups are precisely the ambient Borel subgroups. The kernel condition expresses this containment in coordinate Hopf ideal order.