The global function attached to a degree-zero element

Proj.toSpecZero makes Proj 𝒜 a scheme over Spec (𝒜 0), so every degree-zero element of the graded ring becomes a global function. This file computes that function: it is the constant. At every point its value is a / 1 in the homogeneous localization there, which is HomogeneousLocalization.fromZeroRingHom.

Why it is not immediate

toSpecZero is not defined pointwise. It is built from basicOpenToSpec 𝒜 1 through three transports — Scheme.topIso, Scheme.isoOfEq along basicOpen 𝒜 1 = ⊤, and Scheme.Opens.topIso — none of which is the identity on the nose, and the whole thing is stated against Spec (𝒜 0) rather than against sections. So the computation has three steps:

• toSpecZero_appTop_eq peels the Spec side. ΓSpecIso_inv_naturality cancels the spectrum against the ring map and basicOpenToSpec_app_top exposes awayToSection, which is pointwise by construction;
• toSpecZero_transport_eq collapses the three transports into a single presheaf restriction. The three composed scheme morphisms are the identity of Proj 𝒜 — the same observation Mathlib's own awayι_toSpecZero proof makes — and cancelling the resulting restriction against its inverse leaves the eqToHom for basicOpen 𝒜 1 = ⊤;
• openToLocalization_toSpecZero_appTop then evaluates, and by that point everything is definitional: openToLocalization is literally s.1 ⟨x, hx⟩, presheaf restriction is restriction of the function, and awayToSection was pointwise all along.

What it is for

The base-field action on cohomology (varietyScalarAction) is multiplication by the global function attached to a scalar, and it acts on the sections of an associated sheaf pointwise on fibers. So identifying that action with scalar multiplication on the graded localizations comes down to exactly this lemma. It is the bridge #666 needs between the k-action the Čech lane can compute with and the one module_finite_linearCoherentH_of_cech consumes.

Fintype ι and the polynomial grading play no part: this is a statement about an arbitrary ℕ-graded ring.

theorem AlgebraicGeometry.Proj.toSpecZero_appTop_eq {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (CommRingCat.of ↥(𝒜 0))).inv (Scheme.Hom.appTop (toSpecZero 𝒜)) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers 1))) (CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 1) (CategoryTheory.CategoryStruct.comp (basicOpen 𝒜 1).topIso.inv (CategoryTheory.CategoryStruct.comp (Scheme.Hom.appTop ((Proj 𝒜).isoOfEq ⋯).inv) (Scheme.Hom.appTop (Proj 𝒜).topIso.inv))))

The Spec side, peeled. The ring map 𝒜 0 → Γ(Proj 𝒜, ⊤) induced by the structure morphism is fromZeroRingHom followed by awayToSection at f = 1, transported back to ⊤. awayToSection is pointwise by construction, which is the whole point of getting here.

theorem AlgebraicGeometry.Proj.toSpecZero_transport_eq {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : CategoryTheory.CategoryStruct.comp (basicOpen 𝒜 1).topIso.inv (CategoryTheory.CategoryStruct.comp (Scheme.Hom.appTop ((Proj 𝒜).isoOfEq ⋯).inv) (Scheme.Hom.appTop (Proj 𝒜).topIso.inv)) = (Proj 𝒜).presheaf.map (CategoryTheory.eqToHom ⋯).op

The three transports collapse to one restriction. Scheme.topIso, the isoOfEq along basicOpen 𝒜 1 = ⊤ and Scheme.Opens.topIso compose to the identity of Proj 𝒜, so on sections they compose to the presheaf restriction that equality induces.

theorem AlgebraicGeometry.Proj.openToLocalization_presheaf_map {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (U V : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) (i : U ⟶ V) (x : ↑(ProjectiveSpectrum.top 𝒜)) (hx : x ∈ U) (s : ↑((Proj 𝒜).presheaf.obj (Opposite.op V))) : (CommRingCat.Hom.hom (openToLocalization 𝒜 U x hx)) ((CategoryTheory.ConcreteCategory.hom ((Proj 𝒜).presheaf.map i.op)) s) = (CommRingCat.Hom.hom (openToLocalization 𝒜 V x ⋯)) s

Evaluating a section at a point commutes with restriction: both are s.1 ⟨x, _⟩.

theorem AlgebraicGeometry.Proj.openToLocalization_toSpecZero_appTop {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (a : ↥(𝒜 0)) (x : ↑(ProjectiveSpectrum.top 𝒜)) : (CommRingCat.Hom.hom (openToLocalization 𝒜 ⊤ x trivial)) ((CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (CommRingCat.of ↥(𝒜 0))).inv (Scheme.Hom.appTop (toSpecZero 𝒜)))) a) = (HomogeneousLocalization.fromZeroRingHom 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl) a

A degree-zero element becomes the constant function. The global function the structure morphism attaches to a : 𝒜 0 has value a / 1 at every point.

This is what makes the base-field action on cohomology computable: varietyScalarAction is multiplication by such a function, and it acts on sections of an associated sheaf pointwise.