fix(algebraic_geometry/presheafedspace): fix lame proofs (#1273)

* fix(algebraic_geometry/presheafedspace): fix lame proofs

* fix

* Update src/algebraic_geometry/presheafed_space.lean

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

src/algebraic_geometry/presheafed_space.lean

@@ -3,12 +3,23 @@
 -- Authors: Scott Morrison
 import topology.Top.presheaf
 
+/-!
+# Presheafed spaces
+
+Introduces the category of topological spaces equipped with a presheaf (taking values in an
+arbitrary target category `C`.)
+
+We further describe how to apply functors and natural transformations to the values of the
+presheaves.
+-/
+
 universes v u
 
 open category_theory
 open Top
 open topological_space
 open opposite
+open category_theory.category category_theory.functor
 
 variables (C : Type u) [𝒞 : category.{v+1} C]
 include 𝒞
@@ -17,6 +28,7 @@ local attribute [tidy] tactic.op_induction'
 
 namespace algebraic_geometry
 
+/-- A `PresheafedSpace C` is a topological space equipped with a presheaf of `C`s. -/
 structure PresheafedSpace :=
 (to_Top : Top.{v})
 (𝒪 : to_Top.presheaf C)
@@ -34,6 +46,9 @@ instance coe_to_Top : has_coe (PresheafedSpace.{v} C) Top :=
 
 instance (X : PresheafedSpace.{v} C) : topological_space X := X.to_Top.str
 
+/-- A morphism between presheafed spaces `X` and `Y` consists of a continuous map
+    `f` between the underlying topological spaces, and a (notice contravariant!) map
+    from the presheaf on `Y` to the pushforward of the presheaf on `X` via `f`. -/
 structure hom (X Y : PresheafedSpace.{v} C) :=
 (f : (X : Top.{v}) ⟶ (Y : Top.{v}))
 (c : Y.𝒪 ⟶ f _* X.𝒪)
@@ -61,44 +76,36 @@ variables (C)
 section
 local attribute [simp] id comp presheaf.pushforward
 
-/- Ihis proof is filled in by the `tidy` hole command and modified for performance.
-   It should not remain like this. -/
+/- The proofs below can be done by `tidy`, but it is too slow,
+   and we don't have a tactic caching mechanism. -/
+/-- The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map
+    from the presheaf on the target to the pushforward of the presheaf on the source. -/
 instance category_of_PresheafedSpaces : category (PresheafedSpace.{v} C) :=
 { hom := hom,
   id := id,
   comp := comp,
-  id_comp' :=
+  id_comp' := λ X Y f,
   begin
-    intros X Y f,
-    dsimp at *,
-    tactic.ext1 [] {new_goals := tactic.new_goals.all},
-    work_on_goal 0 { simp only [category_theory.category.id_comp] },
-    dsimp at *,
-    ext1,
-    dsimp at *,
-    simp only [category.id_comp, category.assoc],
-    tactic.op_induction',
-    cases X_1,
-    dsimp at *,
-    simp only [category_theory.category.comp_id, category_theory.functor.map_id]
+    ext1, swap,
+    { dsimp, simp only [id_comp] },
+    { ext1 U,
+      op_induction,
+      cases U,
+      dsimp,
+      simp only [comp_id, map_id] },
   end,
-  comp_id' :=
+  comp_id' := λ X Y f,
   begin
-    intros X Y f,
-    dsimp at *,
-    tactic.ext1 [] {new_goals := tactic.new_goals.all},
-    work_on_goal 0 { simp only [category_theory.category.comp_id] },
-    dsimp at *,
-    ext1,
-    dsimp at *,
-    tactic.op_induction',
-    cases X_1,
-    dsimp at *,
-    simp
+    ext1, swap,
+    { dsimp, simp only [comp_id] },
+    { ext1 U,
+      op_induction,
+      cases U,
+      dsimp,
+      simp only [comp_id, id_comp, map_id] }
   end,
-  assoc' :=
+  assoc' := λ W X Y Z f g h,
   begin
-    intros W X Y Z f g h,
     simp only [true_and, presheaf.pushforward, id, comp, whisker_left_twice, whisker_left_comp,
                heq_iff_eq, category.assoc],
     split; refl
@@ -124,16 +131,19 @@ 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
 
-lemma comp_c {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) := rfl
+-- Implementation note: this harmless looking lemma causes deterministic timeouts,
+-- but happily we can survive without it.
+-- lemma comp_c {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
+--   (α ≫ β).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 }
+  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { op_induction U, cases U, refl }) :=
+by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
 
 @[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
 
+/-- The forgetful functor from `PresheafedSpace` to `Top`. -/
 def forget : PresheafedSpace.{v} C ⥤ Top :=
 { obj := λ X, (X : Top.{v}),
   map := λ X Y f, f }
@@ -142,41 +152,40 @@ end PresheafedSpace
 
 end algebraic_geometry
 
-open algebraic_geometry
+open algebraic_geometry algebraic_geometry.PresheafedSpace
+
 variables {C}
 
 namespace category_theory
 
 variables {D : Type u} [𝒟 : category.{v+1} D]
 include 𝒟
 
-local attribute [simp] PresheafedSpace.id_c PresheafedSpace.comp_c presheaf.pushforward
+local attribute [simp] presheaf.pushforward
 
 namespace functor
 
-/- Ihis proof is filled in by the `tidy` hole command and modified for performance.
-   It should not remain like this. -/
+/-- We can apply a functor `F : C ⥤ D` to the values of the presheaf in any `PresheafedSpace C`,
+    giving a functor `PresheafedSpace C ⥤ PresheafedSpace D` -/
+/- The proofs below can be done by `tidy`, but it is too slow,
+   and we don't have a tactic caching mechanism. -/
 def map_presheaf (F : C ⥤ D) : PresheafedSpace.{v} C ⥤ PresheafedSpace.{v} D :=
 { obj := λ X, { to_Top := X.to_Top, 𝒪 := X.𝒪 ⋙ F },
   map := λ X Y f, { f := f.f, c := whisker_right f.c F },
-  map_id' :=
+  map_id' := λ X,
   begin
-    intros X,
-    dsimp at *,
-    simp only [presheaf.pushforward, whisker_right_twice, whisker_right_comp],
-    tactic.ext1 [] {new_goals := tactic.new_goals.all},
-    work_on_goal 0 { refl },
-    dsimp at *,
-    ext1,
-    dsimp at *,
-    simp only [category_theory.category.comp_id, topological_space.opens.map_id_obj,
-               category_theory.category.id_comp, category_theory.functor.map_id]
+    ext1, swap,
+    { refl },
+    { ext1,
+      dsimp,
+      simp only [presheaf.pushforward, eq_to_hom_map, map_id, comp_id, id_c_app],
+      refl }
   end,
-  map_comp' :=
+  map_comp' := λ X Y Z f g,
   begin
-    intros X Y Z f g,
-    simp only [PresheafedSpace.comp_c, presheaf.pushforward, whisker_right_comp],
-    refl
+    ext1, swap,
+    { refl, },
+    { ext, dsimp, simp only [comp_id, assoc, map_comp, map_id], },
   end }
 
 @[simp] lemma map_presheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
@@ -192,30 +201,26 @@ end functor
 
 namespace nat_trans
 
-/- Ihis proof is filled in by the `tidy` hole command and modified for performance.
-   It should not remain like this. -/
+/- The proofs below can be done by `tidy`, but it is too slow,
+   and we don't have a tactic caching mechanism. -/
 def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_presheaf :=
 { app := λ X,
   { f := 𝟙 _,
     c := whisker_left X.𝒪 α ≫ ((functor.left_unitor _).inv) ≫
            (whisker_right (nat_trans.op (opens.map_id _).hom) _) },
-  naturality' :=
+  naturality' := λ X Y f,
   begin
-    intros X Y f,
-    dsimp at *,
-    tactic.ext1 [] {new_goals := tactic.new_goals.all},
-    work_on_goal 0 { refl },
-    dsimp at *,
-    ext1,
-    dsimp at *,
-    simp at *,
-    tactic.op_induction',
-    cases X_1,
-    dsimp at *,
-    simp at *
+    ext1, swap,
+    { refl },
+    { ext1 U,
+      op_induction,
+      cases U,
+      dsimp,
+      simp only [comp_id, assoc, map_id, nat_trans.naturality] }
   end }
 
-
+-- TODO Assemble the last two constructions into a functor
+--   `(C ⥤ D) ⥤ (PresheafedSpace C ⥤ PresheafedSpace D)`
 end nat_trans
 
 end category_theory

src/algebraic_geometry/stalks.lean

@@ -4,10 +4,17 @@
 import algebraic_geometry.presheafed_space
 import topology.Top.stalks
 
+/-!
+# Stalks for presheaved spaces
+
+This file lifts constructions of stalks and pushforwards of stalks to work with
+the category of presheafed spaces.
+-/
+
 universes v u v' u'
 
 open category_theory
-open category_theory.limits
+open category_theory.limits category_theory.category category_theory.functor
 open algebraic_geometry
 open topological_space
 
@@ -31,7 +38,7 @@ namespace stalk_map
 begin
   dsimp [stalk_map],
   simp only [stalk_pushforward.id],
-  rw [←category_theory.functor.map_comp],
+  rw [←map_comp],
   convert (stalk_functor C x).map_id X.𝒪,
   tidy,
 end
@@ -42,18 +49,17 @@ end
     (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],
+  dsimp [stalk_map, stalk_functor, stalk_pushforward],
   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],
+    assoc, id_comp, map_id, map_comp],
   dsimp,
-  simp only [category_theory.functor.map_id],
+  simp only [map_id, assoc],
   -- FIXME Why doesn't simp do this:
-  erw [category.id_comp, category.id_comp],
+  erw [id_comp, id_comp],
 end
 end stalk_map