fix(category_theory/limits): Add some missing instances for special s…

…hapes of limits (leanprover-community#2083)

* Add some instances for limit shapes

* Deduce has_(equalizers|kernels|pullbacks) from has_finite_limits

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/category_theory/limits/shapes/equalizers.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison, Markus Himmel
 -/
 import data.fintype
 import category_theory.limits.limits
+import category_theory.limits.shapes.finite_limits
 
 /-!
 # Equalizers and coequalizers
@@ -62,13 +63,21 @@ instance fintype_walking_parallel_pair : fintype walking_parallel_pair :=
 open walking_parallel_pair
 
 /-- The type family of morphisms for the diagram indexing a (co)equalizer. -/
-inductive walking_parallel_pair_hom : walking_parallel_pair → walking_parallel_pair → Type v
+@[derive _root_.decidable_eq] inductive walking_parallel_pair_hom :
+  walking_parallel_pair → walking_parallel_pair → Type v
 | left : walking_parallel_pair_hom zero one
 | right : walking_parallel_pair_hom zero one
 | id : Π X : walking_parallel_pair.{v}, walking_parallel_pair_hom X X
 
 open walking_parallel_pair_hom
 
+instance (j j' : walking_parallel_pair) : fintype (walking_parallel_pair_hom j j') :=
+{ elems := walking_parallel_pair.rec_on j
+    (walking_parallel_pair.rec_on j' [walking_parallel_pair_hom.id zero].to_finset
+      [left, right].to_finset)
+    (walking_parallel_pair.rec_on j' ∅ [walking_parallel_pair_hom.id one].to_finset),
+  complete := by tidy }
+
 def walking_parallel_pair_hom.comp :
   Π (X Y Z : walking_parallel_pair)
     (f : walking_parallel_pair_hom X Y) (g : walking_parallel_pair_hom Y Z),
@@ -83,6 +92,8 @@ instance walking_parallel_pair_hom_category : small_category.{v} walking_paralle
   id   := walking_parallel_pair_hom.id,
   comp := walking_parallel_pair_hom.comp }
 
+instance : fin_category.{v} walking_parallel_pair.{v} := { }
+
 lemma walking_parallel_pair_hom_id (X : walking_parallel_pair.{v}) :
   walking_parallel_pair_hom.id X = 𝟙 X :=
 rfl
@@ -447,4 +458,13 @@ class has_coequalizers :=
 
 attribute [instance] has_equalizers.has_limits_of_shape has_coequalizers.has_colimits_of_shape
 
+/-- Equalizers are finite limits, so if `C` has all finite limits, it also has all equalizers -/
+def has_equalizers_of_has_finite_limits [has_finite_limits.{v} C] : has_equalizers.{v} C :=
+{ has_limits_of_shape := infer_instance }
+
+/-- Coequalizers are finite colimits, of if `C` has all finite colimits, it also has all
+    coequalizers -/
+def has_coequalizers_of_has_finite_colimits [has_finite_colimits.{v} C] : has_coequalizers.{v} C :=
+{ has_colimits_of_shape := infer_instance }
+
 end category_theory.limits

src/category_theory/limits/shapes/kernels.lean

@@ -222,4 +222,14 @@ class has_kernels :=
 class has_cokernels :=
 (has_colimit : Π {X Y : C} (f : X ⟶ Y), has_colimit (parallel_pair f 0))
 
+attribute [instance] has_kernels.has_limit has_cokernels.has_colimit
+
+/-- Kernels are finite limits, so if `C` has all finite limits, it also has all kernels -/
+def has_kernels_of_has_finite_limits [has_finite_limits.{v} C] : has_kernels.{v} C :=
+{ has_limit := infer_instance }
+
+/-- Cokernels are finite limits, so if `C` has all finite colimits, it also has all cokernels -/
+def has_cokernels_of_has_finite_colimits [has_finite_colimits.{v} C] : has_cokernels.{v} C :=
+{ has_colimit := infer_instance }
+
 end category_theory.limits

src/category_theory/limits/shapes/pullbacks.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import data.fintype
 import category_theory.limits.limits
+import category_theory.limits.shapes.finite_limits
 import category_theory.sparse
 
 /-!
@@ -46,13 +47,20 @@ instance fintype_walking_span : fintype walking_span :=
 namespace walking_cospan
 
 /-- The arrows in a pullback diagram. -/
-inductive hom : walking_cospan → walking_cospan → Type v
+@[derive _root_.decidable_eq] inductive hom : walking_cospan → walking_cospan → Type v
 | inl : hom left one
 | inr : hom right one
 | id : Π X : walking_cospan.{v}, hom X X
 
 open hom
 
+instance fintype_walking_cospan_hom (j j' : walking_cospan) : fintype (hom j j') :=
+{ elems := walking_cospan.rec_on j
+    (walking_cospan.rec_on j' [hom.id left].to_finset ∅ [inl].to_finset)
+    (walking_cospan.rec_on j' ∅ [hom.id right].to_finset [inr].to_finset)
+    (walking_cospan.rec_on j' ∅ ∅ [hom.id one].to_finset),
+  complete := by tidy }
+
 def hom.comp : Π (X Y Z : walking_cospan) (f : hom X Y) (g : hom Y Z), hom X Z
 | _ _ _ (id _) h := h
 | _ _ _ inl    (id one) := inl
@@ -73,18 +81,28 @@ lemma hom_id (X : walking_cospan.{v}) : hom.id X = 𝟙 X := rfl
 /-- The walking_cospan is the index diagram for a pullback. -/
 instance : small_category.{v} walking_cospan.{v} := sparse_category
 
+instance : fin_category.{v} walking_cospan.{v} :=
+{ fintype_hom := walking_cospan.fintype_walking_cospan_hom }
+
 end walking_cospan
 
 namespace walking_span
 
 /-- The arrows in a pushout diagram. -/
-inductive hom : walking_span → walking_span → Type v
+@[derive _root_.decidable_eq] inductive hom : walking_span → walking_span → Type v
 | fst : hom zero left
 | snd : hom zero right
 | id : Π X : walking_span.{v}, hom X X
 
 open hom
 
+instance fintype_walking_span_hom (j j' : walking_span) : fintype (hom j j') :=
+{ elems := walking_span.rec_on j
+    (walking_span.rec_on j' [hom.id zero].to_finset [fst].to_finset [snd].to_finset)
+    (walking_span.rec_on j' ∅ [hom.id left].to_finset ∅)
+    (walking_span.rec_on j' ∅ ∅ [hom.id right].to_finset),
+  complete := by tidy }
+
 def hom.comp : Π (X Y Z : walking_span) (f : hom X Y) (g : hom Y Z), hom X Z
   | _ _ _ (id _) h := h
   | _ _ _ fst    (id left) := fst
@@ -105,6 +123,9 @@ lemma hom_id (X : walking_span.{v}) : hom.id X = 𝟙 X := rfl
 /-- The walking_span is the index diagram for a pushout. -/
 instance : small_category.{v} walking_span.{v} := sparse_category
 
+instance : fin_category.{v} walking_span.{v} :=
+{ fintype_hom := walking_span.fintype_walking_span_hom }
+
 end walking_span
 
 open walking_span walking_cospan walking_span.hom walking_cospan.hom
@@ -299,11 +320,22 @@ lemma pushout.condition {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [has_colimit (sp
 
 variables (C)
 
+/-- `has_pullbacks` represents a choice of pullback for every pair of morphisms -/
 class has_pullbacks :=
 (has_limits_of_shape : has_limits_of_shape.{v} walking_cospan C)
+
+/-- `has_pushouts` represents a choice of pushout for every pair of morphisms -/
 class has_pushouts :=
 (has_colimits_of_shape : has_colimits_of_shape.{v} walking_span C)
 
 attribute [instance] has_pullbacks.has_limits_of_shape has_pushouts.has_colimits_of_shape
 
+/-- Pullbacks are finite limits, so if `C` has all finite limits, it also has all pullbacks -/
+def has_pullbacks_of_has_finite_limits [has_finite_limits.{v} C] : has_pullbacks.{v} C :=
+{ has_limits_of_shape := infer_instance }
+
+/-- Pushouts are finite colimits, so if `C` has all finite colimits, it also has all pushouts -/
+def has_pushouts_of_has_finite_colimits [has_finite_colimits.{v} C] : has_pushouts.{v} C :=
+{ has_colimits_of_shape := infer_instance }
+
 end category_theory.limits