refactor(category_theory/finite_limits): missing piece of #3320 (#3400)

A recent PR #3320 did some refactoring of special shapes of limits. It seems I forgot to include `wide_pullbacks` in that refactor, so I've done that here.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/category_theory/limits/shapes/finite_limits.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import data.fintype.basic
 import category_theory.limits.shapes.products
 import category_theory.limits.shapes.equalizers
 import category_theory.limits.shapes.pullbacks
@@ -89,12 +90,70 @@ def has_coequalizers_of_has_finite_colimits [has_finite_colimits C] : has_coequa
 
 variables {J : Type v}
 
+local attribute [tidy] tactic.case_bash
+
+namespace wide_pullback_shape
+
+instance fintype_obj [fintype J] : fintype (wide_pullback_shape J) :=
+by { rw wide_pullback_shape, apply_instance }
+
+instance fintype_hom [decidable_eq J] (j j' : wide_pullback_shape J) :
+  fintype (j ⟶ j') :=
+{ elems :=
+  begin
+    cases j',
+    { cases j,
+      { exact {hom.id none} },
+      { exact {hom.term j} } },
+    { by_cases some j' = j,
+      { rw h,
+        exact {hom.id j} },
+      { exact ∅ } }
+  end,
+  complete := by tidy }
+
+end wide_pullback_shape
+
+namespace wide_pushout_shape
+
+instance fintype_obj [fintype J] : fintype (wide_pushout_shape J) :=
+by { rw wide_pushout_shape, apply_instance }
+
+instance fintype_hom [decidable_eq J] (j j' : wide_pushout_shape J) :
+  fintype (j ⟶ j') :=
+{ elems :=
+  begin
+    cases j,
+    { cases j',
+      { exact {hom.id none} },
+      { exact {hom.init j'} } },
+    { by_cases some j = j',
+      { rw h,
+        exact {hom.id j'} },
+      { exact ∅ } }
+  end,
+  complete := by tidy }
+
+end wide_pushout_shape
+
 instance fin_category_wide_pullback [fintype J] [decidable_eq J] : fin_category (wide_pullback_shape J) :=
 { fintype_hom := wide_pullback_shape.fintype_hom }
 
 instance fin_category_wide_pushout [fintype J] [decidable_eq J] : fin_category (wide_pushout_shape J) :=
 { fintype_hom := wide_pushout_shape.fintype_hom }
 
+/-- `has_finite_wide_pullbacks` represents a choice of wide pullback for every finite collection of morphisms -/
+class has_finite_wide_pullbacks :=
+(has_limits_of_shape : Π (J : Type v) [decidable_eq J] [fintype J], has_limits_of_shape (wide_pullback_shape J) C)
+
+attribute [instance] has_finite_wide_pullbacks.has_limits_of_shape
+
+/-- `has_finite_wide_pushouts` represents a choice of wide pushout for every finite collection of morphisms -/
+class has_finite_wide_pushouts :=
+(has_colimits_of_shape : Π (J : Type v) [decidable_eq J] [fintype J], has_colimits_of_shape (wide_pushout_shape J) C)
+
+attribute [instance] has_finite_wide_pushouts.has_colimits_of_shape
+
 /-- Finite wide pullbacks are finite limits, so if `C` has all finite limits, it also has finite wide pullbacks -/
 def has_finite_wide_pullbacks_of_has_finite_limits [has_finite_limits C] : has_finite_wide_pullbacks C :=
 { has_limits_of_shape := λ J _ _, by exactI (has_finite_limits.has_limits_of_shape _) }

src/category_theory/limits/shapes/wide_pullbacks.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import data.fintype.basic
 import category_theory.limits.limits
 import category_theory.sparse
 
@@ -29,6 +28,8 @@ universes v u
 
 open category_theory category_theory.limits
 
+namespace category_theory.limits
+
 variable (J : Type v)
 
 /-- A wide pullback shape for any type `J` can be written simply as `option J`. -/
@@ -41,9 +42,6 @@ def wide_pushout_shape := option J
 
 namespace wide_pullback_shape
 
-instance fintype_obj [fintype J] : fintype (wide_pullback_shape J) :=
-by { rw wide_pullback_shape, apply_instance }
-
 variable {J}
 
 /-- The type of arrows for the shape indexing a wide pullback. -/
@@ -69,21 +67,6 @@ instance hom.inhabited : inhabited (hom none none) := ⟨hom.id (none : wide_pul
 
 local attribute [tidy] tactic.case_bash
 
-instance fintype_hom [decidable_eq J] (j j' : wide_pullback_shape J) :
-  fintype (j ⟶ j') :=
-{ elems :=
-  begin
-    cases j',
-    { cases j,
-      { exact {hom.id none} },
-      { exact {hom.term j} } },
-    { by_cases some j' = j,
-      { rw h,
-        exact {hom.id j} },
-      { exact ∅ } }
-  end,
-  complete := by tidy }
-
 instance subsingleton_hom (j j' : wide_pullback_shape J) : subsingleton (j ⟶ j') :=
 ⟨by tidy⟩
 
@@ -116,9 +99,6 @@ end wide_pullback_shape
 
 namespace wide_pushout_shape
 
-instance fintype_obj [fintype J] : fintype (wide_pushout_shape J) :=
-by { rw wide_pushout_shape, apply_instance }
-
 variable {J}
 
 /-- The type of arrows for the shape indexing a wide psuhout. -/
@@ -144,21 +124,6 @@ instance hom.inhabited : inhabited (hom none none) := ⟨hom.id (none : wide_pus
 
 local attribute [tidy] tactic.case_bash
 
-instance fintype_hom [decidable_eq J] (j j' : wide_pushout_shape J) :
-  fintype (j ⟶ j') :=
-{ elems :=
-  begin
-    cases j,
-    { cases j',
-      { exact {hom.id none} },
-      { exact {hom.init j'} } },
-    { by_cases some j = j',
-      { rw h,
-        exact {hom.id j'} },
-      { exact ∅ } }
-  end,
-  complete := by tidy }
-
 instance subsingleton_hom (j j' : wide_pushout_shape J) : subsingleton (j ⟶ j') :=
 ⟨by tidy⟩
 
@@ -195,20 +160,12 @@ variables (C : Type u) [category.{v} C]
 class has_wide_pullbacks :=
 (has_limits_of_shape : Π (J : Type v), has_limits_of_shape (wide_pullback_shape J) C)
 
-/-- `has_wide_pullbacks` represents a choice of wide pullback for every finite collection of morphisms -/
-class has_finite_wide_pullbacks :=
-(has_limits_of_shape : Π (J : Type v) [decidable_eq J] [fintype J], has_limits_of_shape (wide_pullback_shape J) C)
-
 attribute [instance] has_wide_pullbacks.has_limits_of_shape
-attribute [instance] has_finite_wide_pullbacks.has_limits_of_shape
 
 /-- `has_wide_pushouts` represents a choice of wide pushout for every collection of morphisms -/
 class has_wide_pushouts :=
 (has_colimits_of_shape : Π (J : Type v), has_colimits_of_shape (wide_pushout_shape J) C)
 
-/-- `has_wide_pushouts` represents a choice of wide pushout for every finite collection of morphisms -/
-class has_finite_wide_pushouts :=
-(has_colimits_of_shape : Π (J : Type v) [decidable_eq J] [fintype J], has_colimits_of_shape (wide_pushout_shape J) C)
-
 attribute [instance] has_wide_pushouts.has_colimits_of_shape
-attribute [instance] has_finite_wide_pushouts.has_colimits_of_shape
+
+end category_theory.limits