Borel fixed points in projective representations

Let a reduced connected solvable affine group of finite type over an algebraically closed field act on the projective space of a finite-dimensional comodule. Every nonempty closed subset invariant under rational group translations contains a fixed point. The point is a rational line, and its orbit morphism is constant on all scheme points of the group.

This is the projective form of the Borel fixed-point theorem used for homogeneous spaces: once such a space is realized as a closed invariant subset of a projective representation, a connected solvable subgroup fixes a point. In particular, no fixed-vector assertion is made: the group may act on the fixed line through a nontrivial character.

The closed-orbit lemma supplies an orbit inside the invariant subset. Connectedness makes the group irreducible, and the proper--affine argument for closed solvable orbits makes that orbit a singleton. The two conclusions below express the resulting constant orbit and the fixed projective point, respectively.

References

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

theorem TauCeti.Comodule.exists_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] {Z : Set ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))} (hZ : IsClosed Z) (hne : Z.Nonempty) (hinvariant : ∀ (g : WithConv (H →ₐ[k] k)), Set.MapsTo (⇑(projectivePointTranslation g).hom) Z Z) : ∃ (m : M) (hm : Module.IsUnimodular k m), (projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint ∈ Z ∧ ∀ (x : ↥(AlgebraicGeometry.Spec ↧H)), (projectiveOrbitMap m hm) x = (projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint

Borel fixed-point theorem, orbit form. Every nonempty closed invariant subset of projective space contains a rational line whose full scheme-point orbit is a singleton.

theorem TauCeti.Comodule.exists_fixed_mem_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] {Z : Set ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))} (hZ : IsClosed Z) (hne : Z.Nonempty) (hinvariant : ∀ (g : WithConv (H →ₐ[k] k)), Set.MapsTo (⇑(projectivePointTranslation g).hom) Z Z) : ∃ x ∈ Z, x ∈ closedPoints ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M))) ∧ ∀ (g : WithConv (H →ₐ[k] k)), (projectivePointTranslation g).hom x = x

Borel fixed-point theorem, projective form. Every nonempty closed invariant subset of a projective representation of a reduced connected solvable affine group contains a closed point fixed by every rational group translation.