feat(presheaves/stalks): stalks of presheafs, and presheafed spaces w…

…ith extra structure on stalks (#1018)

* feat(category_theory/colimits): missing simp lemmas

* feat(category_theory): functor.map_nat_iso

* define `functor.map_nat_iso`, and relate to whiskering
* rename `functor.on_iso` to `functor.map_iso`
* add some missing lemmas about whiskering

* fix(category_theory): presheaves, unbundled and bundled, and pushforwards

* restoring `(opens X)ᵒᵖ`

* various changes from working on stalks

* rename `nbhds` to `open_nhds`

* fix introduced typo

* typo

* compactify a proof

* rename `presheaf` to `presheaf_on_space`

* fix(category_theory): turn `has_limits` classes into structures

* naming instances to avoid collisions

* breaking up instances.topological_spaces

* fixing all the other pi-type typclasses

* fix import

* oops

* fix import

* feat(category_theory): stalks of sheaves

* renaming

* fixes after rebase

* nothing

* yay, got rid of the @s

* attempting a very general version of structured stalks

* missed one

* typo

* WIP

* oops

* the presheaf of continuous functions to ℂ

* restoring eq_to_hom simp lemmas

* removing unnecessary simp lemma

* remove another superfluous lemma

* removing the nat_trans and vcomp notations; use \hom and \gg

* a simpler proposal

* getting rid of vcomp

* fix

* splitting files

* renaming

* probably working again?

* update notation

* remove old lemma

* fix

* comment out unfinished stuff

* cleanup

* use iso_whisker_right instead of map_nat_iso

* proofs magically got easier?

* improve some proofs

* moving instances

* remove crap

* tidy

* minimise imports

* chore(travis): disable the check for minimal imports

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: semorrison <scott@tqft.net>

* writing `op_induction` tactic, and improving proofs

* squeeze_simping

* cleanup

* rearranging

* cleanup

* cleaning up

* cleaning up

* move

* cleaning up

* structured stalks

* comment

* structured stalks

* more simp lemmas

* formatting

* Update src/category_theory/instances/Top/presheaf_of_functions.lean

Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com>

* fixes in response to review

* tidy regressions... :-(

* oops

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/category_theory/instances/TopCommRing/basic.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* def to lemma

* remove useless lemma

* explicit associator

* broken

* can't get proofs to work...

* remove superfluous imports

* missing headers

* change example

* reverting changes to tidy

* remove presheaf_Z, as it doesn't work at the moment

* fixes

* fixes

* fix

* postponing stuff on structured stalks for a later PR

* coercions

* getting rid of all the `erw`

* omitting some proofs

* deleting more proofs

* convert begin ... end to by

* local

src/algebraic_geometry/presheafed_space.lean

@@ -9,10 +9,13 @@ open category_theory
 open category_theory.instances
 open category_theory.instances.Top
 open topological_space
+open opposite
 
 variables (C : Type u) [𝒞 : category.{v+1} C]
 include 𝒞
 
+local attribute [tidy] tactic.op_induction'
+
 namespace algebraic_geometry
 
 structure PresheafedSpace :=
@@ -23,13 +26,17 @@ variables {C}
 
 namespace PresheafedSpace
 
-instance : has_coe_to_sort (PresheafedSpace.{v} C) :=
-{ S := Type v, coe := λ F, F.to_Top.α }
+instance coe_to_Top : has_coe (PresheafedSpace.{v} C) Top :=
+{ coe := λ X, X.to_Top }
+
+@[simp] lemma as_coe (X : PresheafedSpace.{v} C) : X.to_Top = (X : Top.{v}) := rfl
+@[simp] lemma mk_coe (to_Top) (𝒪) : (({ to_Top := to_Top, 𝒪 := 𝒪 } :
+  PresheafedSpace.{v} C) : Top.{v}) = to_Top := rfl
 
 instance (X : PresheafedSpace.{v} C) : topological_space X := X.to_Top.str
 
 structure hom (X Y : PresheafedSpace.{v} C) :=
-(f : X.to_Top ⟶ Y.to_Top)
+(f : (X : Top.{v}) ⟶ (Y : Top.{v}))
 (c : Y.𝒪 ⟶ f _* X.𝒪)
 
 @[extensionality] lemma ext {X Y : PresheafedSpace.{v} C} (α β : hom X Y)
@@ -43,7 +50,7 @@ end
 .
 
 def id (X : PresheafedSpace.{v} C) : hom X X :=
-{ f := 𝟙 X.to_Top,
+{ f := 𝟙 (X : Top.{v}),
   c := ((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _) }
 
 def comp (X Y Z : PresheafedSpace.{v} C) (α : hom X Y) (β : hom Y Z) : hom X Z :=
@@ -58,43 +65,7 @@ local attribute [simp] id comp presheaf.pushforward
 instance category_of_PresheafedSpaces : category (PresheafedSpace.{v} C) :=
 { hom  := hom,
   id   := id,
-  comp := comp,
-  -- I'm still grumpy about these proofs.
-  -- The obstacle here is the mysterious need to use `erw` for some `simp` lemmas.
-  -- If we could avoid that, locally adding `op_induction` to `tidy` would discharge these.
-  comp_id' := λ X Y f,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp, },
-    { dsimp, simp }
-  end,
-  id_comp' := λ X Y f,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp only [category.assoc],
-      -- This should be done by `simp`, but unfortunately isn't.
-      erw [category_theory.functor.map_id],
-      simp, },
-    { simp }
-  end,
-  assoc' := λ W X Y Z f g h,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp only [category.assoc],
-      -- This should be done by `simp`, but unfortunately isn't.
-      erw [category_theory.functor.map_id],
-      simp, },
-    { refl }
-  end }
+  comp := comp }
 end
 .
 
@@ -103,25 +74,28 @@ variables {C}
 instance {X Y : PresheafedSpace.{v} C} : has_coe (X ⟶ Y) (X.to_Top ⟶ Y.to_Top) :=
 { coe := λ α, α.f }
 
-@[simp] lemma id_f (X : PresheafedSpace.{v} C) : ((𝟙 X) : X ⟶ X).f = 𝟙 X.to_Top := rfl
-@[simp] lemma comp_f {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  (α ≫ β).f = α.f ≫ β.f :=
-rfl
+@[simp] lemma hom_mk_coe {X Y : PresheafedSpace.{v} C} (f) (c) :
+  (({ f := f, c := c } : X ⟶ Y) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
+@[simp] lemma f_as_coe {X Y : PresheafedSpace.{v} C} (α : X ⟶ Y) :
+  α.f = (α : (X : Top.{v}) ⟶ (Y : Top.{v})) := rfl
+@[simp] lemma id_coe (X : PresheafedSpace.{v} C) :
+  (((𝟙 X) : X ⟶ X) : (X : Top.{v}) ⟶ X) = 𝟙 (X : Top.{v}) := rfl
 @[simp] lemma comp_coe {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  ((α ≫ β : X ⟶ Z) : X.to_Top ⟶ Z.to_Top) = (α : X.to_Top ⟶ Y.to_Top) ≫ (β : Y.to_Top ⟶ Z.to_Top) :=
-rfl
+  ((α ≫ β : X ⟶ Z) : (X : Top.{v}) ⟶ Z) = (α : (X : Top.{v}) ⟶ Y) ≫ (β : Y ⟶ Z) := rfl
 
--- We don't mark these as simp lemmas, because the innards are pretty unsightly.
 lemma id_c (X : PresheafedSpace.{v} C) :
   ((𝟙 X) : X ⟶ X).c =
-  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _)) :=
-rfl
+  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _)) := rfl
 lemma comp_c {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) :=
