Equality of projective morphisms on a degree-one chart

On a standard chart whose denominator has degree one, two systems of homogeneous coordinates define the same scheme morphism exactly when their degree-n coordinates are related by the nth power of one unit. This detects equality on nonreduced value rings as well as on fields, and supplies the chart criterion for fibers of projective orbit morphisms.

The chart morphisms use HomogeneousLocalization.Away.lift and Proj.awayι.

References

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

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_eq_toSpecΓ_awayLift {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {t : A} {d : ℕ} (hd : 0 < d) (ht : t ∈ 𝒜 d) (hu : IsUnit (f t)) : fromOfGlobalSections 𝒜 f hf = CategoryTheory.CategoryStruct.comp X.toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 f hu))) (awayι 𝒜 t ht hd))

If one homogeneous coordinate is a unit, the projective morphism factors through its standard affine chart via the degree-zero coordinate map.

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_Spec_eq_awayLift {A B σ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (f : A →+* B) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {t : A} {d : ℕ} (hd : 0 < d) (ht : t ∈ 𝒜 d) (hu : IsUnit (f t)) : fromOfGlobalSections 𝒜 ((CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧B).inv).comp f) ⋯ = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 f hu))) (awayι 𝒜 t ht hd)

Homogeneous coordinates in a ring with an invertible chart denominator give the corresponding projective morphism from its spectrum.

theorem AlgebraicGeometry.Proj.SpecMap_awayLift_awayι_eq_iff {A B σ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (f g : A →+* B) {t : A} (ht : t ∈ 𝒜 1) (hf : IsUnit (f t)) (hg : IsUnit (g t)) : CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 f hf))) (awayι 𝒜 t ht ⋯) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 g hg))) (awayι 𝒜 t ht ⋯) ↔ ∃ (c : Bˣ), ∀ (n : ℕ), ∀ a ∈ 𝒜 n, g a = ↑c ^ n * f a

Two morphisms read on the same degree-one projective chart agree exactly when all homogeneous coordinates differ by powers of a common unit in the value ring.