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 f : A, 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.eq {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.mul_val {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).val = x.val * y.val