Constructibility of projective orbit images

The projective orbit morphism of a unimodular vector in a finite projective Hopf comodule is quasi-compact over any commutative base ring. It is locally of finite type when the coordinate Hopf algebra is finitely generated over the base. Over a Noetherian base it is also locally of finite presentation, so its image in projective space is constructible.

This supplies the constructibility input for realizing homogeneous spaces as locally closed projective orbits. The image here is the image of the underlying scheme map, including nonclosed points; it is not merely the orbit of the base-field-valued points. No smoothness, reducedness, or characteristic assumption is made. Local closedness and identification with a homogeneous quotient are separate assertions.

The construction combines Comodule.projectiveOrbitMap, the structural morphism SymmetricAlgebra.projToSpec, and Mathlib's scheme-theoretic Chevalley theorem Scheme.Hom.isConstructible_image.

References

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

@[simp]

theorem TauCeti.Comodule.projectiveOrbitMap_projToSpec {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] (m : M) (hm : Module.IsUnimodular R m) : CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) (SymmetricAlgebra.projToSpec R (Module.Dual R M)) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R H))

The projective orbit morphism commutes with the structural morphisms over the base ring.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitMap_projToSpec_assoc {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] (m : M) (hm : Module.IsUnimodular R m) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) (CategoryTheory.CategoryStruct.comp (SymmetricAlgebra.projToSpec R (Module.Dual R M)) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R H))) h

The projective orbit morphism commutes with the structural morphisms over the base ring.

instance TauCeti.Comodule.instQuasiCompactProjectiveOrbitMap {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] (m : M) (hm : Module.IsUnimodular R m) : AlgebraicGeometry.QuasiCompact (projectiveOrbitMap m hm)

A projective orbit morphism is quasi-compact over any commutative base ring.

instance TauCeti.Comodule.instLocallyOfFiniteTypeProjectiveOrbitMap {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] [Algebra.FiniteType R H] (m : M) (hm : Module.IsUnimodular R m) : AlgebraicGeometry.LocallyOfFiniteType (projectiveOrbitMap m hm)

A projective orbit morphism of a finite-type affine group scheme is locally of finite type over any commutative base ring.

theorem TauCeti.Comodule.isConstructible_range_projectiveOrbitMap {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] [Algebra.FiniteType R H] [IsNoetherianRing R] (m : M) (hm : Module.IsUnimodular R m) : Topology.IsConstructible (Set.range ⇑(projectiveOrbitMap m hm))

Over a Noetherian base, the scheme-theoretic topological image of a finite-type affine group's projective orbit morphism is constructible, even for nonreduced groups.