mathlib documentation

algebraic_geometry.projective_spectrum.scheme

Proj as a scheme #

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

def algebraic_geometry.degree_zero_part {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) :

The degree zero part of the localized ring Aₓ is the subring of elements of the form a/x^n such that a and x^n have the same degree.

Equations
Instances for algebraic_geometry.degree_zero_part
@[protected, instance]
def algebraic_geometry.degree_zero_part.comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] (f : A) {m : } (f_deg : f 𝒜 m) :
Equations
noncomputable def algebraic_geometry.degree_zero_part.deg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } {f_deg : f 𝒜 m} (x : (algebraic_geometry.degree_zero_part f_deg)) :

Every element in the degree zero part of Aₓ can be written as a/x^n for some a and n : ℕ, degree_zero_part.deg picks this natural number n

Equations
noncomputable def algebraic_geometry.degree_zero_part.num {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } {f_deg : f 𝒜 m} (x : (algebraic_geometry.degree_zero_part f_deg)) :
A

Every element in the degree zero part of Aₓ can be written as a/x^n for some a and n : ℕ, degree_zero_part.deg picks the numerator a

Equations
theorem algebraic_geometry.degree_zero_part.num_mem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } {f_deg : f 𝒜 m} (x : (algebraic_geometry.degree_zero_part f_deg)) :
theorem algebraic_geometry.degree_zero_part.coe_mul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (x y : (algebraic_geometry.degree_zero_part f_deg)) :
(x * y) = x * y
theorem algebraic_geometry.degree_zero_part.coe_one {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) :
1 = 1
theorem algebraic_geometry.degree_zero_part.coe_sum {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) {ι : Type u_3} (s : finset ι) (g : ι → (algebraic_geometry.degree_zero_part f_deg)) :
(s.sum (λ (i : ι), g i)) = s.sum (λ (i : ι), (g i))
def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : submodule R A} [graded_algebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (x : ((algebraic_geometry.Proj.to_LocallyRingedSpace 𝒜).restrict algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier._proof_1)) :

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

Equations

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.

Equations

The continuous function between the basic open set D(f) in Proj to the corresponding basic open set in Spec A⁰_f.

Equations

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 carrier.as_ideal.prime;
  • is relevant, as proved in carrier.relevant.
Equations