Projective orbit schemes

For a finite-dimensional representation of a finite-type affine group scheme over an algebraically closed field, the orbit of a line has a locally closed scheme structure. Construct it as the scheme-theoretic image of the projective orbit morphism inside the coborder of its topological image. The resulting immersion has exactly the full orbit image, including its nonclosed points. The map from the group to the orbit scheme is surjective, quasi-compact, locally of finite type, and scheme-theoretically dominant.

This is the scheme on which to study flatness of the orbit map and its comparison with the homogeneous quotient by the stabilizer of the line. Flatness and that quotient comparison are separate results. No smoothness or reducedness hypothesis is imposed on the group; when the group is reduced, so is the orbit scheme.

The construction combines Comodule.isLocallyClosed_range_projectiveOrbitMap with Scheme.Hom.locallyClosedImage and its factorization API.

References

• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f, orbits and homogeneous spaces.
• The Stacks Project, Tag 01R5, scheme-theoretic images.

@[reducible, inline]

noncomputable abbrev TauCeti.Comodule.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) : AlgebraicGeometry.Scheme

The projective orbit scheme of the line generated by a unimodular vector. Its scheme structure is the scheme-theoretic image inside the coborder of the orbit.

Equations

• TauCeti.Comodule.projectiveOrbitScheme m hm = AlgebraicGeometry.Scheme.Hom.locallyClosedImage (TauCeti.Comodule.projectiveOrbitMap m hm) ⋯

noncomputable def TauCeti.Comodule.projectiveOrbitι {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) : projectiveOrbitScheme m hm ⟶ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M))

The inclusion of the projective orbit scheme into projective space.

Equations

• TauCeti.Comodule.projectiveOrbitι m hm = AlgebraicGeometry.Scheme.Hom.locallyClosedImageι (TauCeti.Comodule.projectiveOrbitMap m hm) ⋯

noncomputable def TauCeti.Comodule.toProjectiveOrbit {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) : AlgebraicGeometry.Spec ↧H ⟶ projectiveOrbitScheme m hm

The orbit morphism with its target restricted to the projective orbit scheme.

Equations

• TauCeti.Comodule.toProjectiveOrbit m hm = AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage (TauCeti.Comodule.projectiveOrbitMap m hm) ⋯

theorem TauCeti.Comodule.projectiveOrbitι_def {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) : projectiveOrbitι m hm = AlgebraicGeometry.Scheme.Hom.locallyClosedImageι (projectiveOrbitMap m hm) ⋯

The orbit inclusion is the inclusion of the locally closed scheme image.

theorem TauCeti.Comodule.toProjectiveOrbit_def {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) : toProjectiveOrbit m hm = AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage (projectiveOrbitMap m hm) ⋯

The orbit factorization is the canonical map onto the locally closed scheme image.

instance TauCeti.Comodule.instIsImmersionProjectiveOrbitι {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) : AlgebraicGeometry.IsImmersion (projectiveOrbitι m hm)

The projective orbit scheme is a locally closed subscheme of projective space.

@[simp]

theorem TauCeti.Comodule.toProjectiveOrbit_projectiveOrbitι {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) : CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) (projectiveOrbitι m hm) = projectiveOrbitMap m hm

The map onto the orbit scheme followed by its inclusion is the original orbit morphism.

@[simp]

theorem TauCeti.Comodule.toProjectiveOrbit_projectiveOrbitι_assoc {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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) (CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) h) = CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) h

The map onto the orbit scheme followed by its inclusion is the original orbit morphism.

instance TauCeti.Comodule.instSurjectiveToProjectiveOrbit {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) : AlgebraicGeometry.Surjective (toProjectiveOrbit m hm)

Every point of the orbit scheme comes from a point of the group scheme.

@[simp]

theorem TauCeti.Comodule.range_projectiveOrbitι {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) : Set.range ⇑(projectiveOrbitι m hm) = Set.range ⇑(projectiveOrbitMap m hm)

The orbit scheme has exactly the topological image of the original orbit morphism.

instance TauCeti.Comodule.instIsSchemeTheoreticallyDominantToProjectiveOrbit {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) : AlgebraicGeometry.IsSchemeTheoreticallyDominant (toProjectiveOrbit m hm)

The orbit map does not factor through any proper closed subscheme of the orbit scheme.

instance TauCeti.Comodule.instLocallyOfFiniteTypeToProjectiveOrbit {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) : AlgebraicGeometry.LocallyOfFiniteType (toProjectiveOrbit m hm)

The map onto the orbit scheme is locally of finite type.

instance TauCeti.Comodule.instIsReducedProjectiveOrbitScheme {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] [IsReduced H] (m : M) (hm : Module.IsUnimodular k m) : AlgebraicGeometry.IsReduced (projectiveOrbitScheme m hm)

The orbit scheme of a reduced affine group scheme is reduced.

instance TauCeti.Comodule.instIsNoetherianProjectiveOrbitScheme {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) : AlgebraicGeometry.IsNoetherian (projectiveOrbitScheme m hm)

The orbit scheme is Noetherian, including when the group is nonreduced.

noncomputable def TauCeti.Comodule.projectiveOrbitToSpec {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) : projectiveOrbitScheme m hm ⟶ AlgebraicGeometry.Spec ↧k

The structural morphism of the projective orbit scheme over the base field.

Equations

• TauCeti.Comodule.projectiveOrbitToSpec m hm = CategoryTheory.CategoryStruct.comp (TauCeti.Comodule.projectiveOrbitι m hm) (TauCeti.SymmetricAlgebra.projToSpec k (Module.Dual k M))

theorem TauCeti.Comodule.projectiveOrbitToSpec_def {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) : projectiveOrbitToSpec m hm = CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) (SymmetricAlgebra.projToSpec k (Module.Dual k M))

The structural morphism is inherited from the ambient projective space.

@[simp]

theorem TauCeti.Comodule.toProjectiveOrbit_projectiveOrbitToSpec {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) : CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) (projectiveOrbitToSpec m hm) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k H))

The orbit factorization is a morphism over the base field.

@[simp]

theorem TauCeti.Comodule.toProjectiveOrbit_projectiveOrbitToSpec_assoc {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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) (CategoryTheory.CategoryStruct.comp (projectiveOrbitToSpec m hm) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k H))) h

The orbit factorization is a morphism over the base field.

instance TauCeti.Comodule.instLocallyOfFiniteTypeProjectiveOrbitToSpec {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) : AlgebraicGeometry.LocallyOfFiniteType (projectiveOrbitToSpec m hm)

The projective orbit scheme is locally of finite type over its base field.

instance TauCeti.Comodule.instJacobsonSpaceProjectiveOrbitScheme {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) : JacobsonSpace ↥(projectiveOrbitScheme m hm)

Closed points are dense in every locally closed subset of the orbit scheme.