@[reducible, inline]

noncomputable abbrev ProjectiveDefinitions.polynomialGrading (k : Type u) [CommRing k] (n a✝ : ℕ) : Submodule k (MvPolynomial (Fin (n + 1)) k)

The standard grading on the polynomial ring k[x_0, ..., x_n] by total degree, where polynomialGrading k n d is the k-submodule of homogeneous polynomials of degree d.

@[implicit_reducible]

noncomputable instance ProjectiveDefinitions.polynomialGradedAlgebra (k : Type u) [CommRing k] (n : ℕ) : GradedRing (polynomialGrading k n)

The polynomial ring k[x_0, ..., x_n] is a graded ring under the total-degree grading.

noncomputable def ProjectiveDefinitions.ProjectiveSpace (k : Type u) [CommRing k] (n : ℕ) : AlgebraicGeometry.Scheme

Projective n-space over a commutative ring k, defined as ℙ^n_k := Proj k[x_0, ..., x_n] with the standard grading.

noncomputable def ProjectiveDefinitions.ProjectiveSpace.structureMorphism (k : Type u) [CommRing k] (n : ℕ) : ProjectiveSpace k n ⟶ AlgebraicGeometry.Spec (CommRingCat.of ↥(polynomialGrading k n 0))

The structure morphism ℙ^n_k → Spec k of projective n-space, induced by the inclusion of the degree-zero piece into the graded polynomial ring.

theorem ProjectiveDefinitions.ProjectiveSpace.isSeparated (k : Type u) [CommRing k] (n : ℕ) : (ProjectiveSpace k n).IsSeparated

Projective n-space ℙ^n_k is a separated scheme.

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

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

def ProjectiveDefinitions.IsQuasiProjectiveVariety (k : Type u) [CommRing k] (X : AlgebraicGeometry.Scheme) : Prop

A scheme X is a quasi-projective variety over k if it is an open subscheme of a projective variety: there exists a closed immersion Y ↪ ℙ^n_k and an open immersion X ↪ Y.

theorem ProjectiveDefinitions.IsProjectiveVariety.isQuasiProjective {k : Type u} [CommRing k] {X : AlgebraicGeometry.Scheme} (h : IsProjectiveVariety k X) : IsQuasiProjectiveVariety k X

Every projective variety is quasi-projective: take the open immersion to be the identity.

theorem ProjectiveDefinitions.projectiveSpace_isProjective (k : Type u) [CommRing k] (n : ℕ) : IsProjectiveVariety k (ProjectiveSpace k n)

Projective space ℙ^n_k is itself a projective variety, via the identity closed immersion.

theorem ProjectiveDefinitions.projectiveSpace_isQuasiProjective (k : Type u) [CommRing k] (n : ℕ) : IsQuasiProjectiveVariety k (ProjectiveSpace k n)

Projective space ℙ^n_k is in particular quasi-projective.

theorem ProjectiveDefinitions.IsProjectiveVariety.of_closedImmersion {k : Type u} [CommRing k] {X Y : AlgebraicGeometry.Scheme} (hY : IsProjectiveVariety k Y) (ι : X ⟶ Y) [hι : AlgebraicGeometry.IsClosedImmersion ι] : IsProjectiveVariety k X

A closed subscheme of a projective variety is again a projective variety: compose the closed immersion X ↪ Y with a closed immersion Y ↪ ℙ^n_k.

theorem ProjectiveDefinitions.IsQuasiProjectiveVariety.of_openImmersion {k : Type u} [CommRing k] {X Y : AlgebraicGeometry.Scheme} (hY : IsQuasiProjectiveVariety k Y) (j : X ⟶ Y) [hj : AlgebraicGeometry.IsOpenImmersion j] : IsQuasiProjectiveVariety k X

An open subscheme of a quasi-projective variety is again quasi-projective: compose the open immersion X ↪ Y with the existing open immersion of Y into a projective variety.