-rfl
+  (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) := rfl
+@[simp] lemma id_c_app (X : PresheafedSpace.{v} C) (U) :
+  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by tidy) :=
+by { simp only [id_c], tidy }
+@[simp] lemma comp_c_app {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
+  (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.f)).obj (unop U))) := rfl
 
 def forget : PresheafedSpace.{v} C ⥤ Top :=
-{ obj := λ X, X.to_Top,
+{ obj := λ X, (X : Top.{v}),
   map := λ X Y f, f }
 
 end PresheafedSpace
@@ -145,11 +119,11 @@ def map_presheaf (F : C ⥤ D) : PresheafedSpace.{v} C ⥤ PresheafedSpace.{v} D
   map := λ X Y f, { f := f.f, c := whisker_right f.c F } }.
 
 @[simp] lemma map_presheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
-  (F.map_presheaf.obj X).to_Top = X.to_Top := rfl
+  ((F.map_presheaf.obj X) : Top.{v}) = (X : Top.{v}) := rfl
 @[simp] lemma map_presheaf_obj_𝒪 (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
   (F.map_presheaf.obj X).𝒪 = X.𝒪 ⋙ F := rfl
 @[simp] lemma map_presheaf_map_f (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
-  (F.map_presheaf.map f).f = f := rfl
+  ((F.map_presheaf.map f) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
 @[simp] lemma map_presheaf_map_c (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
   (F.map_presheaf.map f).c = whisker_right f.c F := rfl
 
@@ -161,21 +135,7 @@ def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_preshe
 { app := λ X,
   { f := 𝟙 _,
     c := whisker_left X.𝒪 α ≫ ((functor.left_unitor _).inv) ≫
-           (whisker_right (nat_trans.op (opens.map_id _).hom) _) },
-  naturality' := λ X Y f,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp only [functor.map_id, category.id_comp, category.comp_id, category.assoc],
-      -- This should be done by `simp`, but unfortunately isn't.
-      erw category_theory.functor.map_id,
-      erw category_theory.functor.map_id,
-      simp only [category.comp_id],
-      exact (α.naturality _).symm, },
-    { refl, }
-  end }.
+           (whisker_right (nat_trans.op (opens.map_id _).hom) _) } }.
 
 end nat_trans
 

src/algebraic_geometry/stalks.lean

@@ -0,0 +1,61 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+import algebraic_geometry.presheafed_space
+import category_theory.instances.Top.stalks
+
+universes v u v' u'
+
+open category_theory
+open category_theory.instances
+open category_theory.limits
+open algebraic_geometry
+open topological_space
+
+variables {C : Type u} [𝒞 : category.{v+1} C] [has_colimits.{v} C]
+include 𝒞
+
+local attribute [tidy] tactic.op_induction'
+
+open category_theory.instances.Top.presheaf
+
+namespace algebraic_geometry.PresheafedSpace
+
+def stalk (X : PresheafedSpace.{v} C) (x : X) : C := X.𝒪.stalk x
+
+def stalk_map {X Y : PresheafedSpace.{v} C} (α : X ⟶ Y) (x : X) : Y.stalk (α x) ⟶ X.stalk x :=
+(stalk_functor C (α x)).map (α.c) ≫ X.𝒪.stalk_pushforward C α x
+
+namespace stalk_map
+
+@[simp] lemma id (X : PresheafedSpace.{v} C) (x : X) : stalk_map (𝟙 X) x = 𝟙 (X.stalk x) :=
+begin
+  dsimp [stalk_map],
+  simp only [stalk_pushforward.id],
+  rw [←category_theory.functor.map_comp],
+  convert (stalk_functor C x).map_id X.𝒪,
+  tidy,
+end
+.
+
+@[simp] lemma comp {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : X) :
+  stalk_map (α ≫ β) x =
+    (stalk_map β (α x) : Z.stalk (β (α x)) ⟶ Y.stalk (α x)) ≫
+    (stalk_map α x : Y.stalk (α x) ⟶ X.stalk x) :=
+begin
+  dsimp [stalk, stalk_map, stalk_functor, stalk_pushforward, comp_c],
+  ext U,
+  op_induction U,
+  cases U,
+  cases U_val,
+  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
+    whisker_left.app, whisker_right.app,
+    functor.map_comp, category.assoc, category_theory.functor.map_id, category.id_comp],
+  dsimp,
+  simp only [category_theory.functor.map_id],
+  -- FIXME Why doesn't simp do this:
+  erw [category.id_comp, category.id_comp],
+end
+end stalk_map
+
+end algebraic_geometry.PresheafedSpace

