Krull dimension of projective orbits

The projective orbit scheme of a line is a locally closed subscheme of projective space whose underlying set is the orbit, the full image of the projective orbit morphism. Since an immersion is a homeomorphism onto its image, the orbit scheme and the orbit have the same Krull dimension. The orbit has finite Krull dimension because projective space over a field is quasi-compact and of finite type. Only finite-dimensionality of the representation is needed for the latter. A locally closed subset of a finite-type scheme has the dimension of its closure, and its boundary has strictly smaller dimension if the subset is nonempty. Thus these orbit dimension statements apply also to disconnected groups.

Main declarations

• TauCeti.Comodule.topologicalKrullDim_projectiveOrbitScheme: the orbit scheme has the Krull dimension of the orbit.
• TauCeti.Comodule.topologicalKrullDim_range_projectiveOrbitMap_ne_top and TauCeti.Comodule.exists_topologicalKrullDim_range_projectiveOrbitMap_eq_natCast: the orbit has finite Krull dimension, a natural number.
• TauCeti.Comodule.topologicalKrullDim_range_projectiveOrbitMap_add_one_le_finrank: the orbit of a line in M has Krull dimension at most dim M - 1.
• TauCeti.Comodule.topologicalKrullDim_closure_range_projectiveOrbitMap: the orbit of a line has the Krull dimension of its closure.
• TauCeti.Comodule.topologicalKrullDim_closure_diff_range_projectiveOrbitMap_lt: its boundary has strictly smaller Krull dimension.

References

• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f, orbits and homogeneous spaces.

theorem TauCeti.Comodule.topologicalKrullDim_range_projectiveOrbitMap_ne_top {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm)) ≠ ⊤

The orbit of a line, the image of its projective orbit morphism, has finite Krull dimension. No finiteness or algebraic closedness hypothesis is needed beyond finite dimensionality of the representation.

theorem TauCeti.Comodule.exists_topologicalKrullDim_range_projectiveOrbitMap_eq_natCast {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : ∃ (n : ℕ), topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm)) = ↑n

The orbit of a line has the Krull dimension of a natural number: it is finite, and it is not ⊥ because the orbit is nonempty.

theorem TauCeti.Comodule.topologicalKrullDim_range_projectiveOrbitMap_add_one_le_finrank {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm)) + 1 ≤ ↑(Module.finrank k M)

Orbits have dimension at most that of the projective space. The orbit of a line in M has Krull dimension at most dim M - 1.

theorem TauCeti.Comodule.topologicalKrullDim_projectiveOrbitScheme {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) : topologicalKrullDim ↥(projectiveOrbitScheme m hm) = topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm))

The projective orbit scheme of a line has the Krull dimension of the orbit.

theorem TauCeti.Comodule.topologicalKrullDim_closure_range_projectiveOrbitMap {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) : topologicalKrullDim ↑(closure (Set.range ⇑(projectiveOrbitMap m hm))) = topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm))

The orbit of a line has the Krull dimension of its closure, including for disconnected groups.

theorem TauCeti.Comodule.topologicalKrullDim_closure_diff_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) (hm : Module.IsUnimodular k m) : topologicalKrullDim ↑(closure (Set.range ⇑(projectiveOrbitMap m hm)) \ Set.range ⇑(projectiveOrbitMap m hm)) < topologicalKrullDim ↑(Set.range ⇑(projectiveOrbitMap m hm))

The boundary closure O \ O of the orbit O of a line has strictly smaller Krull dimension than O, including for disconnected groups.