Properness of the relative Proj

Let A = ⨁ₙ Aₙ be a graded algebra on a scheme X with quasi-coherent homogeneous components, and let Proj_X(A) ⟶ X be its relative Proj (CategoryTheory.CommMon.relativeProjToBase). Over an affine open U of X this morphism is the coefficient morphism Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U), so every property of morphisms that is local on the target can be checked on these charts (CategoryTheory.CommMon.relativeProjToBase_iff_forall_isAffineOpen). Combined with the corresponding properties of the projective spectrum of a graded ring, in TauCeti.AlgebraicGeometry.ProjectiveSpectrum.Proper, this gives:

• the relative Proj is always separated over X;
• it is quasi-compact over X when ⨁ n, Γ(Aₙ, U) is a finitely generated Γ(A₀, U)-algebra for every affine open U;
• it is locally of finite type over X when A is of finite type, that is, when ⨁ n, Γ(Aₙ, U) is a finitely generated Γ(X, U)-algebra for every affine open U;
• it is proper over X when moreover A₀ is finite, that is, when Γ(A₀, U) is a finite Γ(X, U)-module for every affine open U. This covers the case A₀ = 𝒪_X of blowups and of Proj of section algebras of invertible sheaves.

Main results

• CategoryTheory.CommMon.relativeProjToBase_iff_forall_isAffineOpen: a property of morphisms that is local on the target holds for Proj_X(A) ⟶ X exactly when it holds for every chart Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U).
• CategoryTheory.CommMon.isSeparated_relativeProjToBase: the relative Proj is separated.
• CategoryTheory.CommMon.quasiCompact_relativeProjToBase: the relative Proj of an algebra of finite type over its degree-zero part is quasi-compact.
• CategoryTheory.CommMon.locallyOfFiniteType_relativeProjToBase: the relative Proj of an algebra of finite type is locally of finite type.
• CategoryTheory.CommMon.isProper_relativeProjToBase: the relative Proj of an algebra of finite type with finite degree-zero part is proper.

References

• Stacks Project, Tag 01NS, Relative Proj
• R. Hartshorne, Algebraic Geometry, Proposition II.7.10, for the case of an algebra with A₀ = 𝒪_X generated by a coherent A₁ over a Noetherian scheme.

theorem CategoryTheory.CommMon.relativeProjToBase_iff_forall_isAffineOpen {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (P : MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P] : P A.relativeProjToBase ↔ ∀ (U : X.Opens), AlgebraicGeometry.IsAffineOpen U → P (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading U))

A property of morphisms that is local on the target holds for the structure morphism of the relative Proj exactly when it holds for the coefficient morphism Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U) over every affine open U of X.

instance CategoryTheory.CommMon.isSeparated_relativeProjToBase {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] : AlgebraicGeometry.IsSeparated A.relativeProjToBase

The relative Proj is separated over the base.

theorem CategoryTheory.CommMon.quasiCompact_relativeProjToBase {X : AlgebraicGeometry.Scheme} {A : CommMon (GradedObject ℕ X.Modules)} [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (h : ∀ (U : X.Opens), AlgebraicGeometry.IsAffineOpen U → Algebra.FiniteType (↥(A.gradedSectionsGrading U 0)) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) : AlgebraicGeometry.QuasiCompact A.relativeProjToBase

The relative Proj of a graded algebra of finite type over its degree-zero part is quasi-compact over the base.

theorem CategoryTheory.CommMon.locallyOfFiniteType_relativeProjToBase {X : AlgebraicGeometry.Scheme} {A : CommMon (GradedObject ℕ X.Modules)} [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (h : ∀ (U : X.Opens), AlgebraicGeometry.IsAffineOpen U → Algebra.FiniteType (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) : AlgebraicGeometry.LocallyOfFiniteType A.relativeProjToBase

The relative Proj of a graded algebra of finite type is locally of finite type over the base.

theorem CategoryTheory.CommMon.isProper_relativeProjToBase {X : AlgebraicGeometry.Scheme} {A : CommMon (GradedObject ℕ X.Modules)} [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (h : ∀ (U : X.Opens), AlgebraicGeometry.IsAffineOpen U → Algebra.FiniteType (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) (h₀ : ∀ (U : X.Opens), AlgebraicGeometry.IsAffineOpen U → Module.Finite ↑(X.presheaf.obj (Opposite.op U)) ↑((A.X 0).presheaf.obj (Opposite.op U))) : AlgebraicGeometry.IsProper A.relativeProjToBase

The relative Proj is proper. If the graded algebra A is of finite type and its degree-zero part A₀ is finite over X, then Proj_X(A) ⟶ X is proper.