src/category_theory/functor_category.lean

@@ -81,11 +81,13 @@ protected def flip (F : C ⥤ (D ⥤ E)) : D ⥤ (C ⥤ E) :=
     map_id' := λ X, begin rw category_theory.functor.map_id, refl end,
     map_comp' := λ X Y Z f g, by rw [map_comp, ←comp_app] },
   map := λ c c' f,
-  { app := λ j, (F.obj j).map f,
-    naturality' := λ X Y g, by dsimp; rw ←naturality } }.
+  { app := λ j, (F.obj j).map f } }.
 
+@[simp] lemma flip_obj_obj (F : C ⥤ (D ⥤ E)) (c) (d) : (F.flip.obj d).obj c = (F.obj c).obj d := rfl
 @[simp] lemma flip_obj_map (F : C ⥤ (D ⥤ E)) {c c' : C} (f : c ⟶ c') (d : D) :
-  ((F.flip).obj d).map f = (F.map f).app d := rfl
+  (F.flip.obj d).map f = (F.map f).app d := rfl
+@[simp] lemma flip_map_app (F : C ⥤ (D ⥤ E)) {d d' : D} (f : d ⟶ d') (c : C) :
+  (F.flip.map f).app c = (F.obj c).map f := rfl
 
 end functor
 

src/category_theory/instances/Top/basic.lean

@@ -21,6 +21,8 @@ instance topological_space_unbundled (x : Top) : topological_space x := x.str
 namespace Top
 instance concrete_category_continuous : concrete_category @continuous := ⟨@continuous_id, @continuous.comp⟩
 
