Graded rings of sections over basic opens

Let A = ⨁ₙ Aₙ be a graded algebra on a scheme X whose homogeneous components are quasicoherent, let U be an affine open of X and f ∈ Γ(X, U). Restriction of sections identifies the graded ring ⨁ n, Γ(Aₙ, X.basicOpen f) with the localization of the graded ring ⨁ n, Γ(Aₙ, U) away from f, placed in degree zero. In each degree this is the localization of the sections of a quasicoherent module (Scheme.Modules.isLocalizedModule_basicOpenRestrict), and localization of modules commutes with direct sums.

This is the compatibility of the affine graded charts of A with passage to basic opens: it is what identifies the spectrum, or the Proj, of the graded ring over X.basicOpen f with the corresponding open subscheme of the construction over U, as needed to glue affine-local constructions with graded algebras. It is the graded counterpart of CategoryTheory.CommMon.isLocalization_basicOpen for commutative 𝒪_X-algebras.

Main statements

• CategoryTheory.CommMon.isLocalization_gradedSections_basicOpen: the restriction ⨁ n, Γ(Aₙ, U) → ⨁ n, Γ(Aₙ, X.basicOpen f) is a localization away from f.
• CategoryTheory.CommMon.isBaseChange_restrictGradedSections: the same restriction exhibits ⨁ n, Γ(Aₙ, X.basicOpen f) as the base change of ⨁ n, Γ(Aₙ, U) along Γ(X, U) → Γ(X, X.basicOpen f), for the algebra structure CategoryTheory.CommMon.algebraGradedSectionsBasicOpen.
• CategoryTheory.CommMon.coequifibered_toGradedSectionsPresheaf: on the affine opens of X, the presheaf of graded rings of sections is coequifibered over the structure presheaf.

theorem CategoryTheory.CommMon.isLocalization_gradedSections_basicOpen {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : IsLocalization.Away ((algebraMap (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) f) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op (X.basicOpen f))))

For a graded algebra A with quasicoherent homogeneous components, an affine open U and f ∈ Γ(X, U), restriction exhibits the graded ring of sections ⨁ n, Γ(Aₙ, X.basicOpen f) as the localization of ⨁ n, Γ(Aₙ, U) away from the image of f in degree zero.

@[reducible, inline]

noncomputable abbrev CategoryTheory.CommMon.algebraGradedSectionsBasicOpen {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) : Algebra (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op (X.basicOpen f))))

The Γ(X, U)-algebra structure on ⨁ n, Γ(Aₙ, D(f)) whose underlying module structure is the one by restriction of scalars along Γ(X, U) → Γ(X, D(f)) (Scheme.Modules.moduleBasicOpen).

theorem CategoryTheory.CommMon.restrictGradedSections_algebraMap_basicOpen {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (f r : ↑(X.presheaf.obj (Opposite.op U))) : have this := A.algebraGradedSectionsBasicOpen f; (A.restrictGradedSectionsGradedHom (homOfLE ⋯)) ((algebraMap (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) r) = (algebraMap (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op (X.basicOpen f))))) r

Restriction of sections from U to D(f) is a homomorphism of Γ(X, U)-algebras.

theorem CategoryTheory.CommMon.isBaseChange_restrictGradedSections {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (hU : AlgebraicGeometry.IsAffineOpen U) : have this := A.algebraGradedSectionsBasicOpen f; IsBaseChange ↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) { toRingHom := ↑(A.restrictGradedSectionsGradedHom (homOfLE ⋯)), commutes' := ⋯ }.toLinearMap

Over an affine open U and f ∈ Γ(X, U), restriction of sections exhibits ⨁ n, Γ(Aₙ, D(f)) as the base change of ⨁ n, Γ(Aₙ, U) along Γ(X, U) → Γ(X, D(f)).

theorem CategoryTheory.CommMon.coequifibered_toGradedSectionsPresheaf {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] : NatTrans.Coequifibered ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.whiskerLeft A.toGradedSectionsPresheaf)

On the affine opens of X, the presheaf of graded rings of sections of a graded algebra with quasicoherent homogeneous components is coequifibered over the structure presheaf: its graded rings of sections over basic opens are localizations. This is the condition under which Mathlib glues the spectra of its sections (AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData).