mathlib3 documentation


Proj as a scheme #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is to prove that Proj is a scheme.

Notation #

Implementation #

In src/algebraic_geometry/projective_spectrum/structure_sheaf.lean, we have given Proj a structure sheaf so that Proj is a locally ringed space. In this file we will prove that Proj equipped with this structure sheaf is a scheme. We achieve this by using an affine cover by basic open sets in Proj, more specifically:

  1. We prove that Proj can be covered by basic open sets at homogeneous element of positive degree.
  2. We prove that for any homogeneous element f : A of positive degree m, Proj.T | (pbo f) is homeomorphic to Spec.T A⁰_f:

Main Definitions and Statements #

For a homogeneous element f of degree n

For any x in Proj| (pbo f), the corresponding ideal in Spec A⁰_f. This fact that this ideal is prime is proven in Top_component.forward.to_fun


The function between the basic open set D(f) in Proj to the corresponding basic open set in Spec A⁰_f. This is bundled into a continuous map in Top_component.forward.


The function from Spec A⁰_f to Proj|D(f) is defined by q ↦ {a | aᵢᵐ/fⁱ ∈ q}, i.e. sending q a prime ideal in A⁰_f to the homogeneous prime relevant ideal containing only and all the elements a : A such that for every i, the degree 0 element formed by dividing the m-th power of the i-th projection of a by the i-th power of the degree-m homogeneous element f, lies in q.

The set {a | aᵢᵐ/fⁱ ∈ q}

  • is an ideal, as proved in carrier.as_ideal;
  • is homogeneous, as proved in carrier.as_homogeneous_ideal;
  • is prime, as proved in;
  • is relevant, as proved in carrier.relevant.