Projective schemes over a ring

A scheme X over Spec R is projective over R if it is a closed subscheme, over R, of the projective spectrum Proj (Sym_R M) of the symmetric algebra of a finite R-module M. Mathlib has no class of projective morphisms, so this file records projectivity over an affine base as a predicate on schemes over Spec R.

Over an affine base this is the usual notion: a finite R-module M is a quotient of some Rⁿ, so Proj (Sym_R M) is itself a closed subscheme of Proj (Sym_R Rⁿ) = ℙⁿ⁻¹_R, and the definition agrees with Hartshorne's (a closed subscheme of some ℙⁿ_R). Over a field k every finite module is a finite-dimensional vector space, so Proj (Sym_k M) is a projective space over k.

A projective scheme over R is proper over R, because closed immersions are proper and Proj (Sym_R M) is proper over R for finite M (TauCeti.SymmetricAlgebra.instIsProperProjToSpec).

Main definitions

• AlgebraicGeometry.Scheme.IsProjectiveOver R X: the scheme X over Spec R is a closed subscheme, over R, of Proj (Sym_R M) for some finite R-module M.

Main results

• AlgebraicGeometry.Scheme.IsProjectiveOver.of_isClosedImmersion: a closed subscheme over R of a projective scheme over R is projective over R.
• the instance (Proj (Sym_R M)).IsProjectiveOver R for a finite R-module M.
• the instance IsProper (X ↘ Spec R) for X projective over R.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section II.4 (definition of a projective morphism before Theorem II.4.9).

class AlgebraicGeometry.Scheme.IsProjectiveOver (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] : Prop

A scheme X over Spec R is projective over R if it is a closed subscheme, over R, of the projective spectrum Proj (Sym_R M) of the symmetric algebra of a finite R-module M.

• exists_isClosedImmersion : ∃ (M : Type u) (x : AddCommMonoid M) (x_1 : Module R M) (_ : Module.Finite R M) (f : X ⟶ Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)), IsClosedImmersion f ∧ Hom.IsOver f (Spec ↧R)

  There is a closed immersion over R into Proj (Sym_R M) for a finite R-module M.

instance AlgebraicGeometry.Scheme.isProjectiveOver_proj (R : Type u) [CommRing R] (M : Type u) [AddCommMonoid M] [Module R M] [Module.Finite R M] : IsProjectiveOver R

The projective spectrum of the symmetric algebra of a finite R-module is projective over R.

theorem AlgebraicGeometry.Scheme.IsProjectiveOver.of_isClosedImmersion (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] {Y : Scheme} [Y.Over (Spec ↧R)] [IsProjectiveOver R] (f : X ⟶ Y) [IsClosedImmersion f] [Hom.IsOver f (Spec ↧R)] : IsProjectiveOver R

A closed subscheme over R of a projective scheme over R is projective over R.

instance AlgebraicGeometry.Scheme.IsProjectiveOver.isProper (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] [IsProjectiveOver R] : IsProper (X ↘ Spec ↧R)

A projective scheme is proper: a scheme projective over R is proper over R.