Polynomial projective space as a variety over the base field

IsVariety k X asks for an integral scheme with a finite-type morphism to Spec k. For Pⁿ = Proj k[Xᵢ] the integrality is AlgebraicGeometry.Proj.isIntegral, and this file supplies the rest, as instances on Proj (polynomialGrading ι k) itself rather than on a bundle:

• the degree-zero part of the standard grading is the constants, so the base field maps isomorphically onto 𝒜 0 and Proj.toSpecZero becomes a morphism to Spec k;
• k[Xᵢ] is of finite type over 𝒜 0 when the variables are finite in number, which is what Mathlib's LocallyOfFiniteType (Proj.toSpecZero 𝒜) consumes.

Finiteness of the variable set is genuinely required here and not elsewhere in the Čech lane: acyclicity of the variable cover holds for any index type, but Pⁿ is of finite type over k only for finitely many variables.

theorem AlgebraicGeometry.Proj.algebraMap_polynomialGradeZero_surjective (ι k : Type u) [Field k] : Function.Surjective ⇑(algebraMap k ↥(MvPolynomial.polynomialGrading ι k 0))

The degree-zero part of the standard grading consists of the constants, so the base field maps onto it.

instance AlgebraicGeometry.Proj.finiteType_polynomialGradeZero (ι k : Type u) [Field k] : Algebra.FiniteType k ↥(MvPolynomial.polynomialGrading ι k 0)

The degree-zero part of the standard grading is of finite type over the base field, being a quotient of it.

instance AlgebraicGeometry.Proj.isScalarTower_polynomialGradeZero (ι k : Type u) [Field k] : IsScalarTower k (↥(MvPolynomial.polynomialGrading ι k 0)) (MvPolynomial ι k)

The base field acts on the polynomial ring through the degree-zero part of its grading.

instance AlgebraicGeometry.Proj.finiteType_polynomialGrading (ι k : Type u) [Field k] [Finite ι] : Algebra.FiniteType (↥(MvPolynomial.polynomialGrading ι k 0)) (MvPolynomial ι k)

With finitely many variables the polynomial ring is of finite type over the degree-zero part of its grading.

noncomputable def AlgebraicGeometry.Proj.projectiveSpaceToSpec (ι k : Type u) [Field k] : Proj (MvPolynomial.polynomialGrading ι k) ⟶ Spec (CommRingCat.of k)

The structure morphism of polynomial projective space to the base field.

Proj.toSpecZero lands in the spectrum of the degree-zero part; composing with the spectrum of the base field's map onto that part gives the morphism Variety asks for.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Proj.locallyOfFiniteType_projectiveSpaceToSpec (ι k : Type u) [Field k] [Finite ι] : LocallyOfFiniteType (projectiveSpaceToSpec ι k)

instance AlgebraicGeometry.Proj.isProper_projectiveSpaceToSpec (ι k : Type u) [Field k] [Finite ι] : IsProper (projectiveSpaceToSpec ι k)

The structure morphism of polynomial projective space is proper.

Proj.toSpecZero is proper because the polynomial ring is of finite type over its degree-zero part, and the identification of k with that part is an isomorphism: surjective by algebraMap_polynomialGradeZero_surjective, injective because k is a field. This is what makes Pⁿ Noetherian and separated through Variety.isNoetherian_of_isProper and Variety.isSeparated_of_isProper, which the finite-cover cohomology bound consumes.

instance AlgebraicGeometry.Proj.nonempty_projectiveSpace (ι k : Type u) [Field k] [Nonempty ι] : Nonempty ↥(Proj (MvPolynomial.polynomialGrading ι k))

Polynomial projective space is nonempty once there is a variable.

Nonemptiness is a hypothesis of Proj.isIntegral rather than a consequence: Proj of a graded ring concentrated in degree zero is empty. A variable supplies the missing point.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Proj.instOverProjectiveSpace (ι k : Type u) [Field k] : (Proj (MvPolynomial.polynomialGrading ι k)).Over (Spec (CommRingCat.of k))

Polynomial projective space is a scheme over the base field, with structure morphism projectiveSpaceToSpec. This is the Scheme.Over instance every statement about Pⁿ over k consumes; Proj (polynomialGrading ι k) ↘ Spec (CommRingCat.of k) unfolds to it.

Equations

• AlgebraicGeometry.Proj.instOverProjectiveSpace ι k = { hom := AlgebraicGeometry.Proj.projectiveSpaceToSpec ι k }

instance AlgebraicGeometry.Proj.isVariety_projectiveSpace (ι k : Type u) [Field k] [Finite ι] [Nonempty ι] : IsVariety k (Proj (MvPolynomial.polynomialGrading ι k))

Polynomial projective space is a variety over the base field.

Finiteness of the variable set is what makes the structure morphism of finite type; nonemptiness is what makes the space irreducible rather than vacuously so.

theorem AlgebraicGeometry.Proj.polynomialIntShift_isCoherent (ι k : Type u) [Field k] (d : ℤ) : Scheme.Modules.IsCoherent (Proj (MvPolynomial.polynomialGrading ι k)) (associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d))

The twisting sheaf O(d) on polynomial projective space is coherent.

noncomputable def AlgebraicGeometry.Proj.projectiveSpaceTwist (ι k : Type u) [Field k] (d : ℤ) : Coh (Proj (MvPolynomial.polynomialGrading ι k))

O(d) as a coherent sheaf on polynomial projective space.

This is the object coherentScalarAction and linearCoherentH are stated about, so with it the finiteness interface can name Hⁱ(Pⁿ, O(d)) as a k-vector space. Coherence of O(d) needs no finiteness of the index type; that enters only through isVariety_projectiveSpace.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.projectiveSpaceTwist_obj (ι k : Type u) [Field k] (d : ℤ) : (Coh.ι (Proj (MvPolynomial.polynomialGrading ι k))).obj (projectiveSpaceTwist ι k d) = associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d)

The coherent-sheaf bundle changes nothing about the underlying module sheaf, so the Čech lane's results about the twist apply to it directly.