# Proj as a scheme #

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 AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.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 toSpec: for any x : pbo f, i.e. a relevant homogeneous prime ideal x, send it to A⁰_f ∩ span {g / 1 | g ∈ x} (see ProjIsoSpecTopComponent.IoSpec.carrier). This ideal is prime, the proof is in ProjIsoSpecTopComponent.ToSpec.toFun. The fact that this function is continuous is found in ProjIsoSpecTopComponent.toSpec
• backward direction fromSpec: 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 ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal;
• This ideal is also homogeneous, the proof can be found in ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous;
• This ideal is relevant, the proof can be found in ProjIsoSpecTopComponent.FromSpec.carrier.relevant;
• This ideal is prime, the proof can be found in ProjIsoSpecTopComponent.FromSpec.carrier.prime. Hence we have a well defined function Spec.T A⁰_f → Proj.T | (pbo f), this function is called ProjIsoSpecTopComponent.FromSpec.toFun. But to prove the continuity of this function, we need to prove fromSpec ∘ toSpec and toSpec ∘ fromSpec are both identities; these are achieved in ProjIsoSpecTopComponent.fromSpec_toSpec and ProjIsoSpecTopComponent.toSpec_fromSpec.

## Main Definitions and Statements #

For a homogeneous element f of degree m

• ProjIsoSpecTopComponent.toSpec: the continuous map between Proj.T| pbo f and Spec.T A⁰_f defined by sending x : Proj| (pbo f) to A⁰_f ∩ span {g / 1 | g ∈ x}. We also denote this map as ψ.
• ProjIsoSpecTopComponent.ToSpec.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.

If we further assume m is positive

• ProjIsoSpecTopComponent.fromSpec: the continuous map between Spec.T A⁰_f and Proj.T| pbo f defined by sending q to {a | aᵢᵐ/fⁱ ∈ q} where aᵢ is the i-th coordinate of a. We also denote this map as φ
• projIsoSpecTopComponent: the homeomorphism Proj.T| pbo f ≅ Spec.T A⁰_f obtained by φ and ψ.

## Reference #

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

Proj restrict to some open set

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) (z : ) :
Ideal.span (() '' (x).asHomogeneousIdeal)
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) [] {z : } (hz : z Ideal.span (() '' (x).asHomogeneousIdeal)) :
∃ (c : (() '' (x).asHomogeneousIdeal) →₀ ) (N : ) (acd : (y : ) → y Finset.image (c) c.supportA), f ^ N z = () (c.support.attach.sum fun (i : { x_1 : (() '' (x).asHomogeneousIdeal) // x_1 c.support }) => acd (c i) * )
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) [] {z : } :
∃ (c : (() '' (x).asHomogeneousIdeal) →₀ ) (N : ) (acd : (y : ) → y Finset.image (c) c.supportA), = () (c.support.attach.sum fun (i : { x_1 : (() '' (x).asHomogeneousIdeal) // x_1 c.support }) => acd (c i) * )
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_eq_span {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) :
= Ideal.span {z : | ∃ (s : A) (F : A) (_ : s (x).asHomogeneousIdeal) (n : ) (s_mem : s 𝒜 n) (F_mem1 : F 𝒜 n) (F_mem2 : ), z = Quotient.mk'' { deg := n, num := s, s_mem, den := F, F_mem1, den_mem := F_mem2 }}

For x : pbo f, the ideal A⁰_f ∩ span {g / 1 | g ∈ x} is equal to span {a/f^n | a ∈ x and deg(a) = deg(f^n)}.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.disjoint {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) :
Disjoint (x).asHomogeneousIdeal.toIdeal ()
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_ne_top {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (x : (.restrict ).toTopCat) :
def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] (f : A) (x : (.restrict ).toPresheafedSpace) :
.toPresheafedSpace

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 TopComponent.forward.

Equations
• = { asIdeal := , IsPrime := }
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_eq {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] (f : A) (a : A) (b : A) (k : ) (a_mem : a 𝒜 k) (b_mem1 : b 𝒜 k) (b_mem2 : ) :
⁻¹' (PrimeSpectrum.basicOpen (Quotient.mk'' { deg := k, num := a, a_mem, den := b, b_mem1, den_mem := b_mem2 })) = {x : (.restrict ).toPresheafedSpace | }
def AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] (f : A) :
(.restrict ).toPresheafedSpace .toPresheafedSpace

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

Equations
• = { toFun := , continuous_toFun := }
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_eq {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} (a : A) (b : A) (k : ) (a_mem : a 𝒜 k) (b_mem1 : b 𝒜 k) (b_mem2 : ) :
⁻¹' (PrimeSpectrum.basicOpen (Quotient.mk'' { deg := k, num := a, a_mem, den := b, b_mem1, den_mem := b_mem2 })) = {x : .obj (.restrict ).toPresheafedSpace | }
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (q : .toPresheafedSpace) :
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.asIdeal;
• is homogeneous, as proved in carrier.asHomogeneousIdeal;
• is prime, as proved in carrier.asIdeal.prime;
• is relevant, as proved in carrier.relevant.
Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (q : .toPresheafedSpace) (a : A) :
∀ (i : ), Quotient.mk'' { deg := m * i, num := () a ^ m, , den := f ^ i, , den_mem := } q.asIdeal
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (q : .toPresheafedSpace) (a : A) :
∀ (i : ), Localization.mk (() a ^ m) f ^ i, () '' {s : | s q.asIdeal}
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.add_mem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (q : .toPresheafedSpace) {a : A} {b : A} (ha : ) (hb : ) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.smul_mem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) (c : A) (x : A) (hx : ) :
def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :
def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.ne_top {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.prime {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : .toPresheafedSpace) :
.IsPrime
def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
.toPresheafedSpace(.restrict ).toPresheafedSpace

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (x : .toPresheafedSpace) :
@[deprecated AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec]
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpecFromSpec {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (x : .toPresheafedSpace) :

Alias of AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (x : (.restrict ).toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (𝒜 : ) [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (a : A) (i : ) :
'' {x : .obj (.restrict ).toPresheafedSpace | x ProjectiveSpectrum.basicOpen 𝒜 (( a) i)} = (PrimeSpectrum.basicOpen (Quotient.mk'' { deg := m * i, num := (( a) i) ^ m, , den := f ^ i, , den_mem := })).carrier
def AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
.toPresheafedSpace (.restrict ).toPresheafedSpace

The continuous function Spec A⁰_f → Proj|D(f) sending q to {a | aᵢᵐ/fⁱ ∈ q} where m is the degree of f

Equations
• = { toFun := , continuous_toFun := }
Instances For
def AlgebraicGeometry.projIsoSpecTopComponent {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {𝒜 : } [] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
(.restrict ).toPresheafedSpace .toPresheafedSpace

The homeomorphism Proj|D(f) ≅ Spec A⁰_f defined by

• φ : Proj|D(f) ⟶ Spec A⁰_f by sending x to A⁰_f ∩ span {g / 1 | g ∈ x}
• ψ : Spec A⁰_f ⟶ Proj|D(f) by sending q to {a | aᵢᵐ/fⁱ ∈ q}.
Equations
• One or more equations did not get rendered due to their size.
Instances For