Algebra-valued fibers of projective orbit maps on standard charts

For two algebra-valued group points whose orbit images lie on the same standard chart, the resulting morphisms to projective space agree exactly when their matrix coefficients at the chosen vector differ by one unit. These are equalities of scheme morphisms, so the criterion detects infinitesimal information over nonreduced value rings. It supplies the local fiber comparison between a projective orbit and a quotient by a line stabilizer.

No smoothness, reducedness, field, or finite-type hypothesis is imposed on the group or the value ring. The chosen vector belongs to a finite projective comodule and is unimodular, and the chart is specified by a linear functional whose evaluated matrix coefficient is a unit at both points.

The chart computation follows Comodule.projectiveOrbitMap and Proj.fromOfGlobalSections_naturality. Unit rescaling is tested by the degree-zero localization maps, rather than by the underlying homogeneous prime ideals.

References

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

theorem TauCeti.Comodule.projectiveOrbitMap_SpecMap_eq_awayLift {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) (hg : IsUnit (g (matrixCoefficient φ m))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g.toRingHom)) (projectiveOrbitMap m hm) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) (g.comp (orbitCoordinates m)).toRingHom ⋯))) (AlgebraicGeometry.Proj.awayι (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((SymmetricAlgebra.ι R (Module.Dual R M)) φ) ⋯ ⋯)

On a chart with a unit evaluated matrix coefficient, an algebra-valued orbit map is Spec of the degree-zero homogeneous coordinate map followed by the chart inclusion.

theorem TauCeti.Comodule.projectiveOrbitMap_SpecMap_eq_iff_exists_unit {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) (φ : Module.Dual R M) (hg : IsUnit (g (matrixCoefficient φ m))) (hh : IsUnit (h (matrixCoefficient φ m))) : 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)

Two algebra-valued orbit maps on the same linear chart agree exactly when their matrix coefficients at the chosen vector differ by a common unit. This compares full scheme morphisms, including their structure-sheaf maps.