feat(algebraic_geometry/Scheme): improve cosmetics of definition (#7325)

Purely cosmetic, but the definition is going on a poster, so ...



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebraic_geometry/Scheme.lean

@@ -26,16 +26,16 @@ 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`.
+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.)
 -/
 structure Scheme extends X : LocallyRingedSpace :=
-(local_affine : ∀ x : carrier, ∃ (U : opens carrier) (m : x ∈ U) (R : CommRing)
-  (i : X.to_SheafedSpace.to_PresheafedSpace.restrict _ (opens.inclusion_open_embedding U) ≅
-    Spec.PresheafedSpace R), true)
+(local_affine : ∀ x : X, ∃ (U : open_nhds x) (R : CommRing),
+  nonempty (X.to_PresheafedSpace.restrict _ U.open_embedding ≅ Spec.PresheafedSpace R))
 
 -- PROJECT
 -- In fact, we can make the isomorphism `i` above an isomorphism in `LocallyRingedSpace`.
@@ -63,7 +63,7 @@ def to_LocallyRingedSpace (S : Scheme) : LocallyRingedSpace := { ..S }
 -/
 noncomputable
 def Spec (R : CommRing) : Scheme :=
-{ local_affine := λ x, ⟨⊤, trivial, R, (Spec.PresheafedSpace R).restrict_top_iso, trivial⟩,
+{ local_affine := λ x, ⟨⟨⊤, trivial⟩, R, ⟨(Spec.PresheafedSpace R).restrict_top_iso⟩⟩,
   .. Spec.LocallyRingedSpace R }
 
 /--

src/algebraic_geometry/presheafed_space.lean

@@ -197,12 +197,12 @@ subspace.
 -/
 @[simps]
 def to_restrict_top (X : PresheafedSpace C) :
-  X ⟶ X.restrict (opens.inclusion ⊤) (opens.inclusion_open_embedding ⊤) :=
+  X ⟶ X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) :=
 { base := ⟨λ x, ⟨x, trivial⟩, continuous_def.2 $ λ U ⟨S, hS, hSU⟩, hSU ▸ hS⟩,
   c := { app := λ U, X.presheaf.map $ (hom_of_le $ λ x hxU, ⟨⟨x, trivial⟩, hxU, rfl⟩ :
       (opens.map (⟨λ x, ⟨x, trivial⟩, continuous_def.2 $ λ U ⟨S, hS, hSU⟩, hSU ▸ hS⟩ :
           X.1 ⟶ (opens.to_Top X.1).obj ⊤)).obj (unop U) ⟶
-        (opens.inclusion_open_embedding ⊤).is_open_map.functor.obj (unop U)).op,
+        (opens.open_embedding ⊤).is_open_map.functor.obj (unop U)).op,
     naturality':= λ U V f, show X.presheaf.map _ ≫ _ = _ ≫ X.presheaf.map _,
       by { rw [← map_comp, ← map_comp], refl } } }
 
@@ -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.inclusion_open_embedding ⊤) ≅ X :=
+  X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) ≅ X :=
 { hom := X.of_restrict _ _ _,
   inv := X.to_restrict_top,
   hom_inv_id' := ext _ _ (concrete_category.hom_ext _ _ $ λ ⟨x, _⟩, rfl) $

src/topology/category/Top/open_nhds.lean

@@ -66,6 +66,9 @@ full_subcategory_inclusion _
 
 @[simp] lemma inclusion_obj (x : X) (U) (p) : (inclusion x).obj ⟨U,p⟩ = U := rfl
 
+lemma open_embedding {x : X} (U : open_nhds x) : open_embedding (U.1.inclusion) :=
+U.1.open_embedding
+
 instance open_nhds_is_filtered (x : X) : is_filtered (open_nhds x)ᵒᵖ :=
 { nonempty := ⟨op ⊤⟩,
   cocone_objs := λ U V, ⟨op (unop U ⊓ unop V),

src/topology/category/Top/opens.lean

@@ -119,7 +119,7 @@ def inclusion {X : Top.{u}} (U : opens X) : (to_Top X).obj U ⟶ X :=
 { to_fun := _,
   continuous_to_fun := continuous_subtype_coe }
 
-lemma inclusion_open_embedding {X : Top.{u}} (U : opens X) : open_embedding (inclusion U) :=
+lemma open_embedding {X : Top.{u}} (U : opens X) : open_embedding (inclusion U) :=
 is_open.open_embedding_subtype_coe U.2
 
 /-- `opens.map f` gives the functor from open sets in Y to open set in X,