noncomputable def ProjectiveScheme (k : Type u_1) [CommRing k] (n : ℕ) : AlgebraicGeometry.Scheme

Projective n-space P^n_k as the Proj of the standard graded polynomial ring in n + 1 variables over k.

def AlgebraicGeometry.Scheme.IsProjectiveVariety (k : Type u_1) [CommRing k] (X : Scheme) : Prop

A scheme X is a projective variety over k if it admits a closed immersion into some projective space P^n_k.