+abbreviation forget : Top ⥤ Type u := category_theory.forget
+
 def of (X : Type u) [topological_space X] : Top := ⟨X, by apply_instance⟩
 
 def discrete : Type u ⥤ Top.{u} :=

src/category_theory/instances/Top/open_nhds.lean

@@ -27,6 +27,8 @@ def map (x : X) : open_nhds (f x) ⥤ open_nhds x :=
 { obj := λ U, ⟨(opens.map f).obj U.1, by tidy⟩,
   map := λ U V i, (opens.map f).map i }
 
+@[simp] lemma map_obj (x : X) (U) (q) : (map f x).obj ⟨U, q⟩ = ⟨(opens.map f).obj U, by tidy⟩ :=
+rfl
 @[simp] lemma map_id_obj' (x : X) (U) (p) (q) : (map (𝟙 X) x).obj ⟨⟨U, p⟩, q⟩ = ⟨⟨U, p⟩, q⟩ :=
 rfl
 @[simp] lemma map_id_obj (x : X) (U) : (map (𝟙 X) x).obj U = U :=

src/category_theory/instances/Top/opens.lean

@@ -36,6 +36,9 @@ def map (f : X ⟶ Y) : opens Y ⥤ opens X :=
 { obj := λ U, ⟨ f.val ⁻¹' U.val, f.property _ U.property ⟩,
   map := λ U V i, ⟨ ⟨ λ a b, i.down.down b ⟩ ⟩ }.
 
+@[simp] lemma map_obj (f : X ⟶ Y) (U) (p) : (map f).obj ⟨U, p⟩ = ⟨ f.val ⁻¹' U, f.property _ p ⟩ :=
+rfl
+
 @[simp] lemma map_id_obj' (U) (p) : (map (𝟙 X)).obj ⟨U, p⟩ = ⟨U, p⟩ :=
 rfl
 

src/category_theory/instances/Top/presheaf.lean

@@ -28,7 +28,7 @@ variables {C}
 def pushforward {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf C :=
 (opens.map f).op ⋙ ℱ
 
-infix `_*`: 80 := pushforward
+infix ` _* `: 80 := pushforward
 
 def pushforward_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf C) :
   f _* ℱ ≅ g _* ℱ :=
@@ -47,14 +47,10 @@ def id : (𝟙 X) _* ℱ ≅ ℱ :=
   (id ℱ).hom.app (op ⟨U, p⟩) = ℱ.map (𝟙 (op ⟨U, p⟩)) :=
 by { dsimp [id], simp, }
 
+local attribute [tidy] tactic.op_induction'
+
 @[simp] lemma id_hom_app (U) :
-  (id ℱ).hom.app U = ℱ.map (eq_to_hom (opens.op_map_id_obj U)) :=
-begin
-  op_induction U,
-  cases U,
-  simp,
-  apply category_theory.functor.map_id,
-end
+  (id ℱ).hom.app U = ℱ.map (eq_to_hom (opens.op_map_id_obj U)) := by tidy
 
 @[simp] lemma id_inv_app' (U) (p) : (id ℱ).inv.app (op ⟨U, p⟩) = ℱ.map (𝟙 (op ⟨U, p⟩)) :=
 by { dsimp [id], simp, }
@@ -65,13 +61,13 @@ iso_whisker_right (nat_iso.op (opens.map_comp f g).symm) ℱ
 @[simp] lemma comp_hom_app {Y Z : Top.{v}} (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (comp ℱ f g).hom.app U = 𝟙 _ :=
 begin
   dsimp [pushforward, comp],
-  erw category_theory.functor.map_id, -- FIXME simp should do this
+  tidy,
 end
 
 @[simp] lemma comp_inv_app {Y Z : Top.{v}} (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (comp ℱ f g).inv.app U = 𝟙 _ :=
 begin
   dsimp [pushforward, comp],
-  erw category_theory.functor.map_id,
+  tidy,
 end
 
 end pushforward

src/category_theory/instances/Top/presheaf_of_functions.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
 import category_theory.instances.Top.presheaf
 import category_theory.instances.TopCommRing.basic
 import category_theory.yoneda
@@ -63,9 +66,6 @@ def presheaf_to_TopCommRing (T : TopCommRing.{v}) :
   X.presheaf CommRing.{v} :=
 (opens.to_Top X).op ⋙ (CommRing_yoneda.obj T)
 
-noncomputable def presheaf_ℚ (Y : Top) : Y.presheaf CommRing :=
-presheaf_to_TopCommRing Y (TopCommRing.of ℚ)
-
 noncomputable def presheaf_ℝ (Y : Top) : Y.presheaf CommRing :=
 presheaf_to_TopCommRing Y (TopCommRing.of ℝ)