refactor(algebraic_geometry/structure_sheaf): Enclose definitions in structure_sheaf namespace (#8010)

Moves some pretty generic names like `const` and `to_open` to the `structure_sheaf` namespace.

Author: justus-springer

src/algebraic_geometry/Spec.lean

@@ -34,6 +34,7 @@ noncomputable theory
 namespace algebraic_geometry
 open opposite
 open category_theory
+open structure_sheaf
 
 /--
 The spectrum of a commutative ring, as a topological space.
@@ -83,16 +84,16 @@ The induced map of a ring homomorphism on the ring spectra, as a morphism of she
   Spec.SheafedSpace_obj S ⟶ Spec.SheafedSpace_obj R :=
 { base := Spec.Top_map f,
   c :=
-  { app := λ U, structure_sheaf.comap f (unop U)
-      ((topological_space.opens.map (Spec.Top_map f)).obj (unop U)) (λ p, id),
+  { app := λ U, comap f (unop U) ((topological_space.opens.map (Spec.Top_map f)).obj (unop U))
+      (λ p, id),
     naturality' := λ U V i, ring_hom.ext $ λ s, subtype.eq $ funext $ λ p, rfl } }
 
 @[simp] lemma Spec.SheafedSpace_map_id {R : CommRing} :
   Spec.SheafedSpace_map (𝟙 R) = 𝟙 (Spec.SheafedSpace_obj R) :=
 PresheafedSpace.ext _ _ (Spec.Top_map_id R) $ nat_trans.ext _ _ $ funext $ λ U,
 begin
   dsimp,
-  erw [PresheafedSpace.id_c_app, structure_sheaf.comap_id], swap,
+  erw [PresheafedSpace.id_c_app, comap_id], swap,
     { rw [Spec.Top_map_id, topological_space.opens.map_id_obj_unop] },
   rw [eq_to_hom_op, eq_to_hom_map, eq_to_hom_trans],
   refl,
@@ -104,7 +105,7 @@ PresheafedSpace.ext _ _ (Spec.Top_map_comp f g) $ nat_trans.ext _ _ $ funext $ 
 begin
   dsimp,
   erw [Top.presheaf.pushforward.comp_inv_app, ← category.assoc, category.comp_id,
-    (structure_sheaf T).presheaf.map_id, category.comp_id, structure_sheaf.comap_comp],
+    (structure_sheaf T).presheaf.map_id, category.comp_id, comap_comp],
   refl,
 end
 

src/algebraic_geometry/structure_sheaf.lean

@@ -256,6 +256,9 @@ def structure_sheaf : sheaf CommRing (prime_spectrum.Top R) :=
       (sheaf_condition_equiv_of_iso (structure_presheaf_comp_forget R).symm
         (structure_sheaf_in_Type R).sheaf_condition), }
 
+
+namespace structure_sheaf
+
 @[simp] lemma res_apply (U V : opens (prime_spectrum.Top R)) (i : V ⟶ U)
   (s : (structure_sheaf R).presheaf.obj (op U)) (x : V) :
   ((structure_sheaf R).presheaf.map i.op s).1 x = (s.1 (i x) : _) :=
@@ -797,30 +800,31 @@ At the moment, we work with arbitrary dependent functions `s : Π x : U, localiz
 we prove the predicate `is_locally_fraction` is preserved by this map, hence it can be extended to
 a morphism between the structure sheaves of `R` and `S`.
 -/
-def structure_sheaf.comap_fun (f : R →+* S) (U : opens (prime_spectrum.Top R))
-  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1)
+def comap_fun (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (prime_spectrum.comap f) ⁻¹' U.1)
   (s : Π x : U, localizations R x) (y : V) : localizations S y :=
-localization.local_ring_hom (comap f y.1).as_ideal _ f rfl (s ⟨(comap f y.1), hUV y.2⟩ : _)
+localization.local_ring_hom (prime_spectrum.comap f y.1).as_ideal _ f rfl
+  (s ⟨(prime_spectrum.comap f y.1), hUV y.2⟩ : _)
 
-lemma structure_sheaf.comap_fun_is_locally_fraction (f : R →+* S)
+lemma comap_fun_is_locally_fraction (f : R →+* S)
   (U : opens (prime_spectrum.Top R)) (V : opens (prime_spectrum.Top S))
-  (hUV : V.1 ⊆ (comap f) ⁻¹' U.1) (s : Π x : U, localizations R x)
+  (hUV : V.1 ⊆ (prime_spectrum.comap f) ⁻¹' U.1) (s : Π x : U, localizations R x)
   (hs : (is_locally_fraction R).to_prelocal_predicate.pred s) :
-  (is_locally_fraction S).to_prelocal_predicate.pred (structure_sheaf.comap_fun f U V hUV s) :=
+  (is_locally_fraction S).to_prelocal_predicate.pred (comap_fun f U V hUV s) :=
 begin
   rintro ⟨p, hpV⟩,
-  -- Since `s` is locally fraction, we can find a neighborhood `W` of `comap f p` in `U`, such
-  -- that `s = a / b` on `W`, for some ring elements `a, b : R`.
-  rcases hs ⟨comap f p, hUV hpV⟩ with ⟨W, m, iWU, a, b, h_frac⟩,
+  -- Since `s` is locally fraction, we can find a neighborhood `W` of `prime_spectrum.comap f p`
+  -- in `U`, such that `s = a / b` on `W`, for some ring elements `a, b : R`.
+  rcases hs ⟨prime_spectrum.comap f p, hUV hpV⟩ with ⟨W, m, iWU, a, b, h_frac⟩,
   -- We claim that we can write our new section as the fraction `f a / f b` on the neighborhood
   -- `(comap f) ⁻¹ W ⊓ V` of `p`.
   refine ⟨opens.comap (comap_continuous f) W ⊓ V, ⟨m, hpV⟩, opens.inf_le_right _ _, f a, f b, _⟩,
   rintro ⟨q, ⟨hqW, hqV⟩⟩,
   specialize h_frac ⟨prime_spectrum.comap f q, hqW⟩,
   refine ⟨h_frac.1, _⟩,
-  dsimp only [structure_sheaf.comap_fun],
-  erw [← localization.local_ring_hom_to_map ((comap f q).as_ideal), ← ring_hom.map_mul,
-    h_frac.2, localization.local_ring_hom_to_map],
+  dsimp only [comap_fun],
+  erw [← localization.local_ring_hom_to_map ((prime_spectrum.comap f q).as_ideal),
+    ← ring_hom.map_mul, h_frac.2, localization.local_ring_hom_to_map],
   refl,
 end
 
@@ -832,41 +836,41 @@ at `U` to the structure sheaf of `S` at `V`.
 Explicitly, this map is given as follows: For a point `p : V`, if the section `s` evaluates on `p`
 to the fraction `a / b`, its image on `V` evaluates on `p` to the fraction `f(a) / f(b)`.
 -/
-def structure_sheaf.comap (f : R →+* S) (U : opens (prime_spectrum.Top R))
-  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1) :
+def comap (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (prime_spectrum.comap f) ⁻¹' U.1) :
   (structure_sheaf R).presheaf.obj (op U) →+* (structure_sheaf S).presheaf.obj (op V) :=
-{ to_fun := λ s, ⟨structure_sheaf.comap_fun f U V hUV s.1,
-    structure_sheaf.comap_fun_is_locally_fraction f U V hUV s.1 s.2⟩,
+{ to_fun := λ s, ⟨comap_fun f U V hUV s.1, comap_fun_is_locally_fraction f U V hUV s.1 s.2⟩,
   map_one' := subtype.ext $ funext $ λ p, by
-    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
-      (sections_subring R (op U)).coe_one, pi.one_apply, ring_hom.map_one], refl },
+    { rw [subtype.coe_mk, subtype.val_eq_coe, comap_fun, (sections_subring R (op U)).coe_one,
+      pi.one_apply, ring_hom.map_one], refl },
   map_zero' := subtype.ext $ funext $ λ p, by
-    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
-      (sections_subring R (op U)).coe_zero, pi.zero_apply, ring_hom.map_zero], refl },
+    { rw [subtype.coe_mk, subtype.val_eq_coe, comap_fun, (sections_subring R (op U)).coe_zero,
+      pi.zero_apply, ring_hom.map_zero], refl },
   map_add' := λ s t, subtype.ext $ funext $ λ p, by
-    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
-      (sections_subring R (op U)).coe_add, pi.add_apply, ring_hom.map_add], refl },
+    { rw [subtype.coe_mk, subtype.val_eq_coe, comap_fun, (sections_subring R (op U)).coe_add,
+      pi.add_apply, ring_hom.map_add], refl },
   map_mul' := λ s t, subtype.ext $ funext $ λ p, by
-    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
-      (sections_subring R (op U)).coe_mul, pi.mul_apply, ring_hom.map_mul], refl }
+    { rw [subtype.coe_mk, subtype.val_eq_coe, comap_fun, (sections_subring R (op U)).coe_mul,
+      pi.mul_apply, ring_hom.map_mul], refl }
 }
 
 @[simp]
-lemma structure_sheaf.comap_apply (f : R →+* S) (U : opens (prime_spectrum.Top R))
-  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1)
+lemma comap_apply (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (prime_spectrum.comap f) ⁻¹' U.1)
   (s : (structure_sheaf R).presheaf.obj (op U)) (p : V) :
-  (structure_sheaf.comap f U V hUV s).1 p =
-  localization.local_ring_hom (comap f p.1).as_ideal _ f rfl (s.1 ⟨(comap f p.1), hUV p.2⟩ : _) :=
+  (comap f U V hUV s).1 p =
+  localization.local_ring_hom (prime_spectrum.comap f p.1).as_ideal _ f rfl
+    (s.1 ⟨(prime_spectrum.comap f p.1), hUV p.2⟩ : _) :=
 rfl
 
-lemma structure_sheaf.comap_const (f : R →+* S) (U : opens (prime_spectrum.Top R))
-  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1)
+lemma comap_const (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (prime_spectrum.comap f) ⁻¹' U.1)
   (a b : R) (hb : ∀ x : prime_spectrum R, x ∈ U → b ∈ x.as_ideal.prime_compl) :
-  structure_sheaf.comap f U V hUV (const R a b U hb) =
-  const S (f a) (f b) V (λ p hpV, hb (comap f p) (hUV hpV)) :=
+  comap f U V hUV (const R a b U hb) =
+  const S (f a) (f b) V (λ p hpV, hb (prime_spectrum.comap f p) (hUV hpV)) :=
 subtype.eq $ funext $ λ p,
 begin
-  rw [structure_sheaf.comap_apply, const_apply, const_apply],
+  rw [comap_apply, const_apply, const_apply],
   erw localization.local_ring_hom_mk',
   refl,
 end
@@ -878,22 +882,23 @@ identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure
 This is a generalization of the fact that, for fixed `U`, the comap of the identity from OO_X(U)
 to OO_X(U) is the identity.
 -/
-lemma structure_sheaf.comap_id_eq_map (U V : opens (prime_spectrum.Top R)) (iVU : V ⟶ U) :
-  structure_sheaf.comap (ring_hom.id R) U V
+lemma comap_id_eq_map (U V : opens (prime_spectrum.Top R)) (iVU : V ⟶ U) :
+  comap (ring_hom.id R) U V
     (λ p hpV, le_of_hom iVU $ by rwa prime_spectrum.comap_id) =
   (structure_sheaf R).presheaf.map iVU.op :=
 ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
 begin
-  rw structure_sheaf.comap_apply,
+  rw comap_apply,
   -- Unfortunately, we cannot use `localization.local_ring_hom_id` here, because
-  -- `comap (ring_hom.id R) p` is not *definitionally* equal to `p`. Instead, we use that we can
-  -- write `s` as a fraction `a/b` in a small neighborhood around `p`. Since
-  -- `comap (ring_hom.id R) p` equals `p`, it is also contained in the same neighborhood, hence
-  -- `s` equals `a/b` there too.
+  -- `prime_spectrum.comap (ring_hom.id R) p` is not *definitionally* equal to `p`. Instead, we use
+  -- that we can write `s` as a fraction `a/b` in a small neighborhood around `p`. Since
+  -- `prime_spectrum.comap (ring_hom.id R) p` equals `p`, it is also contained in the same
+  -- neighborhood, hence `s` equals `a/b` there too.
   obtain ⟨W, hpW, iWU, h⟩ := s.2 (iVU p),
   obtain ⟨a, b, h'⟩ := h.eq_mk',
   obtain ⟨hb₁, s_eq₁⟩ := h' ⟨p, hpW⟩,
-  obtain ⟨hb₂, s_eq₂⟩ := h' ⟨comap (ring_hom.id _) p.1, by rwa prime_spectrum.comap_id⟩,
+  obtain ⟨hb₂, s_eq₂⟩ := h' ⟨prime_spectrum.comap (ring_hom.id _) p.1,
+    by rwa prime_spectrum.comap_id⟩,
   dsimp only at s_eq₁ s_eq₂,
   erw [s_eq₂, localization.local_ring_hom_mk', ← s_eq₁, ← res_apply],
 end
@@ -903,40 +908,42 @@ The comap of the identity is the identity. In this variant of the lemma, two ope
 `V` are given as arguments, together with a proof that `U = V`. This is be useful when `U` and `V`
 are not definitionally equal.
 -/
-lemma structure_sheaf.comap_id (U V : opens (prime_spectrum.Top R)) (hUV : U = V) :
-  structure_sheaf.comap (ring_hom.id R) U V
-    (λ p hpV, by rwa [hUV, prime_spectrum.comap_id]) =
+lemma comap_id (U V : opens (prime_spectrum.Top R)) (hUV : U = V) :
+  comap (ring_hom.id R) U V (λ p hpV, by rwa [hUV, prime_spectrum.comap_id]) =
   eq_to_hom (show (structure_sheaf R).presheaf.obj (op U) = _, by rw hUV) :=
-by erw [structure_sheaf.comap_id_eq_map U V (eq_to_hom hUV.symm), eq_to_hom_op, eq_to_hom_map]
+by erw [comap_id_eq_map U V (eq_to_hom hUV.symm), eq_to_hom_op, eq_to_hom_map]
 
-@[simp] lemma structure_sheaf.comap_id' (U : opens (prime_spectrum.Top R)) :
-  structure_sheaf.comap (ring_hom.id R) U U (λ p hpU, by rwa prime_spectrum.comap_id) =
+@[simp] lemma comap_id' (U : opens (prime_spectrum.Top R)) :
+  comap (ring_hom.id R) U U (λ p hpU, by rwa prime_spectrum.comap_id) =
   ring_hom.id _ :=
-by { rw structure_sheaf.comap_id U U rfl, refl }
+by { rw comap_id U U rfl, refl }
 
-lemma structure_sheaf.comap_comp (f : R →+* S) (g : S →+* P) (U : opens (prime_spectrum.Top R))
+lemma comap_comp (f : R →+* S) (g : S →+* P) (U : opens (prime_spectrum.Top R))
   (V : opens (prime_spectrum.Top S)) (W : opens (prime_spectrum.Top P))
-  (hUV : ∀ p ∈ V, comap f p ∈ U) (hVW : ∀ p ∈ W, comap g p ∈ V) :
-  structure_sheaf.comap (g.comp f) U W (λ p hpW, hUV (comap g p) (hVW p hpW)) =
-    (structure_sheaf.comap g V W hVW).comp (structure_sheaf.comap f U V hUV) :=
+  (hUV : ∀ p ∈ V, prime_spectrum.comap f p ∈ U) (hVW : ∀ p ∈ W, prime_spectrum.comap g p ∈ V) :
+  comap (g.comp f) U W (λ p hpW, hUV (prime_spectrum.comap g p) (hVW p hpW)) =
+    (comap g V W hVW).comp (comap f U V hUV) :=
 ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
 begin
-  rw structure_sheaf.comap_apply,
-  erw localization.local_ring_hom_comp _ (comap g p.1).as_ideal,
-  -- refl works here, because `comap (g.comp f) p` is defeq to `comap f (comap g p)`
+  rw comap_apply,
+  erw localization.local_ring_hom_comp _ (prime_spectrum.comap g p.1).as_ideal,
+  -- refl works here, because `prime_spectrum.comap (g.comp f) p` is defeq to
+  -- `prime_spectrum.comap f (prime_spectrum.comap g p)`
   refl,
 end
 
 @[elementwise, reassoc] lemma to_open_comp_comap (f : R →+* S) :
-  to_open R ⊤ ≫ structure_sheaf.comap f ⊤ ⊤ (λ p hpV, trivial) =
+  to_open R ⊤ ≫ comap f ⊤ ⊤ (λ p hpV, trivial) =
   @category_theory.category_struct.comp _ _ (CommRing.of R) (CommRing.of S) _ f (to_open S ⊤) :=
 ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
 begin
-  simp_rw [comp_apply, structure_sheaf.comap_apply, subtype.val_eq_coe, to_open_apply_coe],
+  simp_rw [comp_apply, comap_apply, subtype.val_eq_coe, to_open_apply_coe],
   erw localization.local_ring_hom_to_map,
   refl,
 end
 
 end comap
 
+end structure_sheaf
+
 end algebraic_geometry