Unit rescaling of global projective coordinates

Multiplying the degree-n homogeneous coordinates by the nth power of a global unit does not change the morphism to Proj. This is equality of scheme morphisms, including their structure-sheaf maps, not merely equality on field-valued points. It permits semi-invariant homogeneous coordinates to define invariant projective morphisms.

For Mathlib's Proj.fromOfGlobalSections, the coordinates must send the irrelevant ideal to the unit ideal.

References

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

theorem TauCeti.ProjectiveSpectrum.toBasicOpenOfGlobalSections_eq {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) {t : A} {d : ℕ} (hd : 0 < d) (ht : t ∈ 𝒜 d) : AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f ⋯ hd ht = CategoryTheory.CategoryStruct.comp (X.basicOpen (f t)).toSpecΓ (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 ((CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)).comp f) ⋯))) (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 t ht hd).inv)

On a standard open, global homogeneous coordinates give the degree-zero localization map of their restrictions to that open.

theorem TauCeti.ProjectiveSpectrum.toBasicOpenOfGlobalSections_eq_of_unit_rescaling {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f g : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (c : (↑(X.presheaf.obj (Opposite.op ⊤)))ˣ) (h : ∀ (n : ℕ), ∀ a ∈ 𝒜 n, g a = ↑c ^ n * f a) {t : A} {d : ℕ} (hd : 0 < d) (ht : t ∈ 𝒜 d) : ∃ (e : X.basicOpen (f t) = X.basicOpen (g t)), CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 g ⋯ hd ht) = AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f ⋯ hd ht

Unit rescaling of homogeneous coordinates preserves each projective chart map.

theorem TauCeti.ProjectiveSpectrum.fromOfGlobalSections_eq_of_unit_rescaling {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f g : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (c : (↑(X.presheaf.obj (Opposite.op ⊤)))ˣ) (h : ∀ (n : ℕ), ∀ a ∈ 𝒜 n, g a = ↑c ^ n * f a) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) : AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 g ⋯ = AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf

Multiplying the degree-n coordinates by the nth power of a global unit does not change the resulting morphism to Proj.