Projective orbit morphisms of Hopf comodules

For a unimodular vector m in a finite projective comodule M over a commutative Hopf algebra H, construct the scheme morphism

Spec H ⟶ Proj(Sym(M∨))

with homogeneous coordinates φ ↦ c(φ, m). On points this sends g to the line through g · m, using the original action on M, rather than its contragredient. The dual module appears because its elements are the linear homogeneous coordinates of projective space. Over a field, every nonzero vector is unimodular. Over a general ring, unimodularity ensures that the vector generates a direct summand of rank one.

The matrix coefficients generate the unit ideal by Comodule.span_matrixCoefficient_eq_top_iff_isUnimodular. The construction then uses Mathlib's Proj.fromOfGlobalSections, including its chart and base-morphism formulas. No smoothness, reducedness, or finite-type hypothesis on H is imposed.

References

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

noncomputable def TauCeti.Comodule.orbitCoordinates {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) : SymmetricAlgebra R (Module.Dual R M) →ₐ[R] H

The homogeneous coordinate map of the orbit of a vector: the linear coordinate φ pulls back to the matrix coefficient c(φ, m).

Equations

• TauCeti.Comodule.orbitCoordinates m = SymmetricAlgebra.lift (TauCeti.Comodule.matrixCoefficientBilinear.flip m)

@[simp]

theorem TauCeti.Comodule.orbitCoordinates_ι {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) (φ : Module.Dual R M) : (orbitCoordinates m) ((SymmetricAlgebra.ι R (Module.Dual R M)) φ) = matrixCoefficient φ m

Linear homogeneous coordinates pull back to their matrix coefficients.

theorem TauCeti.Comodule.orbitCoordinates_smul_of_mem_homogeneousSubmodule {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) (c : R) {n : ℕ} {s : SymmetricAlgebra R (Module.Dual R M)} (hs : s ∈ SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M) n) : (orbitCoordinates (c • m)) s = c ^ n • (orbitCoordinates m) s

Scaling a vector by c scales its degree-n orbit coordinates by c ^ n.

@[simp]

theorem TauCeti.Comodule.counitAlgHom_comp_orbitCoordinates {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) : (Bialgebra.counitAlgHom R H).comp (orbitCoordinates m) = SymmetricAlgebra.lift ((Module.Dual.eval R M) m)

At the identity point, orbit coordinates specialize to evaluation at the original vector.

theorem TauCeti.Comodule.map_irrelevant_orbitCoordinates {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] {m : M} (hm : Module.IsUnimodular R m) : Ideal.map (orbitCoordinates m).toRingHom (HomogeneousIdeal.irrelevant (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M))).toIdeal = ⊤

The images of the irrelevant ideal under orbit coordinates of a unimodular vector generate the unit ideal. This defines a morphism on the whole group scheme.

noncomputable def TauCeti.Comodule.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] (m : M) (hm : Module.IsUnimodular R m) : AlgebraicGeometry.Spec ↧H ⟶ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M))

The projective orbit morphism of a unimodular vector in a finite projective Hopf comodule. Its homogeneous coordinate functions are the vector's matrix coefficients.

Equations

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

theorem TauCeti.Comodule.projectiveOrbitMap_def {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] (m : M) (hm : Module.IsUnimodular R m) : projectiveOrbitMap m hm = AlgebraicGeometry.Proj.fromOfGlobalSections (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧H).inv).comp (orbitCoordinates m).toRingHom) ⋯

The orbit morphism is the morphism defined by its global homogeneous coordinate map.

theorem TauCeti.Comodule.projectiveOrbitMap_preimage_basicOpen {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] (m : M) (hm : Module.IsUnimodular R m) {s : SymmetricAlgebra R (Module.Dual R M)} {n : ℕ} (hn : 0 < n) (hs : s ∈ SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M) n) : (TopologicalSpace.Opens.map (projectiveOrbitMap m hm).base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) s) = (AlgebraicGeometry.Spec ↧H).basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧H).inv) ((orbitCoordinates m) s))

The inverse image of a standard projective open is the principal open of its pulled-back homogeneous coordinate function.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitMap_preimage_basicOpen_ι {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] (m : M) (hm : Module.IsUnimodular R m) (φ : Module.Dual R M) : (TopologicalSpace.Opens.map (projectiveOrbitMap m hm).base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((SymmetricAlgebra.ι R (Module.Dual R M)) φ)) = (AlgebraicGeometry.Spec ↧H).basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧H).inv) (matrixCoefficient φ m))

The standard open of a linear coordinate pulls back to the principal open of the corresponding matrix coefficient.

theorem TauCeti.Comodule.projectiveOrbitMap_resLE {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] (m : M) (hm : Module.IsUnimodular R m) {s : SymmetricAlgebra R (Module.Dual R M)} {n : ℕ} (hn : 0 < n) (hs : s ∈ SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M) n) : AlgebraicGeometry.Scheme.Hom.resLE (projectiveOrbitMap m hm) (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) s) ((AlgebraicGeometry.Spec ↧H).basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧H).inv) ((orbitCoordinates m) s))) ⋯ = AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M)) ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧H).inv).comp (orbitCoordinates m).toRingHom) ⋯ hn hs

On every standard chart, the orbit morphism is obtained by localizing its matrix coefficient coordinate map.

theorem TauCeti.Comodule.projectiveOrbitMap_toSpecZero {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] (m : M) (hm : Module.IsUnimodular R m) : CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) (AlgebraicGeometry.Proj.toSpecZero (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((orbitCoordinates m).comp (algebraMap (↥(SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M) 0)) (SymmetricAlgebra R (Module.Dual R M)))))

The projective orbit morphism lies over the coordinate map on degree-zero elements.

theorem TauCeti.Comodule.projectiveOrbitMap_toSpecZero_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] (m : M) (hm : Module.IsUnimodular R m) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧↥(SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M) 0) ⟶ Z) : CategoryTheory.CategoryStruct.comp (projectiveOrbitMap m hm) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((orbitCoordinates m).comp (algebraMap (↥(SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R M) 0)) (SymmetricAlgebra R (Module.Dual R M)))))) h

The projective orbit morphism lies over the coordinate map on degree-zero elements.