chore(category_theory/whiskering): clean up (#1613)

* chore(category_theory/whiskering): clean up

* ugh, the stalks proofs are so fragile

* fixes

* minor

* fix

* fix

Author: kim-em

src/algebraic_geometry/stalks.lean

@@ -55,11 +55,13 @@ begin
   op_induction U,
   cases U,
   simp only [colim.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
-    whisker_left.app, whisker_right.app,
+    whisker_left_app, whisker_right_app,
     assoc, id_comp, map_id, map_comp],
   dsimp,
   simp only [map_id, assoc],
   -- FIXME Why doesn't simp do this:
+  erw [category_theory.functor.map_id],
+  erw [category_theory.functor.map_id],
   erw [id_comp, id_comp],
 end
 end stalk_map

src/category_theory/monad/limits.lean

@@ -46,7 +46,7 @@ variables (D : J ⥤ algebra T) [has_limit.{v₁} (D ⋙ forget T)]
   begin
     ext1,
     dsimp,
-    simp only [limit.lift_π, γ_app, c_π, limit.cone_π, functor.const_comp, whisker_right.app,
+    simp only [limit.lift_π, γ_app, c_π, limit.cone_π, functor.const_comp, whisker_right_app,
                 nat_trans.comp_app, category.assoc],
     dsimp,
     simp only [id_comp],
@@ -75,7 +75,7 @@ def forget_creates_limits (D : J ⥤ algebra T) [has_limit.{v₁} (D ⋙ forget
       begin
         ext, dsimp,
         simp only [limit.lift_π, limit.cone_π, forget_map, id_comp, functor.const_comp,
-                    whisker_right.app, nat_trans.comp_app, category.assoc, functor.map_cone_π],
+                    whisker_right_app, nat_trans.comp_app, category.assoc, functor.map_cone_π],
         dsimp,
         rw [id_comp, ←category.assoc, ←T.map_comp],
         simp only [limit.lift_π, monad.forget_map, algebra.hom.h, functor.map_cone_π],

src/category_theory/opposites.lean

@@ -163,17 +163,17 @@ include 𝒟
 section
 variables {F G : C ⥤ D}
 
-protected definition op (α : F ⟶ G) : G.op ⟶ F.op :=
+@[simps] protected definition op (α : F ⟶ G) : G.op ⟶ F.op :=
 { app         := λ X, (α.app (unop X)).op,
   naturality' := begin tidy, erw α.naturality, refl, end }
 
-@[simp] lemma op_app (α : F ⟶ G) (X) : (nat_trans.op α).app X = (α.app (unop X)).op := rfl
+@[simp] lemma op_id (F : C ⥤ D) : nat_trans.op (𝟙 F) = 𝟙 (F.op) := rfl
 
-protected definition unop (α : F.op ⟶ G.op) : G ⟶ F :=
+@[simps] protected definition unop (α : F.op ⟶ G.op) : G ⟶ F :=
 { app         := λ X, (α.app (op X)).unop,
   naturality' := begin tidy, erw α.naturality, refl, end }
 
-@[simp] lemma unop_app (α : F.op ⟶ G.op) (X) : (nat_trans.unop α).app X = (α.app (op X)).unop := rfl
+@[simp] lemma unop_id (F : C ⥤ D) : nat_trans.unop (𝟙 F.op) = 𝟙 F := rfl
 
 end
 

src/category_theory/whiskering.lean

@@ -10,30 +10,35 @@ namespace category_theory
 universes u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄
 
 section
-variables (C : Type u₁) [𝒞 : category.{v₁} C]
-          (D : Type u₂) [𝒟 : category.{v₂} D]
-          (E : Type u₃) [ℰ : category.{v₃} E]
+variables {C : Type u₁} [𝒞 : category.{v₁} C]
+          {D : Type u₂} [𝒟 : category.{v₂} D]
+          {E : Type u₃} [ℰ : category.{v₃} E]
 include 𝒞 𝒟 ℰ
 
-def whiskering_left : (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)) :=
+@[simps] def whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : (F ⋙ G) ⟶ (F ⋙ H) :=
+{ app := λ c, α.app (F.obj c),
+  naturality' := λ X Y f, by rw [functor.comp_map, functor.comp_map, α.naturality] }
+
+@[simps] def whisker_right {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : (G ⋙ F) ⟶ (H ⋙ F) :=
+{ app := λ c, F.map (α.app c),
+  naturality' := λ X Y f, by rw [functor.comp_map, functor.comp_map, ←F.map_comp, ←F.map_comp, α.naturality] }
+
+variables (C D E)
+
+@[simps] def whiskering_left : (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)) :=
 { obj := λ F,
   { obj := λ G, F ⋙ G,
-    map := λ G H α,
-    { app := λ c, α.app (F.obj c),
-      naturality' := by intros X Y f; rw [functor.comp_map, functor.comp_map, α.naturality] } },
+    map := λ G H α, whisker_left F α },
   map := λ F G τ,
   { app := λ H,
     { app := λ c, H.map (τ.app c),
       naturality' := λ X Y f, begin dsimp, rw [←H.map_comp, ←H.map_comp, ←τ.naturality] end },
     naturality' := λ X Y f, begin ext1, dsimp, rw [f.naturality] end } }
 
-def whiskering_right : (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)) :=
+@[simps] def whiskering_right : (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)) :=
 { obj := λ H,
   { obj := λ F, F ⋙ H,
-    map := λ _ _ α,
-    { app := λ c, H.map (α.app c),
-      naturality' := by intros X Y f;
-        rw [functor.comp_map, functor.comp_map, ←H.map_comp, ←H.map_comp, α.naturality] } },
+    map := λ _ _ α, whisker_right α H },
   map := λ G H τ,
   { app := λ F,
     { app := λ c, τ.app (F.obj c),
@@ -42,38 +47,6 @@ def whiskering_right : (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)) :=
 
 variables {C} {D} {E}
 
-def whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : (F ⋙ G) ⟶ (F ⋙ H) :=
-((whiskering_left C D E).obj F).map α
-
-@[simp] lemma whiskering_left_obj_obj (F : C ⥤ D) (G : D ⥤ E) :
-  ((whiskering_left C D E).obj F).obj G = F ⋙ G :=
-rfl
-@[simp] lemma whiskering_left_obj_map (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) :
-  ((whiskering_left C D E).obj F).map α = whisker_left F α :=
-rfl
-@[simp] lemma whiskering_left_map_app_app {F G : C ⥤ D} (τ : F ⟶ G) (H : D ⥤ E) (c) :
-  (((whiskering_left C D E).map τ).app H).app c = H.map (τ.app c) :=
-rfl
-@[simp] lemma whisker_left.app (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) (X : C) :
-  (whisker_left F α).app X = α.app (F.obj X) :=
-rfl
-
-def whisker_right {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : (G ⋙ F) ⟶ (H ⋙ F) :=
-((whiskering_right C D E).obj F).map α
-
-@[simp] lemma whiskering_right_obj_obj (G : C ⥤ D) (F : D ⥤ E) :
-  ((whiskering_right C D E).obj F).obj G = G ⋙ F :=
-rfl
-@[simp] lemma whiskering_right_obj_map {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) :
-  ((whiskering_right C D E).obj F).map α = whisker_right α F :=
-rfl
-@[simp] lemma whiskering_right_map_app_app (F : C ⥤ D) {G H : D ⥤ E} (τ : G ⟶ H) (c) :
-  (((whiskering_right C D E).map τ).app F).app c = τ.app (F.obj c) :=
-rfl
-@[simp] lemma whisker_right.app {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) (X : C) :
-   (whisker_right α F).app X = F.map (α.app X) :=
-rfl
-
 @[simp] lemma whisker_left_id (F : C ⥤ D) {G : D ⥤ E} :
   whisker_left F (nat_trans.id G) = nat_trans.id (F.comp G) :=
 rfl
@@ -166,11 +139,7 @@ omit 𝒟
 lemma triangle (F : A ⥤ B) (G : B ⥤ C) :
   (associator F (𝟭 B) G).hom ≫ (whisker_left F (left_unitor G).hom) =
     (whisker_right (right_unitor F).hom G) :=
-begin
-  ext1,
-  dsimp [associator, left_unitor, right_unitor],
-  simp
-end
+by { ext1, dsimp, simp }
 
 variables {E : Type u₅} [ℰ : category.{v₅} E]
 include 𝒟 ℰ
@@ -180,11 +149,7 @@ variables (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) (K : D ⥤ E)
 lemma pentagon :
   (whisker_right (associator F G H).hom K) ≫ (associator F (G ⋙ H) K).hom ≫ (whisker_left F (associator G H K).hom) =
     ((associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom) :=
-begin
-  ext1,
-  dsimp [associator],
-  simp,
-end
+by { ext1, dsimp, simp }
 
 end functor
 

src/topology/sheaves/stalks.lean

@@ -74,12 +74,15 @@ begin
   ext1,
   tactic.op_induction',
   cases j, cases j_val,
-  rw [colim.ι_map_assoc, colim.ι_map, colimit.ι_pre, whisker_left.app, whisker_right.app,
+  rw [colim.ι_map_assoc, colim.ι_map, colimit.ι_pre, whisker_left_app, whisker_right_app,
        pushforward.id_hom_app, eq_to_hom_map, eq_to_hom_refl],
   dsimp,
-  rw [category_theory.functor.map_id]
+  -- FIXME A simp lemma which unfortunately doesn't fire:
+  erw [category_theory.functor.map_id],
 end
 
+-- This proof is sadly not at all robust:
+-- having to use `erw` at all is a bad sign.
 @[simp] lemma comp (ℱ : X.presheaf C) (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
   ℱ.stalk_pushforward C (f ≫ g) x =
   ((f _* ℱ).stalk_pushforward C g (f x)) ≫ (ℱ.stalk_pushforward C f x) :=
@@ -89,14 +92,13 @@ begin
   op_induction U,
   cases U,
   cases U_val,
-  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
-             whisker_right.app, category.assoc],
-  dsimp,
-  simp only [category.id_comp, category_theory.functor.map_id],
-  -- FIXME A simp lemma which unfortunately doesn't fire:
-  rw [category_theory.functor.map_id],
+  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc,
+             whisker_right_app, category.assoc],
   dsimp,
-  simp,
+  -- FIXME: Some of these are simp lemmas, but don't fire successfully:
+  erw [category_theory.functor.map_id, category.id_comp, category.id_comp, category.id_comp,
+       colimit.ι_pre, colimit.ι_pre],
+  refl,
 end
 
 end stalk_pushforward