Projective orbits represent homogeneous quotients

Let G be a reduced affine group of finite type over an algebraically closed field k, let N be a closed subgroup, and let m be a vector in a finite-dimensional representation whose matrix coefficients detect the left cosets of N, as Chevalley's coset criterion provides. Then the fppf homogeneous quotient G/N is represented by the projective orbit scheme of the line through m: its fppf sheaf of points is isomorphic to G/N, compatibly with the projections from G. Every closed subgroup admits such a vector, so G/N is represented by a scheme, locally closed in a projective space.

The orbit scheme defines an fppf sheaf on affine k-schemes, CommAlgCat.pointsSheaf, because the fppf topology is subcanonical. The orbit map from G is invariant under N and descends to G/N. The descended map is locally injective because the orbit-map fibers are exactly the left cosets of N (Comodule.projectiveOrbitMap_SpecMap_eq_iff_exists_units_matrixCoefficient), and it is locally surjective because every point of the orbit lifts to G after a faithfully flat, finitely presented extension (Comodule.exists_faithfullyFlat_lift_toProjectiveOrbit). A locally bijective morphism of sheaves is an isomorphism.

Main declarations

• Comodule.projectiveOrbitPointsSheaf: the fppf sheaf of points of a projective orbit scheme.
• Comodule.toProjectiveOrbitPoints: the orbit map on points.
• Comodule.fppfHomogeneousQuotientToProjectiveOrbitPoints: the orbit map descended to G/N.
• Comodule.fppfHomogeneousQuotientIsoProjectiveOrbitPoints: G/N is represented by the projective orbit scheme.
• HopfIdeal.exists_fppfHomogeneousQuotient_iso_projectiveOrbitPoints: every closed subgroup has a projective orbit representing its homogeneous quotient.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and §§7.c–7.f.

noncomputable def TauCeti.Comodule.projectiveOrbitPointsSheaf {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1))

The fppf sheaf of points of the projective orbit scheme of a line: an affine k-scheme Spec A is sent to the morphisms Spec A ⟶ X over Spec k, lifted to Type (u + 1) to sit beside the fppf homogeneous quotient.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitPointsSheaf_obj {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : (projectiveOrbitPointsSheaf m hm).obj = ((AlgebraicGeometry.algSpec ↧k).op.comp (CategoryTheory.yoneda.obj (CategoryTheory.Over.mk (projectiveOrbitToSpec m hm)))).comp CategoryTheory.uliftFunctor.{u + 1, u}

The points of the projective orbit scheme over Spec A are its morphisms from Spec A over the base field.

theorem TauCeti.Comodule.SpecMap_toProjectiveOrbit_projectiveOrbitToSpec {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) {A : Type u} [CommRing A] [Algebra k A] (g : ↑H →ₐ[k] A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g.toRingHom)) (toProjectiveOrbit m hm)) (projectiveOrbitToSpec m hm) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k A))

An algebra-valued group point followed by the orbit map lies over the base field.

noncomputable def TauCeti.Comodule.toProjectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : (HopfAlgebra.pointsPresheaf H).comp CategoryTheory.uliftFunctor.{u + 1, u} ⟶ (projectiveOrbitPointsSheaf m hm).obj

The orbit map on points: an A-valued group point g is sent to the point Spec A ⟶ Spec H ⟶ X of the projective orbit scheme.

@[simp]

theorem TauCeti.Comodule.toProjectiveOrbitPoints_app_apply {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (A : (CommAlgCat k)ᵒᵖᵒᵖ) (g : ↑(HopfAlgebra.points (Opposite.unop (Opposite.unop A)))) : (CategoryTheory.ConcreteCategory.hom ((toProjectiveOrbitPoints m hm).app A)) { down := g } = ⋯ ▸ { down := CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑g.ofConv)) (toProjectiveOrbit m hm)) ⋯ }

The orbit point of g is Spec g followed by the orbit map.

theorem TauCeti.Comodule.toProjectiveOrbitPoints_app_eq_iff {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (A : (CommAlgCat k)ᵒᵖᵒᵖ) (g h : ↑(HopfAlgebra.points (Opposite.unop (Opposite.unop A)))) : (CategoryTheory.ConcreteCategory.hom ((toProjectiveOrbitPoints m hm).app A)) { down := g } = (CategoryTheory.ConcreteCategory.hom ((toProjectiveOrbitPoints m hm).app A)) { down := h } ↔ ∃ (c : (↑(Opposite.unop (Opposite.unop A)))ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)

Two algebra-valued group points have the same orbit point exactly when their matrix coefficients at m differ by one unit of the value algebra.

instance TauCeti.Comodule.isLocallySurjective_toProjectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] [IsReduced ↑H] (m : M) (hm : Module.IsUnimodular k m) : CategoryTheory.Presheaf.IsLocallySurjective (CommAlgCat.fppfTopology k) (toProjectiveOrbitPoints m hm)

