Affine charts containing solvable projective orbits

Every projective orbit of a reduced connected solvable affine group over an algebraically closed field lies in a single standard affine chart of projective space. This assertion concerns the entire scheme-point image, including its nonclosed points.

Lie--Kolchin supplies a triangular basis with group-like diagonal entries. The last nonzero coordinate of the vector, normalized to take value one, pulls back to a group-like matrix coefficient. That coefficient is a unit of the coordinate Hopf algebra, so the corresponding projective chart pulls back to the whole group scheme.

This is the affine-chart step in the Borel fixed-point argument: a closed projective orbit contained in this chart can be studied as a closed subscheme of an affine scheme. Containment in a chart alone does not assert that an arbitrary orbit is affine or closed.

theorem TauCeti.Comodule.exists_isAffineOpen_range_projectiveOrbitMap_subset_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) : ∃ (φ : Module.Dual k M), AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)) ((SymmetricAlgebra.ι k (Module.Dual k M)) φ)) ∧ Set.range ⇑(projectiveOrbitMap m hm) ⊆ ↑(AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)) ((SymmetricAlgebra.ι k (Module.Dual k M)) φ))

Every projective orbit of a reduced connected solvable affine group over an algebraically closed field is contained in one standard affine chart. The containment includes all scheme points, not just rational points.