Properness of the projective spectrum over its coefficient ring

Let A be an ℕ-graded R-algebra with grading 𝒜. Mathlib proves that the projective spectrum Proj 𝒜 is separated over the spectrum of the degree-zero part 𝒜 0, and proper over it when A is of finite type over 𝒜 0 (AlgebraicGeometry.Proj.toSpecZero). This file transfers these properties to the coefficient morphism Proj 𝒜 ⟶ Spec R (AlgebraicGeometry.Proj.toSpecCoeff), which factors through Spec (𝒜 0) ⟶ Spec R:

• it is always separated;
• it is quasi-compact when A is of finite type over 𝒜 0, and of finite type when A is of finite type over R;
• it is universally closed when moreover 𝒜 0 is integral over R, and proper when A is of finite type over R and 𝒜 0 is integral over R, for instance a finite R-module.

The hypothesis on the degree-zero part cannot be dropped: for R[t][x] with t in degree zero and x in degree one, the projective spectrum is Spec R[t], which is not universally closed over Spec R when R is nonzero.

These statements are the affine-local input for properness of the relative Proj of a graded quasi-coherent algebra over a scheme.

Main results

• AlgebraicGeometry.Proj.isSeparated_toSpecCoeff
• AlgebraicGeometry.Proj.quasiCompact_toSpecCoeff
• AlgebraicGeometry.Proj.locallyOfFiniteType_toSpecCoeff
• AlgebraicGeometry.Proj.universallyClosed_toSpecCoeff
• AlgebraicGeometry.Proj.isProper_toSpecCoeff

References

• Stacks Project, Tag 01MC, separatedness of Proj over the degree-zero part.
• Stacks Project, Tag 01MF, universal closedness of Proj over the degree-zero part for a graded ring of finite type over it.

instance AlgebraicGeometry.Proj.isSeparated_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : IsSeparated (toSpecCoeff 𝒜)

The projective spectrum of a graded algebra is separated over its coefficient ring.

instance AlgebraicGeometry.Proj.quasiCompact_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : QuasiCompact (toSpecCoeff 𝒜)

The projective spectrum of a graded algebra of finite type over its degree-zero part is quasi-compact over the coefficient ring.

instance AlgebraicGeometry.Proj.locallyOfFiniteType_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType R A] : LocallyOfFiniteType (toSpecCoeff 𝒜)

The projective spectrum of a graded algebra of finite type over R is locally of finite type over Spec R.

instance AlgebraicGeometry.Proj.universallyClosed_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] [Algebra.IsIntegral R ↥(𝒜 0)] : UniversallyClosed (toSpecCoeff 𝒜)

The projective spectrum of a graded algebra of finite type over its degree-zero part is universally closed over the coefficient ring when the degree-zero part is integral over it.

instance AlgebraicGeometry.Proj.isProper_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType R A] [Algebra.IsIntegral R ↥(𝒜 0)] : IsProper (toSpecCoeff 𝒜)

The projective spectrum is proper over the coefficient ring. If the graded algebra is of finite type over R and its degree-zero part is integral over R, for instance a finite R-module, then Proj 𝒜 ⟶ Spec R is proper.