Zariski-local fibers of projective orbit morphisms

Two algebra-valued group points have the same image under a projective orbit morphism if and only if their matrix coefficients at the chosen vector differ by one unit locally on an affine open cover of the value scheme. This removes the requirement that both points lie in one global standard chart. It compares full scheme morphisms and applies to nonreduced value rings.

The chosen vector is unimodular in a finite projective comodule. Its matrix coefficients generate the unit ideal, so the linear chart opens cover the value scheme. The criterion is the projective part of the comparison between orbit fibers and locally equal cosets of a line stabilizer.

References

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

theorem TauCeti.Comodule.projectiveOrbitMap_SpecMap_eq_iff_exists_affineOpenCover_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) : 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) ↔ ∃ (𝒰 : (AlgebraicGeometry.Spec ↧A).OpenCover), (∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)) ∧ ∀ (i : 𝒰.I₀), ∃ (c : (↑((𝒰.X i).presheaf.obj (Opposite.op ⊤)))ˣ), ∀ (φ : Module.Dual R M), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (𝒰.f i))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧A).inv) (h (matrixCoefficient φ m))) = ↑c * (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (𝒰.f i))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧A).inv) (g (matrixCoefficient φ m)))

Equality of projective orbit images is equivalent to Zariski-local unit proportionality of matrix coefficients. The affine open cover and the unit on each member are existential; no global chart or reducedness hypothesis is required.