Graded changes of global projective coordinates #
Postcomposing a morphism defined by global homogeneous coordinates with a graded projective map amounts to precomposing its coordinate homomorphism. The comparison holds as an equality of scheme morphisms, including the maps on structure sheaves. It allows coordinate identities for linear actions to give equivariance of projective orbit morphisms.
References #
- J. S. Milne, Algebraic Groups (2017), §§7.d–7.f.
theorem
AlgebraicGeometry.Proj.fromOfGlobalSections_map
{A B σ τ : Type u}
[CommRing A]
[CommRing B]
[SetLike σ A]
[AddSubgroupClass σ A]
[SetLike τ B]
[AddSubgroupClass τ B]
{𝒜 : ℕ → σ}
{ℬ : ℕ → τ}
[GradedRing 𝒜]
[GradedRing ℬ]
{X : Scheme}
(F : 𝒜 →+*ᵍ ℬ)
(hF : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map F (HomogeneousIdeal.irrelevant 𝒜))
(f : B →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
(hf : Ideal.map f (HomogeneousIdeal.irrelevant ℬ).toIdeal = ⊤)
:
CategoryTheory.CategoryStruct.comp (fromOfGlobalSections ℬ f hf) (map F hF) = fromOfGlobalSections 𝒜 (f.comp ↑F) ⋯
A graded projective map transforms a global homogeneous-coordinate morphism by precomposition of its coordinates.
theorem
AlgebraicGeometry.Proj.fromOfGlobalSections_map_assoc
{A B σ τ : Type u}
[CommRing A]
[CommRing B]
[SetLike σ A]
[AddSubgroupClass σ A]
[SetLike τ B]
[AddSubgroupClass τ B]
{𝒜 : ℕ → σ}
{ℬ : ℕ → τ}
[GradedRing 𝒜]
[GradedRing ℬ]
{X : Scheme}
(F : 𝒜 →+*ᵍ ℬ)
(hF : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map F (HomogeneousIdeal.irrelevant 𝒜))
(f : B →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
(hf : Ideal.map f (HomogeneousIdeal.irrelevant ℬ).toIdeal = ⊤)
{Z : Scheme}
(h : Proj 𝒜 ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (fromOfGlobalSections ℬ f hf) (CategoryTheory.CategoryStruct.comp (map F hF) h) = CategoryTheory.CategoryStruct.comp (fromOfGlobalSections 𝒜 (f.comp ↑F) ⋯) h
A graded projective map transforms a global homogeneous-coordinate morphism by precomposition of its coordinates.