Projective orbit morphisms under restriction of representations

Restricting a representation along a morphism of affine group schemes pulls back its projective orbit morphism along that morphism. The result is an equality of scheme morphisms over arbitrary commutative rings, rather than only an equality on rational points. It applies in particular to the restriction to a closed subgroup.

The coordinate formula is CoalgHom.matrixCoefficient_corestrict. The scheme comparison combines Comodule.projectiveOrbitMap with AlgebraicGeometry.Proj.fromOfGlobalSections_naturality.

References

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

@[simp]

theorem BialgHom.orbitCoordinates_corestrict {R : Type u} {H : Type v} {K : Type w} {M : Type x} [CommSemiring R] [CommSemiring H] [CommSemiring K] [Bialgebra R H] [Bialgebra R K] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R H M] (f : H →ₐc[R] K) (m : M) : TauCeti.Comodule.orbitCoordinates m = (↑f).comp (TauCeti.Comodule.orbitCoordinates m)

Restricting the representation pulls its homogeneous orbit coordinates back along the coordinate bialgebra morphism.

theorem BialgHom.projectiveOrbitMap_corestrict {R H K M : Type u} [CommRing R] [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R H M] [Module.Finite R M] [Module.Projective R M] (f : H →ₐc[R] K) (m : M) (hm : Module.IsUnimodular R m) : TauCeti.Comodule.projectiveOrbitMap m hm = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑f).toRingHom)) (TauCeti.Comodule.projectiveOrbitMap m hm)

Restriction along a morphism of affine group schemes pulls back the projective orbit morphism. This includes restriction to nonreduced closed subgroup schemes.

theorem BialgHom.projectiveOrbitMap_corestrict_assoc {R H K M : Type u} [CommRing R] [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R H M] [Module.Finite R M] [Module.Projective R M] (f : H →ₐc[R] K) (m : M) (hm : Module.IsUnimodular R m) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.Comodule.projectiveOrbitMap m hm) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑f).toRingHom)) (CategoryTheory.CategoryStruct.comp (TauCeti.Comodule.projectiveOrbitMap m hm) h)

Restriction along a morphism of affine group schemes pulls back the projective orbit morphism. This includes restriction to nonreduced closed subgroup schemes.