Points of the orbit lift fppf locally to the group. For a reduced group, the orbit map on points is locally surjective for the fppf topology.

noncomputable def TauCeti.Comodule.fppfHomogeneousQuotientToProjectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (I : HopfIdeal k ↑H) (m : M) (hm : Module.IsUnimodular k m) (hcoset : ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)) : H.fppfHomogeneousQuotient I ⟶ projectiveOrbitPointsSheaf m hm

The orbit map descended to the fppf homogeneous quotient G/N, for a vector m whose matrix coefficients detect the left cosets of the closed subgroup N cut out by I.

@[simp]

theorem TauCeti.Comodule.fppfHomogeneousQuotientProjection_comp_toProjectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (I : HopfIdeal k ↑H) (m : M) (hm : Module.IsUnimodular k m) (hcoset : ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)) : CategoryTheory.CategoryStruct.comp (H.fppfHomogeneousQuotientProjection I) (fppfHomogeneousQuotientToProjectiveOrbitPoints I m hm hcoset).hom = toProjectiveOrbitPoints m hm

The descended orbit map restricts to the orbit map along the projection G ⟶ G/N.

@[simp]

theorem TauCeti.Comodule.fppfHomogeneousQuotientProjection_comp_toProjectiveOrbitPoints_assoc {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (I : HopfIdeal k ↑H) (m : M) (hm : Module.IsUnimodular k m) (hcoset : ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)) {Z : CategoryTheory.Functor (CommAlgCat k)ᵒᵖᵒᵖ (Type (u + 1))} (h : (projectiveOrbitPointsSheaf m hm).obj ⟶ Z) : CategoryTheory.CategoryStruct.comp (H.fppfHomogeneousQuotientProjection I) (CategoryTheory.CategoryStruct.comp (fppfHomogeneousQuotientToProjectiveOrbitPoints I m hm hcoset).hom h) = CategoryTheory.CategoryStruct.comp (toProjectiveOrbitPoints m hm) h

The descended orbit map restricts to the orbit map along the projection G ⟶ G/N.

instance TauCeti.Comodule.isIso_fppfHomogeneousQuotientToProjectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (I : HopfIdeal k ↑H) (m : M) (hm : Module.IsUnimodular k m) (hcoset : ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)) [IsReduced ↑H] : CategoryTheory.IsIso (fppfHomogeneousQuotientToProjectiveOrbitPoints I m hm hcoset)

Projective orbits represent homogeneous quotients. For a reduced finite-type group over an algebraically closed field and a vector whose matrix coefficients detect the left cosets of a closed subgroup N, the descended orbit map G/N ⟶ X is an isomorphism of fppf sheaves.

noncomputable def TauCeti.Comodule.fppfHomogeneousQuotientIsoProjectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (I : HopfIdeal k ↑H) (m : M) (hm : Module.IsUnimodular k m) (hcoset : ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)) [IsReduced ↑H] : H.fppfHomogeneousQuotient I ≅ projectiveOrbitPointsSheaf m hm

The homogeneous quotient G/N is represented by a projective orbit. For a reduced finite-type group over an algebraically closed field and a vector m whose matrix coefficients detect the left cosets of the closed subgroup N, the fppf quotient G/N is isomorphic to the sheaf of points of the projective orbit scheme of the line through m.

@[simp]

theorem TauCeti.Comodule.fppfHomogeneousQuotientIsoProjectiveOrbitPoints_hom {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k (↑H) M] [Module.Finite k M] (I : HopfIdeal k ↑H) (m : M) (hm : Module.IsUnimodular k m) (hcoset : ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)) [IsReduced ↑H] : (fppfHomogeneousQuotientIsoProjectiveOrbitPoints I m hm hcoset).hom = fppfHomogeneousQuotientToProjectiveOrbitPoints I m hm hcoset

The forward map of the representing isomorphism is the descended orbit map.

theorem TauCeti.HopfIdeal.exists_fppfHomogeneousQuotient_iso_projectiveOrbitPoints {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [IsReduced ↑H] (I : HopfIdeal k ↑H) : ∃ (M : Type u) (x : AddCommGroup M) (x_1 : Module k M) (x_2 : Comodule k (↑H) M) (x_3 : Module.Finite k M) (m : M) (hm : Module.IsUnimodular k m), Nonempty (H.fppfHomogeneousQuotient I ≅ Comodule.projectiveOrbitPointsSheaf m hm)

Homogeneous quotients are representable. For every closed subgroup N of a reduced affine group G of finite type over an algebraically closed field, there are a finite-dimensional representation of G and a line in it whose projective orbit scheme represents the fppf homogeneous quotient G/N.