Fibers of projective orbit morphisms

Two algebra-valued group points have the same image under a projective orbit morphism exactly when their matrix coefficients at the chosen vector differ by one global unit of the value algebra. Combined with Chevalley's coset criterion, which detects the left cosets of a closed subgroup by exactly this unit proportionality, the fibers of the orbit map of a Chevalley line are the left cosets of the subgroup. This is the fiber half of the comparison between the projective orbit and the homogeneous quotient.

Equality of scheme morphisms is local, so the chart criterion only gives unit proportionality locally. The local proportionality says that all 2 × 2 minors of the two coordinate families vanish, which is a condition on the value algebra itself; two coordinate families generating the unit ideal with vanishing minors are unit multiples of one another (TauCeti.forall_mul_eq_mul_iff_exists_units). The value algebra may be nonreduced, and no field hypothesis is imposed on the base ring.

Main declarations

• Comodule.SpecMap_projectiveOrbitMap_preimage_basicOpen_ι: the pullback of a standard chart along an algebra-valued orbit map is the principal open of the evaluated matrix coefficient.
• Comodule.projectiveOrbitMap_SpecMap_eq_iff_exists_units_matrixCoefficient: equality of algebra-valued orbit maps is global unit proportionality of matrix coefficients.

References

• J. S. Milne, Algebraic Groups (2017), §§7.d–7.f.

theorem TauCeti.Comodule.SpecMap_projectiveOrbitMap_preimage_basicOpen_ι {R H M A : 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] [CommRing A] [Algebra R A] (m : M) (hm : Module.IsUnimodular R m) (g : H →ₐ[R] A) (φ : Module.Dual R M) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g.toRingHom)) (projectiveOrbitMap m hm)).base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((SymmetricAlgebra.ι R (Module.Dual R M)) φ)) = (AlgebraicGeometry.Spec ↧A).basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧A).inv) (g (matrixCoefficient φ m)))

The standard chart of a linear coordinate pulls back along an algebra-valued orbit map to the principal open of the evaluated matrix coefficient.

theorem TauCeti.Comodule.projectiveOrbitMap_SpecMap_eq_iff_exists_units_matrixCoefficient {R H M A : 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] [CommRing A] [Algebra R A] (m : M) (hm : Module.IsUnimodular R m) (g h : H →ₐ[R] A) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g.toRingHom)) (projectiveOrbitMap m hm) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom h.toRingHom)) (projectiveOrbitMap m hm) ↔ ∃ (c : Aˣ), ∀ (φ : Module.Dual R M), h (matrixCoefficient φ m) = ↑c * g (matrixCoefficient φ m)

Fibers of algebra-valued orbit maps. Two algebra-valued group points have the same image in projective space exactly when their matrix coefficients at the chosen vector differ by one global unit of the value algebra. The value algebra may be nonreduced.