feat(algebraic_geometry): structure sheaf on Spec R (#3907)

This defines the structure sheaf on Spec R, following Hartshorne, as a sheaf in `CommRing` on `prime_spectrum R`.

We still need to show at the stalk at a point is just the localization; this is another page of Hartshorne, and will come in a subsequent PR.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ashvni <ashvni.n@gmail.com>

Author: 3 people

src/algebraic_geometry/prime_spectrum.lean

@@ -63,7 +63,7 @@ namespace prime_spectrum
 as an ideal of that ring. -/
 abbreviation as_ideal (x : prime_spectrum R) : ideal R := x.val
 
-instance as_ideal.is_prime (x : prime_spectrum R) :
+instance is_prime (x : prime_spectrum R) :
   x.as_ideal.is_prime := x.2
 
 @[ext] lemma ext {x y : prime_spectrum R} :

src/algebraic_geometry/structure_sheaf.lean

@@ -0,0 +1,234 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison
+-/
+import algebraic_geometry.prime_spectrum
+import algebra.category.CommRing
+import topology.sheaves.local_predicate
+import topology.sheaves.forget
+import ring_theory.localization
+import ring_theory.subring
+
+/-!
+# The structure sheaf on `prime_spectrum R`.
+
+We define the structure sheaf on `Top.of (prime_spectrum R)`, for a commutative ring `R`.
+We define this as a subsheaf of the sheaf of dependent functions into the localizations,
+cut out by the condition that the function must be locally equal to a ratio of elements of `R`.
+
+Because the condition "is equal to a fraction" passes to smaller open subsets,
+the subset of functions satisfying this condition is automatically a subpresheaf.
+Because the condition "is locally equal to a fraction" is local,
+it is also a subsheaf.
+
+(It may be helpful to refer back to `topology.sheaves.sheaf_of_functions`,
+where we show that dependent functions into any type family form a sheaf,
+and also `topology.sheaves.local_predicate`, where we characterise the predicates
+which pick out sub-presheaves and sub-sheaves of these sheaves.)
+
+We also set up the ring structure, obtaining
+`structure_sheaf R : sheaf CommRing (Top.of (prime_spectrum R))`.
+-/
+
+universe u
+
+noncomputable theory
+
+variables (R : Type u) [comm_ring R]
+
+open Top
+open topological_space
+open category_theory
+open opposite
+
+namespace algebraic_geometry
+
+/--
+$Spec R$, just as a topological space.
+-/
+def Spec.Top : Top := Top.of (prime_spectrum R)
+
+namespace structure_sheaf
+
+/--
+The type family over `prime_spectrum R` consisting of the localization over each point.
+-/
+@[derive [comm_ring, local_ring]]
+def localizations (P : Spec.Top R) : Type u := localization.at_prime P.as_ideal
+
+instance (P : Spec.Top R) : inhabited (localizations R P) :=
+⟨(localization.of _).to_map 1⟩
+
+variables {R}
+
+/--
+The predicate saying that a dependent function on an open `U` is realised as a fixed fraction
+`r / s` in each of the stalks (which are localizations at various prime ideals).
+-/
+def is_fraction {U : opens (Spec.Top R)} (f : Π x : U, localizations R x) : Prop :=
+∃ (r s : R), ∀ x : U,
+  ¬ (s ∈ x.1.as_ideal) ∧ f x * (localization.of _).to_map s = (localization.of _).to_map r
+
+variables (R)
+
+/--
+The predicate `is_fraction` is "prelocal",
+in the sense that if it holds on `U` it holds on any open subset `V` of `U`.
+-/
+def is_fraction_prelocal : prelocal_predicate (localizations R) :=
+{ pred := λ U f, is_fraction f,
+  res := by { rintro V U i f ⟨r, s, w⟩, exact ⟨r, s, λ x, w (i x)⟩ } }
+
+/--
+We will define the structure sheaf as
+the subsheaf of all dependent functions in `Π x : U, localizations R x`
+consisting of those functions which can locally be expressed as a ratio of
+(the images in the localization of) elements of `R`.
+
+Quoting Hartshorne:
+
+For an open set $$U ⊆ Spec A$$, we define $$𝒪(U)$$ to be the set of functions
+$$s : U → ⨆_{𝔭 ∈ U} A_𝔭$$, such that $s(𝔭) ∈ A_𝔭$$ for each $$𝔭$$,
+and such that $$s$$ is locally a quotient of elements of $$A$$:
+to be precise, we require that for each $$𝔭 ∈ U$$, there is a neighborhood $$V$$ of $$𝔭$$,
+contained in $$U$$, and elements $$a, f ∈ A$$, such that for each $$𝔮 ∈ V, f ∉ 𝔮$$,
+and $$s(𝔮) = a/f$$ in $$A_𝔮$$.
+
+Now Hartshorne had the disadvantage of not knowing about dependent functions,
+so we replace his circumlocution about functions into a disjoint union with
+`Π x : U, localizations x`.
+-/
+def is_locally_fraction : local_predicate (localizations R) :=
+(is_fraction_prelocal R).sheafify
+
+@[simp]
+lemma is_locally_fraction_pred
+  {U : opens (Spec.Top R)} (f : Π x : U, localizations R x) :
+  (is_locally_fraction R).pred f =
+  ∀ x : U, ∃ (V) (m : x.1 ∈ V) (i : V ⟶ U),
+  ∃ (r s : R), ∀ y : V,
+  ¬ (s ∈ y.1.as_ideal) ∧
+    f (i y : U) * (localization.of _).to_map s = (localization.of _).to_map r :=
+rfl
+
+/--
+The functions satisfying `is_locally_fraction` form a submonoid.
+-/
+def sections_subring (U : (opens (Spec.Top R))ᵒᵖ) :
+  subring (Π x : unop U, localizations R x) :=
+{ carrier := { f | (is_locally_fraction R).pred f },
+  zero_mem' :=
+  begin
+    refine λ x, ⟨unop U, x.2, 𝟙 _, 0, 1, λ y, ⟨_, _⟩⟩,
+    { rw ←ideal.ne_top_iff_one, exact y.1.is_prime.1, },
+    { simp, },
+  end,
+  one_mem' :=
+  begin
+    refine λ x, ⟨unop U, x.2, 𝟙 _, 1, 1, λ y, ⟨_, _⟩⟩,
+    { rw ←ideal.ne_top_iff_one, exact y.1.is_prime.1, },
+    { simp, },
+  end,
+  add_mem' :=
+  begin
+    intros a b ha hb x,
+    rcases ha x with ⟨Va, ma, ia, ra, sa, wa⟩,
+    rcases hb x with ⟨Vb, mb, ib, rb, sb, wb⟩,
+    refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, opens.inf_le_left _ _ ≫ ia, ra * sb + rb * sa, sa * sb, _⟩,
+    intro y,
+    rcases wa (opens.inf_le_left _ _ y) with ⟨nma, wa⟩,
+    rcases wb (opens.inf_le_right _ _ y) with ⟨nmb, wb⟩,
+    fsplit,
+    { intro H, cases y.1.is_prime.mem_or_mem H; contradiction, },
+    { simp only [add_mul, ring_hom.map_add, pi.add_apply, ring_hom.map_mul],
+      erw [←wa, ←wb],
+      simp only [mul_assoc],
+      congr' 2,
+      rw [mul_comm], refl, }
+  end,
+  neg_mem' :=
+  begin
+    intros a ha x,
+    rcases ha x with ⟨V, m, i, r, s, w⟩,
+    refine ⟨V, m, i, -r, s, _⟩,
+    intro y,
+    rcases w y with ⟨nm, w⟩,
+    fsplit,
+    { exact nm, },
+    { simp only [ring_hom.map_neg, pi.neg_apply],
+      erw [←w],
+      simp only [neg_mul_eq_neg_mul_symm], }
+  end,
+  mul_mem' :=
+  begin
+    intros a b ha hb x,
+    rcases ha x with ⟨Va, ma, ia, ra, sa, wa⟩,
+    rcases hb x with ⟨Vb, mb, ib, rb, sb, wb⟩,
+    refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, opens.inf_le_left _ _ ≫ ia, ra * rb, sa * sb, _⟩,
+    intro y,
+    rcases wa (opens.inf_le_left _ _ y) with ⟨nma, wa⟩,
+    rcases wb (opens.inf_le_right _ _ y) with ⟨nmb, wb⟩,
+    fsplit,
+    { intro H, cases y.1.is_prime.mem_or_mem H; contradiction, },
+    { simp only [pi.mul_apply, ring_hom.map_mul],
+      erw [←wa, ←wb],
+      simp only [mul_left_comm, mul_assoc, mul_comm],
+      refl, }
+  end, }
+
+end structure_sheaf
+
+open structure_sheaf
+
+/--
+The structure sheaf (valued in `Type`, not yet `CommRing`) is the subsheaf consisting of
+functions satisfying `is_locally_fraction`.
+-/
+def structure_sheaf_in_Type : sheaf (Type u) (Spec.Top R):=
+subsheaf_to_Types (is_locally_fraction R)
+
+instance comm_ring_structure_sheaf_in_Type_obj (U : (opens (Spec.Top R))ᵒᵖ) :
+  comm_ring ((structure_sheaf_in_Type R).presheaf.obj U) :=
+(sections_subring R U).to_comm_ring
+
+/--
+The structure presheaf, valued in `CommRing`, constructed by dressing up the `Type` valued
+structure presheaf.
+-/
+@[simps]
+def structure_presheaf_in_CommRing : presheaf CommRing (Spec.Top R) :=
+{ obj := λ U, CommRing.of ((structure_sheaf_in_Type R).presheaf.obj U),
+  map := λ U V i,
+  { to_fun := ((structure_sheaf_in_Type R).presheaf.map i),
+    map_zero' := rfl,
+    map_add' := λ x y, rfl,
+    map_one' := rfl,
+    map_mul' := λ x y, rfl, }, }
+
+/--
+Some glue, verifying that that structure presheaf valued in `CommRing` agrees
+with the `Type` valued structure presheaf.
+-/
+def structure_presheaf_comp_forget :
+  structure_presheaf_in_CommRing R ⋙ (forget CommRing) ≅ (structure_sheaf_in_Type R).presheaf :=
+nat_iso.of_components
+  (λ U, iso.refl _)
+  (by tidy)
+
+/--
+The structure sheaf on $Spec R$, valued in `CommRing`.
+
+This is provided as a bundled `SheafedSpace` as `Spec.SheafedSpace R` later.
+-/
+def structure_sheaf : sheaf CommRing (Spec.Top R) :=
+{ presheaf := structure_presheaf_in_CommRing R,
+  sheaf_condition :=
+    -- We check the sheaf condition under `forget CommRing`.
+    (sheaf_condition_equiv_sheaf_condition_comp _ _).symm
+      (sheaf_condition_equiv_of_iso (structure_presheaf_comp_forget R).symm
+        (structure_sheaf_in_Type R).sheaf_condition), }
+
+-- TODO: we need to prove that the stalk at `P` is `localization.at_prime P.as_ideal`
+
+end algebraic_geometry