# mathlib3documentation

algebraic_geometry.projective_spectrum.scheme

# 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

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] [ A] (𝒜 : A) {f : A} (x : ) :

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
theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (𝒜 : A) {f : A} (x : ) (z : f) :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier.clear_denominator' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} (x : ) {z : localization.away f} (hz : z ideal.span ( '' (x.val.as_homogeneous_ideal))) :
(c : ( '' (x.val.as_homogeneous_ideal)) →₀ (N : ) (acd : Π (y : , y A), f ^ N z = (c.support.attach.sum (λ (i : {x_1 // x_1 c.support}), acd (c i) _ * Exists.some _))
theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier.clear_denominator {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (𝒜 : A) {f : A} (x : ) {z : f}  :
(c : ( '' (x.val.as_homogeneous_ideal)) →₀ (N : ) (acd : Π (y : , y A), = (c.support.attach.sum (λ (i : {x_1 // x_1 c.support}), acd (c i) _ * Exists.some _))
theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.disjoint {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} (x : ) :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier_ne_top {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} (x : ) :
def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.to_fun {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (𝒜 : A) (f : A)  :

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
theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.preimage_eq {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} (f a b : A) (k : ) (a_mem : a 𝒜 k) (b_mem1 : b 𝒜 k) (b_mem2 : b ) :
⁻¹' (prime_spectrum.basic_open (quotient.mk' {deg := k, num := a, a_mem⟩, denom := b, b_mem1⟩, denom_mem := b_mem2})) =
def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (𝒜 : A) {f : A} :

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

Equations
def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m)  :
set A

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
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (a : A) :
(i : ), quotient.mk' {deg := m * i, num := i) a ^ m, _⟩, denom := f ^ i, _⟩, denom_mem := _} q.as_ideal
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (a : A) :
(i : ), localization.mk ( i) a ^ m) f ^ i, _⟩
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.add_mem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) {a b : A}  :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.zero_mem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.smul_mem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (c x : A)  :
def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :

For a prime ideal q in A⁰_f, the set {a | aᵢᵐ/fⁱ ∈ q} as an ideal.

Equations
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.homogeneous {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :
def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :

For a prime ideal q in A⁰_f, the set {a | aᵢᵐ/fⁱ ∈ q} as a homogeneous ideal.

Equations
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.denom_not_mem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.relevant {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.ne_top {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :
theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.prime {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m)  :
def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.to_fun {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {𝒜 : A} {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.to_fun._proof_1).to_SheafedSpace.to_PresheafedSpace.carrier)

The function Spec A⁰_f → Proj|D(f) by sending q to {a | aᵢᵐ/fⁱ ∈ q}.

Equations