Reducing Borel conjugacy to smooth connected affine groups

A closed subgroup containing every Borel candidate transfers a Borel-conjugacy theorem to the ambient group. The conjugating point is mapped along the closed immersion; no lifting of rational points along a quotient of groups is involved.

Over an algebraically closed field, every Borel candidate lies in the identity component of the reduction. This subgroup is smooth and geometrically connected even when the ambient group is neither reduced nor connected. Consequently, to prove conjugacy of Borel subgroups of all finite-type affine groups, it suffices to prove it for smooth connected groups. The smooth connected conjugacy theorem is a hypothesis here, not a conclusion.

The construction uses HopfIdeal.identityComponent_le_of_le and HopfIdeal.reduction_le_of_isReduced_quotient; transfer uses HopfIdeal.exists_conjugate_eq_comapOfSurjective.

References

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

theorem TauCeti.HopfIdeal.exists_conjugate_eq_of_isBorelOverAlgClosed_of_quotient {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (P : HopfIdeal k ↑H.obj) (hconj : ∀ (I J : HopfIdeal k ↑(H.quotient P).obj), IsBorelOverAlgClosed k (H.quotient P) I → IsBorelOverAlgClosed k (H.quotient P) J → ∃ (g : WithConv (↑(H.quotient P).obj →ₐ[k] k)), I.conjugate g = J) {I J : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) (hJ : IsBorelOverAlgClosed k H J) (hPI : P ≤ I) (hPJ : P ≤ J) : ∃ (g : WithConv (↑H.obj →ₐ[k] k)), I.conjugate g = J

Two ambient Borel subgroups contained in a closed subgroup are conjugate in the ambient group whenever Borel subgroups of that closed subgroup are conjugate.

theorem TauCeti.HopfIdeal.exists_conjugate_eq_of_isBorelOverAlgClosed_of_smooth_connected {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} [IsAlgClosed k] (hconj : ∀ (K : FiniteTypeCommHopfAlgCat k), Algebra.Smooth k ↑K.obj → geometricallyConnectedCommHopfAlgProperty k K.obj → ∀ (I J : HopfIdeal k ↑K.obj), IsBorelOverAlgClosed k K I → IsBorelOverAlgClosed k K J → ∃ (g : WithConv (↑K.obj →ₐ[k] k)), I.conjugate g = J) {I J : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) (hJ : IsBorelOverAlgClosed k H J) : ∃ (g : WithConv (↑H.obj →ₐ[k] k)), I.conjugate g = J

Borel conjugacy reduces to smooth connected affine groups. Over an algebraically closed field, a conjugacy theorem for all smooth geometrically connected finite-type affine groups implies conjugacy for every finite-type affine group, including nonreduced and disconnected ones. The conjugating point comes from the reduced identity component.