From 77674a04e3ec11f5e0f94f4f787e56887b1d9dc6 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 29 May 2020 16:24:02 +0000 Subject: [PATCH] chore(category_theory): T50000 challenge (#2840) A lame effort at making something compile with `-T50000`. No actual speed improvement, just split up a definition into pieces. Co-authored-by: Scott Morrison --- src/category_theory/limits/over.lean | 45 +++++++++++++++---- .../limits/shapes/binary_products.lean | 10 ++--- 2 files changed, 39 insertions(+), 16 deletions(-) diff --git a/src/category_theory/limits/over.lean b/src/category_theory/limits/over.lean index 991968c63a56d..e4da1bd1aa7b1 100644 --- a/src/category_theory/limits/over.lean +++ b/src/category_theory/limits/over.lean @@ -94,16 +94,27 @@ namespace construct_products def wide_pullback_diagram_of_diagram_over (B : C) {J : Type v} (F : discrete J ⥤ over B) : wide_pullback_shape J ⥤ C := wide_pullback_shape.wide_cospan B (λ j, (F.obj j).left) (λ j, (F.obj j).hom) -local attribute [tidy] tactic.case_bash +/-- (Impl) A preliminary definition to avoid timeouts. -/ +@[simps] +def cones_equiv_inverse_obj (B : C) {J : Type v} (F : discrete J ⥤ over B) (c : cone F) : + cone (wide_pullback_diagram_of_diagram_over B F) := +{ X := c.X.left, + π := + { app := λ X, option.cases_on X c.X.hom (λ (j : J), (c.π.app j).left), + -- `tidy` can do this using `case_bash`, but let's try to be a good `-T50000` citizen: + naturality' := λ X Y f, + begin + dsimp, cases X; cases Y; cases f, + { rw [category.id_comp, category.comp_id], }, + { rw [over.w, category.id_comp], }, + { rw [category.id_comp, category.comp_id], }, + end } } --- FIXME deterministic timeout with `-T50000` -/-- (Impl) Pull these out to avoid timeouts. -/ +/-- (Impl) A preliminary definition to avoid timeouts. -/ @[simps] def cones_equiv_inverse (B : C) {J : Type v} (F : discrete J ⥤ over B) : cone F ⥤ cone (wide_pullback_diagram_of_diagram_over B F) := -{ obj := λ c, - { X := c.X.left, - π := { app := λ X, option.cases_on X c.X.hom (λ (j : J), (c.π.app j).left) } }, +{ obj := cones_equiv_inverse_obj B F, map := λ c₁ c₂ f, { hom := f.hom.left, w' := λ j, @@ -115,7 +126,7 @@ def cones_equiv_inverse (B : C) {J : Type v} (F : discrete J ⥤ over B) : refl } end } } -/-- (Impl) Pull these out to avoid timeouts. -/ +/-- (Impl) A preliminary definition to avoid timeouts. -/ @[simps] def cones_equiv_functor (B : C) {J : Type v} (F : discrete J ⥤ over B) : cone (wide_pullback_diagram_of_diagram_over B F) ⥤ cone F := @@ -125,6 +136,22 @@ def cones_equiv_functor (B : C) {J : Type v} (F : discrete J ⥤ over B) : map := λ c₁ c₂ f, { hom := over.hom_mk f.hom } } +local attribute [tidy] tactic.case_bash + +/-- (Impl) A preliminary definition to avoid timeouts. -/ +@[simp] +def cones_equiv_unit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) : + 𝟭 (cone (wide_pullback_diagram_of_diagram_over B F)) ≅ + cones_equiv_functor B F ⋙ cones_equiv_inverse B F := +nat_iso.of_components (λ _, cones.ext {hom := 𝟙 _, inv := 𝟙 _} (by tidy)) (by tidy) + +/-- (Impl) A preliminary definition to avoid timeouts. -/ +@[simp] +def cones_equiv_counit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) : + cones_equiv_inverse B F ⋙ cones_equiv_functor B F ≅ 𝟭 (cone F) := +nat_iso.of_components + (λ _, cones.ext {hom := over.hom_mk (𝟙 _), inv := over.hom_mk (𝟙 _)} (by tidy)) (by tidy) + -- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and `cones.ext`? /-- (Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`. -/ @[simps] @@ -132,8 +159,8 @@ def cones_equiv (B : C) {J : Type v} (F : discrete J ⥤ over B) : cone (wide_pullback_diagram_of_diagram_over B F) ≌ cone F := { functor := cones_equiv_functor B F, inverse := cones_equiv_inverse B F, - unit_iso := nat_iso.of_components (λ _, cones.ext {hom := 𝟙 _, inv := 𝟙 _} (by tidy)) (by tidy), - counit_iso := nat_iso.of_components (λ _, cones.ext {hom := over.hom_mk (𝟙 _), inv := over.hom_mk (𝟙 _)} (by tidy)) (by tidy) } + unit_iso := cones_equiv_unit_iso B F, + counit_iso := cones_equiv_counit_iso B F, } /-- Use the above equivalence to prove we have a limit. -/ def has_over_limit_discrete_of_wide_pullback_limit {B : C} {J : Type v} (F : discrete J ⥤ over B) diff --git a/src/category_theory/limits/shapes/binary_products.lean b/src/category_theory/limits/shapes/binary_products.lean index f2a9f4c7b6e3c..93fa823c48185 100644 --- a/src/category_theory/limits/shapes/binary_products.lean +++ b/src/category_theory/limits/shapes/binary_products.lean @@ -362,8 +362,6 @@ section variables {C} [has_binary_products.{v} C] variables {D : Type u₂} [category.{v} D] [has_binary_products.{v} D] -local attribute [tidy] tactic.case_bash - -- FIXME deterministic timeout with `-T50000` /-- The binary product functor. -/ @[simps] @@ -411,7 +409,7 @@ nat_iso.of_components (prod.associator _ _) (by tidy) lemma prod.pentagon (W X Y Z : C) : prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫ (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) = - (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y⨯Z)).hom := + (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom := by tidy @[reassoc] @@ -482,8 +480,6 @@ end section variables {C} [has_binary_coproducts.{v} C] -local attribute [tidy] tactic.case_bash - /-- The braiding isomorphism which swaps a binary coproduct. -/ @[simps] def coprod.braiding (P Q : C) : P ⨿ Q ≅ Q ⨿ P := { hom := coprod.desc coprod.inr coprod.inl, @@ -512,8 +508,8 @@ by simp lemma coprod.pentagon (W X Y Z : C) : coprod.map ((coprod.associator W X Y).hom) (𝟙 Z) ≫ - (coprod.associator W (X⨿Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) = - (coprod.associator (W⨿X) Y Z).hom ≫ (coprod.associator W X (Y⨿Z)).hom := + (coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) = + (coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom := by tidy lemma coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :