feat(algebraic_geometry/projective_spectrum): degree zero part of a l…

…ocalized ring (#13398)

If we have a graded ring A and some element f of A, the the localised ring A away from f has a degree zero part. This construction is useful because proj locally is spec of degree zero part of some localised ring.

Perhaps this ring belongs to some other file or different name, suggestions are very welcome

src/algebraic_geometry/projective_spectrum/scheme.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import algebraic_geometry.projective_spectrum.structure_sheaf
+import algebraic_geometry.Spec
+
+/-!
+# 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 `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`:
+  - forward direction :
+    for any `x : pbo f`, i.e. a relevant homogeneous prime ideal `x`, send it to
+    `x ∩ span {g / 1 | g ∈ A}` (see `Top_component.forward.carrier`). This ideal is prime, the proof
+    is in `Top_component.forward.to_fun`. The fact that this function is continuous is found in
+    `Top_component.forward`
+  - backward direction : 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`
+* `Top_component.forward`: `forward f` is the
+  continuous map between `Proj.T| pbo f` and `Spec.T A⁰_f`
+* `Top_component.forward.preimage_eq`: for any `a: A`, if `a/f^m` has degree zero, then the preimage
+  of `sbo a/f^m` under `forward f` is `pbo f ∩ pbo a`.
+
+
+* [Robin Hartshorne, *Algebraic Geometry*][Har77]: Chapter II.2 Proposition 2.5
+-/
+
+noncomputable theory
+
+namespace algebraic_geometry
+
+open_locale direct_sum big_operators pointwise big_operators
+open direct_sum set_like.graded_monoid localization finset (hiding mk_zero)
+
+variables {R A : Type*}
+variables [comm_ring R] [comm_ring A] [algebra R A]
+
+variables (𝒜 : ℕ → submodule R A)
+variables [graded_algebra 𝒜]
+
+open Top topological_space
+open category_theory opposite
+open projective_spectrum.structure_sheaf
+
+local notation `Proj` := Proj.to_LocallyRingedSpace 𝒜
+-- `Proj` as a locally ringed space
+local notation `Proj.T` := Proj .1.1.1
+-- the underlying topological space of `Proj`
+local notation `Proj| ` U := Proj .restrict (opens.open_embedding (U : opens Proj.T))
+-- `Proj` restrict to some open set
+local notation `Proj.T| ` U :=
+  (Proj .restrict (opens.open_embedding (U : opens Proj.T))).to_SheafedSpace.to_PresheafedSpace.1
+-- the underlying topological space of `Proj` restricted to some open set
+local notation `pbo` x := projective_spectrum.basic_open 𝒜 x
+-- basic open sets in `Proj`
+local notation `sbo` f := prime_spectrum.basic_open f
+-- basic open sets in `Spec`
+local notation `Spec` ring := Spec.LocallyRingedSpace_obj (CommRing.of ring)
+-- `Spec` as a locally ringed space
+local notation `Spec.T` ring :=
+  (Spec.LocallyRingedSpace_obj (CommRing.of ring)).to_SheafedSpace.to_PresheafedSpace.1
+-- the underlying topological space of `Spec`
+
+section
+variable {𝒜}
+/--
+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.
+-/
+def degree_zero_part {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) : subring (away f) :=
+{ carrier := { y | ∃ (n : ℕ) (a : 𝒜 (m * n)), y = mk a.1 ⟨f^n, ⟨n, rfl⟩⟩ },
+  mul_mem' := λ _ _ ⟨n, ⟨a, h⟩⟩ ⟨n', ⟨b, h'⟩⟩, h.symm ▸ h'.symm ▸
+    ⟨n+n', ⟨⟨a.1 * b.1, (mul_add m n n').symm ▸ mul_mem a.2 b.2⟩,
+    by {rw mk_mul, congr' 1, simp only [pow_add], refl }⟩⟩,
+  one_mem' := ⟨0, ⟨1, (mul_zero m).symm ▸ one_mem⟩,
+    by { symmetry, convert ← mk_self 1, simp only [pow_zero], refl, }⟩,
+  add_mem' := λ _ _ ⟨n, ⟨a, h⟩⟩ ⟨n', ⟨b, h'⟩⟩, h.symm ▸ h'.symm ▸
+    ⟨n+n', ⟨⟨f ^ n * b.1 + f ^ n' * a.1, (mul_add m n n').symm ▸
+      add_mem (mul_mem (by { rw mul_comm, exact set_like.graded_monoid.pow_mem n f_deg }) b.2)
+        begin
+          rw add_comm,
+          refine mul_mem _ a.2,
+          rw mul_comm,
+          exact set_like.graded_monoid.pow_mem _ f_deg
+        end⟩, begin
+          rw add_mk,
+          congr' 1,
+          simp only [pow_add],
+          refl,
+        end⟩⟩,
+  zero_mem' := ⟨0, ⟨0, (mk_zero _).symm⟩⟩,
+  neg_mem' := λ x ⟨n, ⟨a, h⟩⟩, h.symm ▸ ⟨n, ⟨-a, neg_mk _ _⟩⟩ }
+
+local notation `A⁰_` f_deg := degree_zero_part f_deg
+
+instance (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) : comm_ring (degree_zero_part f_deg) :=
+(degree_zero_part f_deg).to_comm_ring
+
+/--
+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`
+-/
+def degree_zero_part.deg {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (x : A⁰_ f_deg) : ℕ :=
+x.2.some
+
+/--
+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`
+-/
+def degree_zero_part.num {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (x : A⁰_ f_deg) : A :=
+x.2.some_spec.some.1
+
+lemma degree_zero_part.num_mem {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (x : A⁰_ f_deg) :
+  degree_zero_part.num f_deg x ∈ 𝒜 (m * degree_zero_part.deg f_deg x) :=
+x.2.some_spec.some.2
+
+lemma degree_zero_part.eq {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (x : A⁰_ f_deg) :
+  x.1 = mk (degree_zero_part.num f_deg x) ⟨f^(degree_zero_part.deg f_deg x), ⟨_, rfl⟩⟩ :=
+x.2.some_spec.some_spec
+
+lemma degree_zero_part.mul_val {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (x y : A⁰_ f_deg) :
+  (x * y).1 = x.1 * y.1 := rfl
+
+end
+
+end algebraic_geometry