From 879da1cf04c2baa9eaa7bd2472100bc0335e5c73 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 28 Jul 2019 20:35:05 +1000 Subject: [PATCH] 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 --- src/algebraic_geometry/presheafed_space.lean | 141 ++++++++++--------- src/algebraic_geometry/stalks.lean | 20 ++- 2 files changed, 86 insertions(+), 75 deletions(-) diff --git a/src/algebraic_geometry/presheafed_space.lean b/src/algebraic_geometry/presheafed_space.lean index ea843f9da5690..d9ec637ce1bd4 100644 --- a/src/algebraic_geometry/presheafed_space.lean +++ b/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,7 +152,8 @@ end PresheafedSpace end algebraic_geometry -open algebraic_geometry +open algebraic_geometry algebraic_geometry.PresheafedSpace + variables {C} namespace category_theory @@ -150,33 +161,31 @@ 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 diff --git a/src/algebraic_geometry/stalks.lean b/src/algebraic_geometry/stalks.lean index d590305322731..59b454ffd0b38 100644 --- a/src/algebraic_geometry/stalks.lean +++ b/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