Projective varieties

This file separates the proposition that a scheme over k is projective from a chosen projective presentation. A ProjectivePresentation k X is a finite-coordinate closed immersion of the fixed X into projective space over the base field. Variety.IsProjective k X merely asserts that such a presentation exists.

Consequently, two embeddings are two presentations of the same scheme, not two bundled varieties, and there is no bundled projective-variety type: a projective variety is (X : Scheme) [X.Over (Spec k)] [IsVariety k X] [Variety.IsProjective k X].

Properness is derived here, not assumed

Properness is derived from any presentation: Proj.toSpecZero is proper once the graded ring is of finite type over its degree-zero part, a closed immersion is finite and hence proper, and properness is stable under composition. The resulting instance depends only on the proposition-valued Variety.IsProjective, not on a globally selected embedding.

The degree-zero identification is a construction, not a coincidence

Proj.toSpecZero 𝒜 lands in Spec (𝒜 0), and for the standard grading 𝒜 0 is the submodule of degree-zero homogeneous polynomials — not k on the nose. homogeneousZeroRingEquiv is the identification, built from MvPolynomial.C and inverted by constantCoeff, and every statement below that mentions the base field passes through it explicitly rather than through a defeq that happens to fire.

Naming

The grading used here is MvPolynomial.homogeneousSubmodule ι k, which is by definition MvPolynomial.polynomialGrading ι k from Algebra/MvPolynomial/Grading.lean. The Mathlib spelling is used so that the variety layer does not import the Proj Čech-comparison stack; the two are the same term, so statements in either spelling compose.

noncomputable def AlgebraicGeometry.homogeneousZeroRingEquiv (ι R : Type u) [CommRing R] : R ≃+* ↥(MvPolynomial.homogeneousSubmodule ι R 0)

The base ring is the degree-zero part of the standard graded polynomial ring.

Both directions are ring homomorphisms already: MvPolynomial.C on the way in, and MvPolynomial.constantCoeff on the way out. What needs proof is that they are mutually inverse on the degree-zero submodule — a degree-zero homogeneous polynomial is a constant, which is MvPolynomial.totalDegree_eq_zero_iff_eq_C read through MvPolynomial.totalDegree_zero_iff_isHomogeneous.

Equations

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

@[simp]

theorem AlgebraicGeometry.homogeneousZeroRingEquiv_apply_coe (ι R : Type u) [CommRing R] (r : R) : ↑((homogeneousZeroRingEquiv ι R) r) = MvPolynomial.C r

The identification is MvPolynomial.C underneath, which is what makes it usable as a rewrite in statements phrased on the polynomial ring rather than on the degree-zero submodule.

theorem AlgebraicGeometry.isScalarTower_homogeneousZero (ι R : Type u) [CommRing R] : IsScalarTower R (↥(MvPolynomial.homogeneousSubmodule ι R 0)) (MvPolynomial ι R)

The tower R → 𝒜₀ → R[ι]. Both algebra structures are Mathlib's — SetLike.GradeZero.instAlgebra on the way in, the subobject coercion on the way out — so the tower is rfl; it is only missing because Mathlib does not register it for grade-zero parts in general. Local: the finite-type transfer below is its only consumer.

instance AlgebraicGeometry.finiteType_homogeneousZero (ι R : Type u) [CommRing R] [Finite ι] : Algebra.FiniteType (↥(MvPolynomial.homogeneousSubmodule ι R 0)) (MvPolynomial ι R)

The polynomial ring is of finite type over its degree-zero part when the variable set is finite. This is what Proj.toSpecZero's properness instance asks for, and it is the only place the finiteness of the variable set is used.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.projectiveSpace (ι k : Type u) [Field k] : Scheme

Projective space over k on the variable set ι, as the Proj of the standard graded polynomial ring.

Equations

• AlgebraicGeometry.projectiveSpace ι k = AlgebraicGeometry.Proj (MvPolynomial.homogeneousSubmodule ι k)

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

The structure morphism of projective space to Spec k: Mathlib's Proj.toSpecZero, followed by the identification of k with the degree-zero part.

Equations

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

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

structure AlgebraicGeometry.ProjectivePresentation (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : Type (u + 1)

A projective presentation of X over k: a closed immersion into a projective space over k, compatible with the two structure morphisms.

The variable set is data rather than a natural number because the ambient projective space is Proj of a polynomial ring on an index type, which is how the Proj lane in this repository states everything else. Finite ι is what makes the ambient space proper, and it is an instance field so that the properness instance below fires without an explicit argument.

• index : Type u

  The homogeneous coordinates of the ambient projective space.

• finiteIndex : Finite self.index

  Finitely many of them.

• embedding : X ⟶ projectiveSpace self.index k

  The projective embedding.

• isClosedImmersion : IsClosedImmersion self.embedding

  It is a closed immersion: this is the projectivity, and it is data.

• overBase : CategoryTheory.CategoryStruct.comp self.embedding (projectiveSpaceToSpec self.index k) = X ↘ Spec (CommRingCat.of k)

  The embedding is a morphism over the base field.

instance AlgebraicGeometry.ProjectivePresentation.instFiniteIndex {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) : Finite P.index

instance AlgebraicGeometry.ProjectivePresentation.instIsClosedImmersionEmbedding {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) : IsClosedImmersion P.embedding

theorem AlgebraicGeometry.ProjectivePresentation.isProper_structureMorphism {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) : IsProper (X ↘ Spec (CommRingCat.of k))

A projective variety is proper over the base field.

Not a field of the variety, and not an appeal to a projective-morphism API that does not exist: the closed immersion is finite hence proper, the ambient projective space is proper over Spec k because the polynomial ring is of finite type over its degree-zero part, and overBase says the structure morphism is their composite.

class AlgebraicGeometry.Variety.IsProjective (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : Prop

Projectivity of X over k, expressed as the mere existence of a projective presentation. The chosen embedding remains separate data.

• presentation : Nonempty (ProjectivePresentation k X)

theorem AlgebraicGeometry.Variety.IsProjective.ofPresentation {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) : IsProjective k X

A chosen presentation proves the proposition that the variety is projective.

instance AlgebraicGeometry.Variety.isProper_of_isProjective {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsProjective k X] : IsProper (X ↘ Spec (CommRingCat.of k))

A projective variety is proper, independently of which presentation witnesses projectivity.