Translations of projective orbit schemes

Every rational group point induces an automorphism of the projective orbit scheme of a line. The orbit inclusion intertwines this automorphism with ambient projective translation, and the map from the group to the orbit intertwines it with left translation. These are equalities of scheme morphisms, retaining the possibly nonreduced structure of the orbit. The automorphisms preserve the structural morphism to the base field.

This provides the translations needed to transport local properties of the orbit map between rational translates. It does not assert flatness or identify the orbit scheme with the fppf homogeneous quotient.

The construction combines Comodule.projectiveOrbitMap_leftTranslation, Comodule.toProjectiveOrbit, and the lifting property of an immersion after a surjective, scheme-theoretically dominant morphism.

References

• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f, orbits and homogeneous spaces.

noncomputable def TauCeti.Comodule.projectiveOrbitTranslation {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : projectiveOrbitScheme m hm ≅ projectiveOrbitScheme m hm

Rational translation on the locally closed projective orbit, with its full scheme-theoretic image structure.

Equations

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

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_hom_ι {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).hom (projectiveOrbitι m hm) = CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) (projectivePointTranslation g).hom

The orbit inclusion intertwines orbit translation with ambient projective translation.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_hom_ι_assoc {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).hom (CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) h) = CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) (CategoryTheory.CategoryStruct.comp (projectivePointTranslation g).hom h)

The orbit inclusion intertwines orbit translation with ambient projective translation.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_inv_ι {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).inv (projectiveOrbitι m hm) = CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) (projectivePointTranslation g).inv

Inverse orbit translation restricts the inverse ambient projective translation.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_inv_ι_assoc {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).inv (CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) h) = CategoryTheory.CategoryStruct.comp (projectiveOrbitι m hm) (CategoryTheory.CategoryStruct.comp (projectivePointTranslation g).inv h)

Inverse orbit translation restricts the inverse ambient projective translation.

theorem TauCeti.Comodule.toProjectiveOrbit_projectiveOrbitTranslation_hom {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) (projectiveOrbitTranslation m hm g).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑(HopfAlgebra.leftTranslationAlgEquiv g)).toRingHom)) (toProjectiveOrbit m hm)

The orbit factorization intertwines group translation with orbit translation.

theorem TauCeti.Comodule.toProjectiveOrbit_projectiveOrbitTranslation_hom_assoc {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) {Z : AlgebraicGeometry.Scheme} (h : projectiveOrbitScheme m hm ⟶ Z) : CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) (CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑(HopfAlgebra.leftTranslationAlgEquiv g)).toRingHom)) (CategoryTheory.CategoryStruct.comp (toProjectiveOrbit m hm) h)

The orbit factorization intertwines group translation with orbit translation.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_one {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : projectiveOrbitTranslation m hm 1 = CategoryTheory.Iso.refl (projectiveOrbitScheme m hm)

Translation by the identity is the identity orbit isomorphism.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_mul {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g h : WithConv (H →ₐ[k] k)) : projectiveOrbitTranslation m hm (g * h) = projectiveOrbitTranslation m hm h ≪≫ projectiveOrbitTranslation m hm g

Translation by a convolution product composes orbit translations in action order.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_inv_eq_symm {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : projectiveOrbitTranslation m hm g⁻¹ = (projectiveOrbitTranslation m hm g).symm

Translation by the inverse point is the inverse orbit isomorphism.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_hom_toSpec {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).hom (projectiveOrbitToSpec m hm) = projectiveOrbitToSpec m hm

Orbit translations are automorphisms over the base field.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_hom_toSpec_assoc {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).hom (CategoryTheory.CategoryStruct.comp (projectiveOrbitToSpec m hm) h) = CategoryTheory.CategoryStruct.comp (projectiveOrbitToSpec m hm) h

Orbit translations are automorphisms over the base field.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_inv_toSpec {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).inv (projectiveOrbitToSpec m hm) = projectiveOrbitToSpec m hm

Inverse orbit translations also preserve the structural morphism to the base field.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_inv_toSpec_assoc {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (projectiveOrbitTranslation m hm g).inv (CategoryTheory.CategoryStruct.comp (projectiveOrbitToSpec m hm) h) = CategoryTheory.CategoryStruct.comp (projectiveOrbitToSpec m hm) h

Inverse orbit translations also preserve the structural morphism to the base field.