refactor(algebraic_geometry/*): rename structure sheaf to `Spec.struc…

…ture_sheaf` (#12785) Following [this Zulip message](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rename.20.60structure_sheaf.60.20to.20.60Spec.2Estructure_sheaf.60/near/275649595), this pr renames `structure_sheaf` to `Spec.structure_sheaf`
leanprover-community · Mar 23, 2022 · 84a438e · 84a438e
1 parent 16fb8e2
commit 84a438e
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 3 deletions.
diff --git a/src/algebraic_geometry/AffineScheme.lean b/src/algebraic_geometry/AffineScheme.lean
@@ -37,6 +37,8 @@ universe u
 
 namespace algebraic_geometry
 
+open Spec (structure_sheaf)
+
 /-- The category of affine schemes -/
 def AffineScheme := Scheme.Spec.ess_image
 

diff --git a/src/algebraic_geometry/Gamma_Spec_adjunction.lean b/src/algebraic_geometry/Gamma_Spec_adjunction.lean
@@ -38,7 +38,7 @@ open prime_spectrum
 namespace algebraic_geometry
 open opposite
 open category_theory
-open structure_sheaf
+open structure_sheaf Spec (structure_sheaf)
 open topological_space
 open algebraic_geometry.LocallyRingedSpace
 open Top.presheaf

diff --git a/src/algebraic_geometry/Spec.lean b/src/algebraic_geometry/Spec.lean
@@ -38,7 +38,7 @@ universes u v
 namespace algebraic_geometry
 open opposite
 open category_theory
-open structure_sheaf
+open structure_sheaf Spec (structure_sheaf)
 
 /--
 The spectrum of a commutative ring, as a topological space.

diff --git a/src/algebraic_geometry/structure_sheaf.lean b/src/algebraic_geometry/structure_sheaf.lean
@@ -257,13 +257,14 @@ 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 (prime_spectrum.Top R) :=
+def Spec.structure_sheaf : sheaf CommRing (prime_spectrum.Top R) :=
 ⟨structure_presheaf_in_CommRing R,
   -- We check the sheaf condition under `forget CommRing`.
   (is_sheaf_iff_is_sheaf_comp _ _).mpr
     (is_sheaf_of_iso (structure_presheaf_comp_forget R).symm
       (structure_sheaf_in_Type R).property)⟩
 
+open Spec (structure_sheaf)
 
 namespace structure_sheaf