feat(algebraic_geometry): Restriction of locally ringed spaces (#8809)

Proves that restriction of presheafed spaces doesn't change the stalks and defines the restriction of a locally ringed space along an open embedding.

src/algebraic_geometry/Scheme.lean

@@ -42,14 +42,11 @@ structure Scheme extends X : LocallyRingedSpace :=
 -- PROJECT
 -- In fact, we can make the isomorphism `i` above an isomorphism in `LocallyRingedSpace`.
 -- However this is a consequence of the above definition, and not necessary for defining schemes.
--- We haven't done this yet because we haven't shown that you can restrict a `LocallyRingedSpace`
--- along an open embedding.
--- We can do this already for `SheafedSpace` (as above), but we need to know that
--- the stalks of the restriction are still local rings, which we follow if we knew that
--- the stalks didn't change.
--- This will follow if we define cofinal functors, and show precomposing with a cofinal functor
--- doesn't change colimits, because open neighbourhoods of `x` within `U` are cofinal in
--- all open neighbourhoods of `x`.
+-- We haven't done this yet because we don't currently have an analogue of
+-- `PresheafedSpace.restrict_top_iso` for locally ringed spaces. But this is needed below to show
+-- that the spectrum of a ring is indeed a scheme.
+-- This will follow once we have shown that the forgetful functor
+-- `LocallyRingedSpace ⥤ SheafedSpace CommRing` reflects isomorphisms.
 
 namespace Scheme
 

src/algebraic_geometry/locally_ringed_space.lean

@@ -8,7 +8,7 @@ import algebraic_geometry.sheafed_space
 import algebra.category.CommRing.limits
 import algebra.category.CommRing.colimits
 import algebraic_geometry.stalks
-import ring_theory.ideal.local_ring
+import data.equiv.transfer_instance
 
 /-!
 # The category of locally ringed spaces
@@ -160,23 +160,21 @@ instance : reflects_isomorphisms forget_to_SheafedSpace :=
     ⟨hom_of_SheafedSpace_hom_of_is_iso (category_theory.inv (forget_to_SheafedSpace.map f)),
       hom_ext _ _ (is_iso.hom_inv_id _), hom_ext _ _ (is_iso.inv_hom_id _)⟩ } }
 
--- PROJECT: once we have `PresheafedSpace.restrict_stalk_iso`
--- (that restriction doesn't change stalks) we can uncomment this.
-/-
-def restrict {U : Top} (X : LocallyRingedSpace)
-  (f : U ⟶ X.to_Top) (h : open_embedding f) : LocallyRingedSpace :=
+/--
+The restriction of a locally ringed space along an open embedding.
+-/
+@[simps]
+noncomputable def restrict {U : Top} (X : LocallyRingedSpace) (f : U ⟶ X.to_Top)
+  (h : open_embedding f) : LocallyRingedSpace :=
 { local_ring :=
   begin
     intro x,
     dsimp at *,
     -- We show that the stalk of the restriction is isomorphic to the original stalk,
-    have := X.to_SheafedSpace.to_PresheafedSpace.restrict_stalk_iso f h x,
-    -- and then transfer `local_ring` across the ring equivalence.
-    apply (this.CommRing_iso_to_ring_equiv).local_ring, -- import data.equiv.transfer_instance
-    apply X.local_ring,
+    apply @ring_equiv.local_ring _ _ _ (X.local_ring (f x)),
+    exact (X.to_PresheafedSpace.restrict_stalk_iso f h x).symm.CommRing_iso_to_ring_equiv,
   end,
-  .. X.to_SheafedSpace.restrict _ f h }
--/
+  .. X.to_SheafedSpace.restrict f h }
 
 /--
 The global sections, notated Gamma.

src/algebraic_geometry/presheafed_space.lean

@@ -181,7 +181,7 @@ def restrict {U : Top} (X : PresheafedSpace C)
 /--
 The map from the restriction of a presheafed space.
 -/
-def of_restrict (U : Top) (X : PresheafedSpace C)
+def of_restrict {U : Top} (X : PresheafedSpace C)
   (f : U ⟶ (X : Top.{v})) (h : open_embedding f) :
   X.restrict f h ⟶ X :=
 { base := f,
@@ -211,7 +211,7 @@ The isomorphism from the restriction to the top subspace.
 @[simps]
 def restrict_top_iso (X : PresheafedSpace C) :
   X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) ≅ X :=
