feat(algebraic_geometry): Redefine Schemes in terms of isos of locall…

…y ringed spaces (#8888)

Addresses the project mentioned in `Scheme.lean` to redefine Schemes in terms of isomorphisms of locally ringed spaces, instead of presheafed spaces.

src/algebraic_geometry/Scheme.lean

@@ -29,24 +29,12 @@ namespace algebraic_geometry
 We define `Scheme` as a `X : LocallyRingedSpace`,
 along with a proof that every point has an open neighbourhood `U`
 so that that the restriction of `X` to `U` is isomorphic,
-as a space with a presheaf of commutative rings,
-to `Spec.PresheafedSpace R` for some `R : CommRing`.
-
-(Note we're not asking in the definition that this is an isomorphism as locally ringed spaces,
-although that is a consequence.)
+as a locally ringed space, to `Spec.to_LocallyRingedSpace.obj (op R)`
+for some `R : CommRing`.
 -/
 structure Scheme extends X : LocallyRingedSpace :=
 (local_affine : ∀ x : X, ∃ (U : open_nhds x) (R : CommRing),
-  nonempty (X.to_PresheafedSpace.restrict _ U.open_embedding ≅ Spec.to_PresheafedSpace.obj (op R)))
-
--- 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 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.
+  nonempty (X.restrict _ U.open_embedding ≅ Spec.to_LocallyRingedSpace.obj (op R)))
 
 namespace Scheme
 
@@ -67,7 +55,8 @@ induced_category.category Scheme.to_LocallyRingedSpace
 The spectrum of a commutative ring, as a scheme.
 -/
 def Spec_obj (R : CommRing) : Scheme :=
-{ local_affine := λ x, ⟨⟨⊤, trivial⟩, R, ⟨(Spec.to_PresheafedSpace.obj (op R)).restrict_top_iso⟩⟩,
+{ local_affine := λ x,
+  ⟨⟨⊤, trivial⟩, R, ⟨(Spec.to_LocallyRingedSpace.obj (op R)).restrict_top_iso⟩⟩,
   .. Spec.LocallyRingedSpace_obj R }
 
 @[simp] lemma Spec_obj_to_LocallyRingedSpace (R : CommRing) :

src/algebraic_geometry/locally_ringed_space.lean

@@ -176,6 +176,14 @@ noncomputable def restrict {U : Top} (X : LocallyRingedSpace) (f : U ⟶ X.to_To
   end,
   .. X.to_SheafedSpace.restrict f h }
 
+/--
+The restriction of a locally ringed space `X` to the top subspace is isomorphic to `X` itself.
+-/
+noncomputable def restrict_top_iso (X : LocallyRingedSpace) :
+  X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) ≅ X :=
+@iso_of_SheafedSpace_iso (X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤)) X
+  X.to_SheafedSpace.restrict_top_iso
+
 /--
 The global sections, notated Gamma.
 -/

src/algebraic_geometry/sheafed_space.lean

@@ -67,6 +67,7 @@ show category (induced_category (PresheafedSpace C) SheafedSpace.to_PresheafedSp
 by apply_instance
 
 /-- Forgetting the sheaf condition is a functor from `SheafedSpace C` to `PresheafedSpace C`. -/
+@[derive [full, faithful]]
 def forget_to_PresheafedSpace : (SheafedSpace C) ⥤ (PresheafedSpace C) :=
 induced_functor _
 
@@ -116,6 +117,16 @@ def restrict {U : Top} (X : SheafedSpace C)
     (sheaf_condition_equalizer_products.fork.iso_of_open_embedding h 𝒰).symm,
   ..X.to_PresheafedSpace.restrict f h }
 
+/--
+The restriction of a sheafed space `X` to the top subspace is isomorphic to `X` itself.
+-/
+noncomputable
+def restrict_top_iso (X : SheafedSpace C) :
+  X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) ≅ X :=
+@preimage_iso _ _ _ _ forget_to_PresheafedSpace _ _
+  (X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤)) _
+  X.to_PresheafedSpace.restrict_top_iso
+
 /--
 The global sections, notated Gamma.
 -/