Pullback of global homogeneous coordinates

The morphism to Proj defined by global homogeneous coordinates commutes with pullback along an arbitrary scheme morphism. This is equality of scheme morphisms, including their structure-sheaf maps. In particular it applies to families over nonreduced rings, where equality on field-valued points would not suffice.

AlgebraicGeometry.Proj.fromOfGlobalSections_naturality turns identities of pulled-back coordinate maps into identities of morphisms. Combined with invariance under unit rescaling, it supplies the passage from semi-invariant coordinates to invariant projective morphisms used in constructing homogeneous spaces.

The chart calculation uses TauCeti.ProjectiveSpectrum.toBasicOpenOfGlobalSections_eq and Mathlib's naturality of the canonical maps from open subschemes to spectra of sections.

References

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

theorem AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections_naturality {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X Y : Scheme} (f : A →+* ↑(Y.presheaf.obj (Opposite.op ⊤))) (g : X ⟶ Y) {t : A} {d : ℕ} (hd : 0 < d) (ht : t ∈ 𝒜 d) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.resLE g (Y.basicOpen (f t)) (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop g)) (f t))) ⋯) (toBasicOpenOfGlobalSections 𝒜 f ⋯ hd ht) = toBasicOpenOfGlobalSections 𝒜 ((CommRingCat.Hom.hom (Scheme.Hom.appTop g)).comp f) ⋯ hd ht

On a standard open, pulling back homogeneous coordinates pulls back the projective chart morphism. The source open is the basic open of the pulled-back coordinate.

theorem AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections_naturality_assoc {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X Y : Scheme} (f : A →+* ↑(Y.presheaf.obj (Opposite.op ⊤))) (g : X ⟶ Y) {t : A} {d : ℕ} (hd : 0 < d) (ht : t ∈ 𝒜 d) {Z : Scheme} (h : ↑(basicOpen 𝒜 t) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.resLE g (Y.basicOpen (f t)) (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop g)) (f t))) ⋯) (CategoryTheory.CategoryStruct.comp (toBasicOpenOfGlobalSections 𝒜 f ⋯ hd ht) h) = CategoryTheory.CategoryStruct.comp (toBasicOpenOfGlobalSections 𝒜 ((CommRingCat.Hom.hom (Scheme.Hom.appTop g)).comp f) ⋯ hd ht) h

On a standard open, pulling back homogeneous coordinates pulls back the projective chart morphism. The source open is the basic open of the pulled-back coordinate.

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_naturality {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X Y : Scheme} (f : A →+* ↑(Y.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp g (fromOfGlobalSections 𝒜 f hf) = fromOfGlobalSections 𝒜 ((CommRingCat.Hom.hom (Scheme.Hom.appTop g)).comp f) ⋯

Pulling back global homogeneous coordinates along a scheme morphism gives the composite with the original projective morphism.

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_naturality_assoc {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X Y : Scheme} (f : A →+* ↑(Y.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) (g : X ⟶ Y) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (fromOfGlobalSections 𝒜 f hf) h) = CategoryTheory.CategoryStruct.comp (fromOfGlobalSections 𝒜 ((CommRingCat.Hom.hom (Scheme.Hom.appTop g)).comp f) ⋯) h

Pulling back global homogeneous coordinates along a scheme morphism gives the composite with the original projective morphism.