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 #

• Proj : Proj as a locally ringed space
• Proj.T : the underlying topological space of Proj
• Proj| U : Proj restricted to some open set U
• Proj.T| U : the underlying topological space of Proj restricted to open set U
• pbo f : basic open set at f in Proj
• Spec : Spec as a locally ringed space
• Spec.T : the underlying topological space of Spec
• sbo g : basic open set at g in Spec
• A⁰_x : the degree zero part of localized ring Aₓ

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:

• forward direction to_Spec: for any x : pbo f, i.e. a relevant homogeneous prime ideal x, send it to A⁰_f ∩ span {g / 1 | g ∈ x} (see Proj_iso_Spec_Top_component.to_Spec.carrier). This ideal is prime, the proof is in Proj_iso_Spec_Top_component.to_Spec.to_fun. The fact that this function is continuous is found in Proj_iso_Spec_Top_component.to_Spec
• backward direction from_Spec: for any q : Spec A⁰_f, we send it to {a | ∀ i, aᵢᵐ/fⁱ ∈ q}; we need this to be a homogeneous prime ideal that is relevant.
  • This is in fact an ideal, the proof can be found in Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal;
  • This ideal is also homogeneous, the proof can be found in Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.homogeneous;
  • This ideal is relevant, the proof can be found in Proj_iso_Spec_Top_component.from_Spec.carrier.relevant;
  • This ideal is prime, the proof can be found in Proj_iso_Spec_Top_component.from_Spec.carrier.prime. Hence we have a well defined function Spec.T A⁰_f → Proj.T | (pbo f), this function is called Proj_iso_Spec_Top_component.from_Spec.to_fun. But to prove the continuity of this function, we need to prove from_Spec ∘ to_Spec and to_Spec ∘ from_Spec are both identities (TBC).

Main Definitions and Statements #

• degree_zero_part: the degree zero part of the localized ring Aₓ where x is a homogeneous element of degree n is the subring of elements of the form a/f^m where a has degree mn.

For a homogeneous element f of degree n

• Proj_iso_Spec_Top_component.to_Spec: forward f is the continuous map between Proj.T| pbo f and Spec.T A⁰_f

• Proj_iso_Spec_Top_component.to_Spec.preimage_eq: for any a: A, if a/f^m has degree zero, then the preimage of sbo a/f^m under to_Spec f is pbo f ∩ pbo a.

• Robin Hartshorne, Algebraic Geometry: Chapter II.2 Proposition 2.5