The closed-orbit lemma for projective orbits

Let O be the orbit of a line [m] in the projective space P(V) of a finite-dimensional representation of an affine group of finite type over an algebraically closed field k, that is, the full image of the projective orbit morphism. Since O is locally closed, its boundary closure O \ O is closed (TauCeti.Comodule.isClosed_closure_diff_range_projectiveOrbitMap, in ProjectiveOrbit/LocallyClosed.lean).

The boundary has strictly smaller Krull dimension than O, including when the group is disconnected (TauCeti.Comodule.topologicalKrullDim_closure_diff_range_projectiveOrbitMap_lt, in ProjectiveOrbit/Dimension.lean). The orbit of a line [m'] in the boundary lies in the boundary (TauCeti.Comodule.closure_range_projectiveOrbitMap_subset_boundary, in ProjectiveOrbit/Boundary.lean), so it has strictly smaller dimension than O. A nonempty closed subset of the quasi-compact space P(V) contains a closed point, which is a line, so an orbit whose dimension is minimal among the orbits of the lines in its closure has empty boundary, that is, it is closed. By induction on the dimension, the closure of every orbit contains a closed orbit.

Neither connectedness, smoothness nor reducedness of the group is assumed.

Main declarations

• TauCeti.Comodule.topologicalKrullDim_range_projectiveOrbitMap_lt: the orbit of a line in the boundary of O has strictly smaller Krull dimension than O.
• TauCeti.Comodule.isClosed_range_projectiveOrbitMap_of_forall_mem_closure, TauCeti.Comodule.isClosed_range_projectiveOrbitMap_of_forall_mem: an orbit of minimal dimension is closed.
• TauCeti.Comodule.exists_isClosed_range_projectiveOrbitMap_subset_closure: the closure of every orbit contains a closed orbit.

References

• C. Chevalley, Classification des groupes de Lie algébriques, Séminaire Chevalley 1956–1958, Exposé 5, Lemme 4 and its corollary.
• A. Borel, Linear Algebraic Groups, 2nd ed., GTM 126, §1.8, the closed orbit lemma.
• J. E. Humphreys, Linear Algebraic Groups, GTM 21, §8.3.
• J. S. Milne, Algebraic Groups (2017), §7.c, orbits and isotropy groups.

theorem TauCeti.Comodule.topologicalKrullDim_range_projectiveOrbitMap_lt {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] {m m' : M} (hm : Module.IsUnimodular k m) (hm' : Module.IsUnimodular k m') (hm'O : (projectiveOrbitMap m' hm') (Bialgebra.counitAlgHom k H).kernelPoint ∈ closure (Set.range ⇑(projectiveOrbitMap m hm)) \ Set.range ⇑(projectiveOrbitMap m hm)) : topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m' hm')) < topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm))

Boundary orbits are smaller. If the line [m'] lies in the boundary closure O \ O of the orbit O of [m], then the orbit of [m'] has strictly smaller Krull dimension than O.

theorem TauCeti.Comodule.isClosed_range_projectiveOrbitMap_of_forall_mem_closure {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (hmin : ∀ (m' : M) (hm' : Module.IsUnimodular k m'), (projectiveOrbitMap m' hm') (Bialgebra.counitAlgHom k H).kernelPoint ∈ closure (Set.range ⇑(projectiveOrbitMap m hm)) → topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm)) ≤ topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m' hm'))) : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))

Closed-orbit lemma. If the orbit O of a line has minimal Krull dimension among the orbits of the lines in its closure, then O is closed.

theorem TauCeti.Comodule.isClosed_range_projectiveOrbitMap_of_forall_mem {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) {Z : Set ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))} (hZ : IsClosed Z) (hmZ : Set.range ⇑(projectiveOrbitMap m hm) ⊆ Z) (hmin : ∀ (m' : M) (hm' : Module.IsUnimodular k m'), (projectiveOrbitMap m' hm') (Bialgebra.counitAlgHom k H).kernelPoint ∈ Z → topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm)) ≤ topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m' hm'))) : IsClosed (Set.range ⇑(projectiveOrbitMap m hm))

Closed-orbit lemma, relative form. If the orbit O of a line lies in a closed subset Z of projective space and has minimal Krull dimension among the orbits of the lines in Z, then O is closed.

theorem TauCeti.Comodule.exists_isClosed_range_projectiveOrbitMap_subset_closure {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : ∃ (m' : M) (hm' : Module.IsUnimodular k m'), IsClosed (Set.range ⇑(projectiveOrbitMap m' hm')) ∧ Set.range ⇑(projectiveOrbitMap m' hm') ⊆ closure (Set.range ⇑(projectiveOrbitMap m hm))

Existence of closed orbits. The closure of the orbit of every line contains a closed orbit of a line.

theorem TauCeti.Comodule.exists_isClosed_range_projectiveOrbitMap_subset_of_isClosed {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [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), IsClosed (Set.range ⇑(projectiveOrbitMap m hm)) ∧ Set.range ⇑(projectiveOrbitMap m hm) ⊆ Z

Every nonempty closed subset of projective space invariant under rational group translations contains a closed orbit.