-{ hom := X.of_restrict _ _ _,
+{ hom := X.of_restrict _ _,
   inv := X.to_restrict_top,
   hom_inv_id' := ext _ _ (concrete_category.hom_ext _ _ $ λ ⟨x, _⟩, rfl) $
     nat_trans.ext _ _ $ funext $ λ U, by { op_induction U,

src/algebraic_geometry/stalks.lean

@@ -4,13 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebraic_geometry.presheafed_space
+import category_theory.limits.final
 import topology.sheaves.stalks
 
 /-!
 # Stalks for presheaved spaces
 
 This file lifts constructions of stalks and pushforwards of stalks to work with
-the category of presheafed spaces.
+the category of presheafed spaces. Additionally, we prove that restriction of
+presheafed spaces does not change the stalks.
 -/
 
 noncomputable theory
@@ -50,22 +52,36 @@ by rw [stalk_map, stalk_functor_map_germ_assoc, stalk_pushforward_germ]
 
 section restrict
 
--- PROJECT: restriction preserves stalks.
--- We'll want to define cofinal functors, show precomposing with a cofinal functor preserves
--- colimits, and (easily) verify that "open neighbourhoods of x within U" is cofinal in "open
--- neighbourhoods of x".
-/-
+/--
+For an open embedding `f : U ⟶ X` and a point `x : U`, we get an isomorphism between the stalk
+of `X` at `f x` and the stalk of the restriction of `X` along `f` at t `x`.
+-/
 def restrict_stalk_iso {U : Top} (X : PresheafedSpace C)
   (f : U ⟶ (X : Top.{v})) (h : open_embedding f) (x : U) :
   (X.restrict f h).stalk x ≅ X.stalk (f x) :=
 begin
-  dsimp only [stalk, Top.presheaf.stalk, stalk_functor],
-  dsimp [colim],
-  sorry
+  -- As a left adjoint, the functor `h.is_open_map.functor_nhds x` is initial.
+  haveI := initial_of_adjunction (h.is_open_map.adjunction_nhds x),
+  -- Typeclass resolution knows that the opposite of an initial functor is final. The result
+  -- follows from the general fact that postcomposing with a final functor doesn't change colimits.
+  exact final.colimit_iso (h.is_open_map.functor_nhds x).op
+    ((open_nhds.inclusion (f x)).op ⋙ X.presheaf),
 end
 
--- TODO `restrict_stalk_iso` is compatible with `germ`.
--/
+@[simp, elementwise, reassoc]
+lemma restrict_stalk_iso_hom_eq_germ {U : Top} (X : PresheafedSpace C) (f : U ⟶ (X : Top.{v}))
+  (h : open_embedding f) (V : opens U) (x : U) (hx : x ∈ V) :
+  (X.restrict f h).presheaf.germ ⟨x, hx⟩ ≫ (restrict_stalk_iso X f h x).hom =
+  X.presheaf.germ ⟨f x, show f x ∈ h.is_open_map.functor.obj V, from ⟨x, hx, rfl⟩⟩ :=
+colimit.ι_pre ((open_nhds.inclusion (f x)).op ⋙ X.presheaf)
+  (h.is_open_map.functor_nhds x).op (op ⟨V, hx⟩)
+
+@[simp, elementwise, reassoc]
+lemma restrict_stalk_iso_inv_eq_germ {U : Top} (X : PresheafedSpace C) (f : U ⟶ (X : Top.{v}))
+  (h : open_embedding f) (V : opens U) (x : U) (hx : x ∈ V) :
+  X.presheaf.germ ⟨f x, show f x ∈ h.is_open_map.functor.obj V, from ⟨x, hx, rfl⟩⟩ ≫
+  (restrict_stalk_iso X f h x).inv = (X.restrict f h).presheaf.germ ⟨x, hx⟩ :=
+by rw [← restrict_stalk_iso_hom_eq_germ, category.assoc, iso.hom_inv_id, category.comp_id]
 
 end restrict
 

src/topology/category/Top/open_nhds.lean

@@ -100,4 +100,31 @@ nat_iso.of_components
 @[simp] lemma inclusion_map_iso_inv (x : X) : (inclusion_map_iso f x).inv = 𝟙 _ := rfl
 
 end open_nhds
+
 end topological_space
+
+namespace is_open_map
+
+open topological_space
+
+variables {f}
+
+/--
+An open map `f : X ⟶ Y` induces a functor `open_nhds x ⥤ open_nhds (f x)`.
+-/
+@[simps]
+def functor_nhds (h : is_open_map f) (x : X) :
+  open_nhds x ⥤ open_nhds (f x) :=
+{ obj := λ U, ⟨h.functor.obj U.1, ⟨x, U.2, rfl⟩⟩,
+  map := λ U V i, h.functor.map i }
+
+/--
+An open map `f : X ⟶ Y` induces an adjunction between `open_nhds x` and `open_nhds (f x)`.
+-/
+def adjunction_nhds (h : is_open_map f) (x : X) :
+  is_open_map.functor_nhds h x ⊣ open_nhds.map f x :=
+adjunction.mk_of_unit_counit
+{ unit := { app := λ U, hom_of_le $ λ x hxU, ⟨x, hxU, rfl⟩ },
+  counit := { app := λ V, hom_of_le $ λ y ⟨x, hfxV, hxy⟩, hxy ▸ hfxV } }
+
+end is_open_map