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 (TBC).

Main Definitions and Statements

• degreeZeroPart: 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

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

• 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.

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

def AlgebraicGeometry.«termProj|_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) : Ideal (HomogeneousLocalization.Away 𝒜 f)

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.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) (z : HomogeneousLocalization.Away 𝒜 f) : z ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x ↔ HomogeneousLocalization.val z ∈ Ideal.span (⇑(algebraMap A (Localization.Away f)) '' ↑(↑x).asHomogeneousIdeal)

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) [DecidableEq (Localization.Away f)] {z : Localization.Away f} (hz : z ∈ Ideal.span (⇑(algebraMap A (Localization.Away f)) '' ↑(↑x).asHomogeneousIdeal)) : ∃ (c : ↑(⇑(algebraMap A (Localization.Away f)) '' ↑(↑x).asHomogeneousIdeal) →₀ Localization.Away f) (N : ℕ) (acd : (y : Localization.Away f) → y ∈ Finset.image (⇑c) c.support → A), f ^ N • z = (algebraMap A (Localization.Away f)) (Finset.sum (Finset.attach c.support) fun (i : { x_1 : ↑(⇑(algebraMap A (Localization.Away f)) '' ↑(↑x).asHomogeneousIdeal) // x_1 ∈ c.support }) => acd (c ↑i) ⋯ * Exists.choose ⋯)

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) [DecidableEq (Localization.Away f)] {z : HomogeneousLocalization.Away 𝒜 f} (hz : z ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x) : ∃ (c : ↑(⇑(algebraMap A (Localization.Away f)) '' ↑(↑x).asHomogeneousIdeal) →₀ Localization.Away f) (N : ℕ) (acd : (y : Localization.Away f) → y ∈ Finset.image (⇑c) c.support → A), f ^ N • HomogeneousLocalization.val z = (algebraMap A (Localization.Away f)) (Finset.sum (Finset.attach c.support) fun (i : { x_1 : ↑(⇑(algebraMap A (Localization.Away f)) '' ↑(↑x).asHomogeneousIdeal) // x_1 ∈ c.support }) => acd (c ↑i) ⋯ * Exists.choose ⋯)

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_eq_span {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) : AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x = Ideal.span {z : HomogeneousLocalization.Away 𝒜 f | ∃ (s : A) (F : A) (_ : s ∈ (↑x).asHomogeneousIdeal) (n : ℕ) (s_mem : s ∈ 𝒜 n) (F_mem1 : F ∈ 𝒜 n) (F_mem2 : F ∈ Submonoid.powers f), z = Quotient.mk'' { deg := n, num := { val := s, property := s_mem }, den := { val := F, property := 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} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) : Disjoint ↑(HomogeneousIdeal.toIdeal (↑x).asHomogeneousIdeal) ↑(Submonoid.powers f)

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_ne_top {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯))) : AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x ≠ ⊤

def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] (f : A) (x : ↑↑(AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯).toPresheafedSpace) : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).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

• AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f x = { asIdeal := AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x, IsPrime := ⋯ }

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_eq {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] (f : A) (a : A) (b : A) (k : ℕ) (a_mem : a ∈ 𝒜 k) (b_mem1 : b ∈ 𝒜 k) (b_mem2 : b ∈ Submonoid.powers f) : AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f ⁻¹' ↑(PrimeSpectrum.basicOpen (Quotient.mk'' { deg := k, num := { val := a, property := a_mem }, den := { val := b, property := b_mem1 }, den_mem := b_mem2 })) = {x : ↑↑(AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯).toPresheafedSpace | ↑x ∈ ProjectiveSpectrum.basicOpen 𝒜 f ⊓ ProjectiveSpectrum.basicOpen 𝒜 a}

def AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} : ↑(AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯).toPresheafedSpace ⟶ ↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace

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

Equations

• AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec = { toFun := AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f, continuous_toFun := ⋯ }

def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac_aux : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).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.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) : a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ ∀ (i : ℕ), Quotient.mk'' { deg := m * i, num := { val := (GradedAlgebra.proj 𝒜 i) a ^ m, property := ⋯ }, den := { val := f ^ i, property := ⋯ }, den_mem := ⋯ } ∈ q.asIdeal

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) : a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ ∀ (i : ℕ), Localization.mk ((GradedAlgebra.proj 𝒜 i) a ^ m) { val := f ^ i, property := ⋯ } ∈ ⇑(algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f)) '' {s : HomogeneousLocalization.Away 𝒜 f | s ∈ q.asIdeal}

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.add_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) {a : A} {b : A} (ha : a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q) (hb : b ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q) : a + b ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : 0 ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.smul_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (c : A) (x : A) (hx : x ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q) : c • x ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q

def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : Ideal A

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.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : Ideal.IsHomogeneous 𝒜 (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q)

def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : HomogeneousIdeal 𝒜

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.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : f ∉ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal f_deg hm q

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.ne_top {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q ≠ ⊤

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.prime {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : Ideal.IsPrime (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q)

def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace → ↑↑(AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯).toPresheafedSpace

The function 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.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) (x : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) : AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm x) = x

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) (x : ↑↑(AlgebraicGeometry.LocallyRingedSpace.restrict (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜) ⋯).toPresheafedSpace) : AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec x) = x

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) : Function.Injective ⇑AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) : Function.Surjective ⇑AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) : Function.Bijective ⇑AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec