Solvable subgroups and closed projective orbits

A reduced connected solvable group mapping to an affine group fixes a rational point of every closed projective orbit of the latter. The ambient group need not be connected or reduced. Restriction of the representation makes the orbit an invariant closed subset for the solvable group, so the projective Borel fixed-point theorem applies.

Consequently a reduced connected solvable closed subgroup is contained in a conjugate of the stabilizer of such an orbit's base point. The conclusion is an inclusion of closed subgroup schemes: reducedness of the solvable subgroup upgrades rational-point containment to an inclusion of defining Hopf ideals. This is the fixed-point step in conjugacy of Borel subgroups with projective homogeneous space.

The proof uses Comodule.exists_fixed_mem_of_isClosed_of_isSolvable, the rational-point description of projective orbits, and HopfIdeal.le_of_quotientPointsSubgroup_le.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §§10--11.
• J. S. Milne, Algebraic Groups (2017), Theorems 17.5--17.6.

theorem BialgHom.exists_projectiveOrbitMap_kernelPoint_fixed_of_isClosed_of_isSolvable {k H K M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [CommRing K] [HopfAlgebra k K] [Algebra.FiniteType k K] [IsReduced K] [ConnectedSpace (PrimeSpectrum K)] [Group.IsSolvable (WithConv (K →ₐ[k] k))] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] [Module.Finite k M] (f : H →ₐc[k] K) (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(TauCeti.Comodule.projectiveOrbitMap m hm))) : ∃ (g : WithConv (H →ₐ[k] k)), ∀ (h : WithConv (K →ₐ[k] k)), (TauCeti.Comodule.projectivePointTranslation (f.mapDomain h)).hom ((TauCeti.Comodule.projectiveOrbitMap m hm) g.ofConv.kernelPoint) = (TauCeti.Comodule.projectiveOrbitMap m hm) g.ofConv.kernelPoint

A morphism from a reduced connected solvable group fixes a rational point of every closed projective orbit of the target group. The fixed point is exhibited as the orbit image of an ambient rational group point.

theorem TauCeti.HopfIdeal.exists_conjugate_le_of_isClosed_projectiveOrbit {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [Module.Finite k M] (D I : HopfIdeal k ↑H.obj) [IsReduced ↑(H.quotient I).obj] [ConnectedSpace (PrimeSpectrum ↑(H.quotient I).obj)] [Group.IsSolvable (WithConv (↑(H.quotient I).obj →ₐ[k] k))] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(Comodule.projectiveOrbitMap m hm))) (hstab : ∀ (a : WithConv (↑H.obj →ₐ[k] k)), a ∈ CommHopfAlgCat.quotientPointsSubgroup H.obj D ↧k ↔ (Comodule.projectiveOrbitMap m hm) a.ofConv.kernelPoint = (Comodule.projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k ↑H.obj).kernelPoint) : ∃ (g : WithConv (↑H.obj →ₐ[k] k)), D.conjugate g ≤ I

A reduced connected solvable closed subgroup is contained scheme-theoretically in a conjugate of the stabilizer of a point in a closed projective orbit. The stabilizer is specified by its rational-point fiber; no smoothness of that stabilizer is required.