Closed projective orbits of connected solvable groups

A closed projective orbit of a reduced connected solvable affine group over an algebraically closed field consists of one point. This is the proper--affine step in the Borel fixed-point argument.

Lie--Kolchin places the whole orbit in an affine chart. Its orbit scheme is therefore affine: the closed orbit immersion factors as a closed immersion into that chart. On the other hand it is proper, being closed in projective space, so its structural morphism is finite. The orbit scheme is connected as a continuous image of the connected group scheme. A finite scheme over an algebraically closed field has discrete underlying space, hence this connected orbit scheme has only one point.

The conclusion applies to every scheme point of the group, not only to its rational points.

References

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

theorem TauCeti.Comodule.isAffine_projectiveOrbitScheme_of_isClosed_of_isSolvable {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))) : AlgebraicGeometry.IsAffine (projectiveOrbitScheme m hm)

The scheme of a closed projective orbit of a reduced connected solvable affine group is affine.

theorem TauCeti.Comodule.isFinite_projectiveOrbitToSpec_of_isClosed_of_isSolvable {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))) : AlgebraicGeometry.IsFinite (projectiveOrbitToSpec m hm)

The structural morphism of a closed projective orbit of a reduced connected solvable affine group is finite.

theorem TauCeti.Comodule.subsingleton_projectiveOrbitScheme_of_isClosed_of_isSolvable {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))) : Subsingleton ↥(projectiveOrbitScheme m hm)

The scheme of a closed projective orbit of a reduced connected solvable affine group has at most one point.

theorem TauCeti.Comodule.projectiveOrbitMap_eq_identity_of_isClosed_of_isSolvable {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))) (x : ↥(AlgebraicGeometry.Spec ↧H)) : (projectiveOrbitMap m hm) x = (projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint

If a projective orbit of a reduced connected solvable affine group is closed, then every scheme point of the group has the same image as the identity point.

theorem TauCeti.Comodule.range_projectiveOrbitMap_eq_singleton_of_isClosed_of_isSolvable {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))) : Set.range ⇑(projectiveOrbitMap m hm) = {(projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint}

A closed projective orbit of a reduced connected solvable affine group is the singleton containing the identity image.

theorem TauCeti.Comodule.map_span_eq_span_of_isClosed_range_projectiveOrbitMap_of_isSolvable {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hclosed : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))) (g : WithConv (H →ₐ[k] k)) : Submodule.map ((basePointsRepresentation M) g) (k ∙ m) = k ∙ m

Every rational point of a reduced connected solvable affine group preserves the line of a vector whose projective orbit is closed.