Translation invariance of projective orbit images

The linear automorphism attached to a base-valued group point induces a projective translation. The projective orbit morphism intertwines left translation on the source with projective translation as an equality of scheme morphisms. Consequently every projective translation preserves the entire orbit image, including its nonclosed points. This is the invariance input for proving that constructible projective orbits are locally closed.

The projective coordinates transform by precomposition of linear functionals with the original representation. No smoothness, reducedness, or finite-type hypothesis is required. The scheme equivariance holds over an arbitrary commutative base ring. Over a field, the final theorem identifies translation of a rational orbit image with the image of the left-multiplied group point. The assertions concern individual base-valued points; family-valued action diagrams additionally require compatibility with scalar extension.

References

• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f.
• Formal precursors: HopfAlgebra.leftTranslationAlgEquiv, the scalar-extended evaluation pairing, Proj.symmetricAlgebraMapIso, and Proj.symmetricAlgebraMulAction.

theorem TauCeti.Comodule.leftTranslationAlgEquiv_matrixCoefficient {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (φ : Module.Dual R M) (m : M) : (HopfAlgebra.leftTranslationAlgEquiv g) (matrixCoefficient φ m) = matrixCoefficient (φ ∘ₗ (basePointsRepresentation M) g) m

Left translation of a matrix coefficient acts on its functional by the original representation.

theorem TauCeti.Comodule.leftTranslationAlgEquiv_comp_orbitCoordinates {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (m : M) : (↑(HopfAlgebra.leftTranslationAlgEquiv g)).comp (orbitCoordinates m) = (orbitCoordinates m).comp (SymmetricAlgebra.map R (LinearMap.dualMap ((basePointsRepresentation M) g)))

Left translation of the homogeneous orbit coordinates is their precomposition with the symmetric-algebra map of the dual linear action.

noncomputable def TauCeti.Comodule.projectivePointTranslation {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ≅ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M))

The individual projective translation attached to a base-valued group point. The homogeneous coordinate module is the dual of the original representation.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def TauCeti.Comodule.projectivePointMulAction {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : MulAction (WithConv (H →ₐ[R] R)) ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)))

The action of base-valued group points on projective space, obtained from the contragredient representation. Install it locally to select this action.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Comodule.projectivePoint_smul_def {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (x : ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)))) : g • x = (projectivePointTranslation g).hom x

The selected projective action is the underlying map of projective translation.

theorem TauCeti.Comodule.projectivePointMulAction_continuousConstSMul {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : ContinuousConstSMul (WithConv (H →ₐ[R] R)) ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)))

Every translation of the selected projective point action is continuous.

@[simp]

theorem TauCeti.Comodule.projectivePointTranslation_one {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : projectivePointTranslation 1 = CategoryTheory.Iso.refl (AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)))

Translation by the identity point is the identity projective isomorphism.

@[simp]

theorem TauCeti.Comodule.projectivePointTranslation_mul {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g h : WithConv (H →ₐ[R] R)) : projectivePointTranslation (g * h) = projectivePointTranslation h ≪≫ projectivePointTranslation g

Projective translation by a convolution product composes the corresponding translations in the order of the point action.

@[simp]

theorem TauCeti.Comodule.projectivePointTranslation_inv_eq_symm {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) : projectivePointTranslation g⁻¹ = (projectivePointTranslation g).symm

Translation by the inverse point is the inverse projective isomorphism.

@[simp]

theorem TauCeti.Comodule.projectivePointTranslation_hom {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) : (projectivePointTranslation g).hom = AlgebraicGeometry.Proj.map (SymmetricAlgebra.gradedMap R (LinearMap.dualMap ((basePointsRepresentation M) g))) ⋯

The forward projective translation is the projective map induced by the dual linear map of the point action.

@[simp]

theorem TauCeti.Comodule.projectivePointTranslation_inv {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) : (projectivePointTranslation g).inv = AlgebraicGeometry.Proj.map (SymmetricAlgebra.gradedMap R (LinearMap.dualMap ((basePointsRepresentation M) g⁻¹))) ⋯

The inverse projective translation is the projective map induced by the dual linear map of the inverse point action.

theorem TauCeti.Comodule.projectivePointTranslation_preimage_basicOpen {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (s : SymmetricAlgebra R (Module.Dual R M)) : (TopologicalSpace.Opens.map (projectivePointTranslation g).hom.base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) s) = AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((SymmetricAlgebra.map R (LinearMap.dualMap ((basePointsRepresentation M) g))) s)

The coordinate pullback of the projective translation is induced by the point action on the dual module.

theorem TauCeti.Comodule.projectivePointTranslation_inv_preimage_basicOpen {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (s : SymmetricAlgebra R (Module.Dual R M)) : (TopologicalSpace.Opens.map (projectivePointTranslation g).inv.base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) s) = AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((SymmetricAlgebra.map R (LinearMap.dualMap ((basePointsRepresentation M) g⁻¹))) s)

The inverse projective translation pulls coordinates back by the dual point action of the inverse group point.

theorem TauCeti.Comodule.projectiveOrbitMap_leftTranslation {R H M : 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] (g : WithConv (H →ₐ[R] R)) (m : M) (hm : Module.IsUnimodular R m) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑(HopfAlgebra.leftTranslationAlgEquiv g)).toRingHom)) (projectiveOrbitMap m hm) = CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) (projectivePointTranslation g).hom

Left translation intertwines the orbit morphism with projective translation, including the maps on structure sheaves.

theorem TauCeti.Comodule.projectiveOrbitMap_leftTranslation_assoc {R H M : 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] (g : WithConv (H →ₐ[R] R)) (m : M) (hm : Module.IsUnimodular R m) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑(HopfAlgebra.leftTranslationAlgEquiv g)).toRingHom)) (CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) h) = CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) (CategoryTheory.CategoryStruct.comp (projectivePointTranslation g).hom h)

Left translation intertwines the orbit morphism with projective translation, including the maps on structure sheaves.

theorem TauCeti.Comodule.projectiveOrbitMap_leftTranslation_apply {R H M : 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] (g : WithConv (H →ₐ[R] R)) (m : M) (hm : Module.IsUnimodular R m) (x : PrimeSpectrum H) : (projectiveOrbitMap m hm) (PrimeSpectrum.comap (↑(HopfAlgebra.leftTranslationAlgEquiv g).toRingEquiv) x) = (projectivePointTranslation g).hom ((projectiveOrbitMap m hm) x)

Left translation on the full source spectrum intertwines the underlying orbit map with projective translation, including at nonclosed points.

theorem TauCeti.Comodule.image_projectivePointTranslation_range_projectiveOrbitMap {R H M : 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] (g : WithConv (H →ₐ[R] R)) (m : M) (hm : Module.IsUnimodular R m) : ⇑(projectivePointTranslation g).hom '' Set.range ⇑(projectiveOrbitMap m hm) = Set.range ⇑(projectiveOrbitMap m hm)

Every projective translation preserves the entire topological image of the orbit morphism, with no restriction to rational or closed points.

theorem TauCeti.Comodule.projectivePointTranslation_projectiveOrbitMap_kernelPoint {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (g h : WithConv (H →ₐ[k] k)) (m : M) (hm : Module.IsUnimodular k m) : (projectivePointTranslation g).hom ((projectiveOrbitMap m hm) (AlgHom.kernelPoint h.ofConv)) = (projectiveOrbitMap m hm) (AlgHom.kernelPoint (g * h).ofConv)

Projective translation of a rational orbit image corresponds to left multiplication of its group point.