Solvability detected by closed projective orbits

Let G be an affine group of finite type over an algebraically closed field k. A closed orbit of a line [m] in the projective space of a finite-dimensional representation is trivial when the line is a subrepresentation, that is, when the stabilizer of k ∙ m is all of G. This file shows that G is solvable exactly when every closed projective orbit is trivial, provided G is reduced and connected.

If every closed orbit is trivial, then every nonzero finite-dimensional representation has a weight vector: the whole projective space is a nonempty closed invariant set, so it contains a closed orbit, whose line is then a subrepresentation. By the triangular embedding criterion, G is then a closed subgroup of an upper-triangular group, hence solvable. This direction needs neither reducedness nor connectedness. Conversely, for a reduced connected solvable group the Borel fixed-point theorem makes every closed orbit a single point, so its line is stable under all rational points, and reducedness promotes this to a subrepresentation.

The first direction is the input for an induction on dimension in the conjugacy of Borel subgroups. A group that is not solvable has a closed projective orbit whose stabilizer is a proper closed subgroup, and every reduced connected solvable closed subgroup is contained in a conjugate of that proper subgroup.

Main declarations

• TauCeti.Comodule.isSolvable_points_of_forall_stabilizerHopfIdeal_eq_bot_of_isClosed: if every closed projective orbit of an affine group is trivial, its points with values in every commutative algebra form a solvable group.
• TauCeti.Comodule.isSolvable_iff_forall_stabilizerHopfIdeal_eq_bot_of_isClosed: a reduced connected group is solvable exactly when all of its closed projective orbits are trivial.
• TauCeti.Comodule.mem_quotientPointsSubgroup_stabilizerHopfIdeal_span_iff: the rational points of the stabilizer of k ∙ m are the rational points fixing the orbit base point [m].
• TauCeti.HopfIdeal.exists_ne_bot_forall_exists_conjugate_le_of_not_isSolvable: an affine group that is not solvable has a proper closed subgroup containing a conjugate of every reduced connected solvable closed subgroup.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §§10.4 and 11.1.
• J. S. Milne, Algebraic Groups (2017), Chapter 16 and Theorem 17.5.

theorem TauCeti.Comodule.mem_quotientPointsSubgroup_stabilizerHopfIdeal_span_iff {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (Submodule.stabilizerHopfIdeal H (k ∙ m)) ↧k ↔ (projectiveOrbitMap m hm) g.ofConv.kernelPoint = (projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint

The rational points of the stabilizer of the line k ∙ m are exactly the rational points fixing the base point [m] of its projective orbit.

theorem TauCeti.Comodule.isSolvable_points_of_forall_stabilizerHopfIdeal_eq_bot_of_isClosed {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (horbit : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module k M] [inst_2 : Comodule k H M] [inst_3 : Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m), IsClosed (Set.range ⇑(projectiveOrbitMap m hm)) → Submodule.stabilizerHopfIdeal H (k ∙ m) = ⊥) (A : Type w) [CommRing A] [Algebra k A] : Group.IsSolvable (WithConv (H →ₐ[k] A))

Solvability from trivial closed orbits. If the line of every closed projective orbit of an affine group of finite type over an algebraically closed field is a subrepresentation, then the points of the group with values in every commutative algebra form a solvable group.

theorem TauCeti.Comodule.isSolvable_iff_forall_stabilizerHopfIdeal_eq_bot_of_isClosed {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] : Group.IsSolvable (WithConv (H →ₐ[k] k)) ↔ ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module k M] [inst_2 : Comodule k H M] [inst_3 : Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m), IsClosed (Set.range ⇑(projectiveOrbitMap m hm)) → Submodule.stabilizerHopfIdeal H (k ∙ m) = ⊥

Closed-orbit criterion for solvability. A reduced connected affine group of finite type over an algebraically closed field is solvable exactly when the line of each of its closed projective orbits is a subrepresentation.

theorem TauCeti.HopfIdeal.exists_ne_bot_forall_exists_conjugate_le_of_not_isSolvable {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (hH : ¬Group.IsSolvable (WithConv (↑H.obj →ₐ[k] k))) : ∃ (D : HopfIdeal k ↑H.obj), 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))], ∃ (g : WithConv (↑H.obj →ₐ[k] k)), D.conjugate g ≤ I

A proper subgroup containing all connected solvable subgroups up to conjugacy. An affine group of finite type over an algebraically closed field whose rational points do not form a solvable group has a proper closed subgroup containing a conjugate of every reduced connected closed subgroup with solvable rational points.