fix(category_theory/adjunctions): fix deterministic timeouts (#1586)

src/category_theory/adjunction/basic.lean

@@ -134,8 +134,8 @@ end core_hom_equiv
 structure core_unit_counit (F : C ⥤ D) (G : D ⥤ C) :=
 (unit : 𝟭 C ⟶ F.comp G)
 (counit : G.comp F ⟶ 𝟭 D)
-(left_triangle' : whisker_right unit F ≫ whisker_left F counit = nat_trans.id _ . obviously)
-(right_triangle' : whisker_left G unit ≫ whisker_right counit G = nat_trans.id _ . obviously)
+(left_triangle' : whisker_right unit F ≫ (functor.associator F G F).hom ≫ whisker_left F counit = nat_trans.id (𝟭 C ⋙ F) . obviously)
+(right_triangle' : whisker_left G unit ≫ (functor.associator G F G).inv ≫ whisker_right counit G = nat_trans.id (G ⋙ 𝟭 C) . obviously)
 
 namespace core_unit_counit
 
@@ -176,13 +176,19 @@ def mk_of_unit_counit (adj : core_unit_counit F G) : F ⊣ G :=
       change F.map (_ ≫ _) ≫ _ = _,
       rw [F.map_comp, assoc, ←functor.comp_map, adj.counit.naturality, ←assoc],
       convert id_comp _ f,
-      exact congr_arg (λ t : nat_trans _ _, t.app _) adj.left_triangle
+      have t := congr_arg (λ t : nat_trans _ _, t.app _) adj.left_triangle,
+      dsimp at t,
+      simp only [id_comp] at t,
+      exact t,
     end,
     right_inv := λ g, begin
       change _ ≫ G.map (_ ≫ _) = _,
       rw [G.map_comp, ←assoc, ←functor.comp_map, ←adj.unit.naturality, assoc],
       convert comp_id _ g,
-      exact congr_arg (λ t : nat_trans _ _, t.app _) adj.right_triangle
+      have t := congr_arg (λ t : nat_trans _ _, t.app _) adj.right_triangle,
+      dsimp at t,
+      simp only [id_comp] at t,
+      exact t,
   end },
   .. adj }
 
@@ -281,8 +287,9 @@ open adjunction
 namespace equivalence
 
 def to_adjunction (e : C ≌ D) : e.functor ⊣ e.inverse :=
-mk_of_unit_counit ⟨e.unit, e.counit, by { ext, exact e.functor_unit_comp X },
-  by { ext, exact e.unit_inverse_comp X }⟩
+mk_of_unit_counit ⟨e.unit, e.counit,
+  by { ext, dsimp, simp only [id_comp], exact e.functor_unit_comp X, },
+  by { ext, dsimp, simp only [id_comp], exact e.unit_inverse_comp X, }⟩
 
 end equivalence
 

src/category_theory/adjunction/limits.lean

@@ -24,13 +24,24 @@ include adj
 section preservation_colimits
 variables {J : Type v} [small_category J] (K : J ⥤ C)
 
+def functoriality_right_adjoint : cocone (K ⋙ F) ⥤ cocone K :=
+(cocones.functoriality G) ⋙
+  (cocones.precompose (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv))
+
+local attribute [reducible] functoriality_right_adjoint
+
+@[simps] def functoriality_unit : 𝟭 (cocone K) ⟶ cocones.functoriality F ⋙ functoriality_right_adjoint adj K :=
+{ app := λ c, { hom := adj.unit.app c.X } }
+
+@[simps] def functoriality_counit : functoriality_right_adjoint adj K ⋙ cocones.functoriality F ⟶ 𝟭 (cocone (K ⋙ F)) :=
+{ app := λ c, { hom := adj.counit.app c.X } }
+
 def functoriality_is_left_adjoint :
   is_left_adjoint (@cocones.functoriality _ _ _ _ K _ _ F) :=
-{ right := (cocones.functoriality G) ⋙ (cocones.precompose
-    (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv)),
+{ right := functoriality_right_adjoint adj K,
   adj := mk_of_unit_counit
-  { unit := { app := λ c, { hom := adj.unit.app c.X } },
-    counit := { app := λ c, { hom := adj.counit.app c.X } } } }
+  { unit := functoriality_unit adj K,
+    counit := functoriality_counit adj K } }
 
 /-- A left adjoint preserves colimits. -/
 instance left_adjoint_preserves_colimits : preserves_colimits F :=
@@ -67,13 +78,24 @@ end preservation_colimits
 section preservation_limits
 variables {J : Type v} [small_category J] (K : J ⥤ D)
 
+def functoriality_left_adjoint : cone (K ⋙ G) ⥤ cone K :=
+(cones.functoriality F) ⋙ (cones.postcompose
+    ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom))
+
+local attribute [reducible] functoriality_left_adjoint
+
+@[simps] def functoriality_unit' : 𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality G :=
+{ app := λ c, { hom := adj.unit.app c.X, } }
+
+@[simps] def functoriality_counit' : cones.functoriality G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
+{ app := λ c, { hom := adj.counit.app c.X, } }
+
 def functoriality_is_right_adjoint :
   is_right_adjoint (@cones.functoriality _ _ _ _ K _ _ G) :=
-{ left := (cones.functoriality F) ⋙ (cones.postcompose
-    ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom)),
+{ left := functoriality_left_adjoint adj K,
   adj := mk_of_unit_counit
-  { unit := { app := λ c, { hom := adj.unit.app c.X, } },
-    counit := { app := λ c, { hom := adj.counit.app c.X, } } } }
+  { unit := functoriality_unit' adj K,
+    counit := functoriality_counit' adj K } }
 
 /-- A right adjoint preserves limits. -/
 instance right_adjoint_preserves_limits : preserves_limits G :=
@@ -107,36 +129,63 @@ def has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit (K
 
 end preservation_limits
 
+/-- auxilliary construction for `cocones_iso` -/
+@[simps]
+def cocones_iso_component_hom {J : Type v} [small_category J] {K : J ⥤ C}
+  (Y : D) (t : ((cocones J D).obj (op (K ⋙ F))).obj Y) :
+  (G ⋙ (cocones J C).obj (op K)).obj Y :=
+{ app := λ j, (adj.hom_equiv (K.obj j) Y) (t.app j),
+  naturality' := λ j j' f, by erw [← adj.hom_equiv_naturality_left, t.naturality]; dsimp; simp }
+
+/-- auxilliary construction for `cocones_iso` -/
+@[simps]
+def cocones_iso_component_inv {J : Type v} [small_category J] {K : J ⥤ C}
+  (Y : D) (t : (G ⋙ (cocones J C).obj (op K)).obj Y) :
+  ((cocones J D).obj (op (K ⋙ F))).obj Y :=
+{ app := λ j, (adj.hom_equiv (K.obj j) Y).symm (t.app j),
+  naturality' := λ j j' f,
+  begin
+    erw [← adj.hom_equiv_naturality_left_symm, ← adj.hom_equiv_naturality_right_symm, t.naturality],
+    dsimp, simp
+  end }
+
 -- Note: this is natural in K, but we do not yet have the tools to formulate that.
 def cocones_iso {J : Type v} [small_category J] {K : J ⥤ C} :
   (cocones J D).obj (op (K ⋙ F)) ≅ G ⋙ ((cocones J C).obj (op K)) :=
 nat_iso.of_components (λ Y,
-{ hom := λ t,
-    { app := λ j, (adj.hom_equiv (K.obj j) Y) (t.app j),
-      naturality' := λ j j' f, by erw [← adj.hom_equiv_naturality_left, t.naturality]; dsimp; simp },
-  inv := λ t,
-    { app := λ j, (adj.hom_equiv (K.obj j) Y).symm (t.app j),
-      naturality' := λ j j' f, begin
-        erw [← adj.hom_equiv_naturality_left_symm, ← adj.hom_equiv_naturality_right_symm, t.naturality],
-        dsimp, simp
-      end } } )
+{ hom := cocones_iso_component_hom adj Y,
+  inv := cocones_iso_component_inv adj Y, })
 (by tidy)
 
+/-- auxilliary construction for `cones_iso` -/
+@[simps]
+def cones_iso_component_hom {J : Type v} [small_category J] {K : J ⥤ D}
+  (X : Cᵒᵖ) (t : (functor.op F ⋙ (cones J D).obj K).obj X) :
+  ((cones J C).obj (K ⋙ G)).obj X :=
+  { app := λ j, (adj.hom_equiv (unop X) (K.obj j)) (t.app j),
+    naturality' := λ j j' f,
+    begin
+      erw [← adj.hom_equiv_naturality_right, ← t.naturality, category.id_comp, category.id_comp],
+      refl
+    end }
+
+/-- auxilliary construction for `cones_iso` -/
+@[simps]
+def cones_iso_component_inv {J : Type v} [small_category J] {K : J ⥤ D}
+  (X : Cᵒᵖ) (t : ((cones J C).obj (K ⋙ G)).obj X) :
+  (functor.op F ⋙ (cones J D).obj K).obj X :=
+{ app := λ j, (adj.hom_equiv (unop X) (K.obj j)).symm (t.app j),
+  naturality' := λ j j' f,
+  begin
+    erw [← adj.hom_equiv_naturality_right_symm, ← t.naturality, category.id_comp, category.id_comp]
+  end }
+
 -- Note: this is natural in K, but we do not yet have the tools to formulate that.
 def cones_iso {J : Type v} [small_category J] {K : J ⥤ D} :
   F.op ⋙ ((cones J D).obj K) ≅ (cones J C).obj (K ⋙ G) :=
 nat_iso.of_components (λ X,
-{ hom := λ t,
-  { app := λ j, (adj.hom_equiv (unop X) (K.obj j)) (t.app j),
-    naturality' := λ j j' f, begin
-      erw [← adj.hom_equiv_naturality_right, ← t.naturality, category.id_comp, category.id_comp],
-      refl
-    end },
-  inv := λ t,
-  { app := λ j, (adj.hom_equiv (unop X) (K.obj j)).symm (t.app j),
-    naturality' := λ j j' f, begin
-      erw [← adj.hom_equiv_naturality_right_symm, ← t.naturality, category.id_comp, category.id_comp]
-    end } } )
+{ hom := cones_iso_component_hom adj X,
+  inv := cones_iso_component_inv adj X, } )
 (by tidy)
 
 end category_theory.adjunction

src/category_theory/limits/cones.lean

@@ -60,10 +60,18 @@ end functor
 section
 variables (J C)
 
+/--
+Functorially associated to each functor `J ⥤ C`, we have the `C`-presheaf consisting of
+cones with a given cone point.
+-/
 @[simps] def cones : (J ⥤ C) ⥤ (Cᵒᵖ ⥤ Type v) :=
 { obj := functor.cones,
   map := λ F G f, whisker_left (const J).op (yoneda.map f) }
 
+/--
+Contravariantly associated to each functor `J ⥤ C`, we have the `C`-copresheaf consisting of
+cocones with a given cocone point.
+-/
 @[simps] def cocones : (J ⥤ C)ᵒᵖ ⥤ (C ⥤ Type v) :=
 { obj := λ F, functor.cocones (unop F),
   map := λ F G f, whisker_left (const J) (coyoneda.map f) }