chore(category_theory/limits): remove unnecessary typeclass arguments (…

…#4141)

Ongoing cleanup post #3995.

Previously we couldn't construct things like `instance : has_kernel (0 : X \hom Y)`, because it wouldn't have agreed definitionally with more general instances. Now we can.



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

src/category_theory/limits/shapes/equalizers.lean

@@ -507,19 +507,24 @@ is_iso_limit_cone_parallel_pair_of_eq ((cancel_epi _).1 (fork.condition c)) h
 
 end
 
+instance : has_equalizer f f :=
+has_limit.mk
+{ cone := id_fork rfl,
+  is_limit := is_limit_id_fork rfl }
+
 /-- The equalizer inclusion for `(f, f)` is an isomorphism. -/
-instance equalizer.ι_of_self [has_equalizer f f] : is_iso (equalizer.ι f f) :=
+instance equalizer.ι_of_self : is_iso (equalizer.ι f f) :=
 equalizer.ι_of_eq rfl
 
 /-- The equalizer of a morphism with itself is isomorphic to the source. -/
-def equalizer.iso_source_of_self [has_equalizer f f] : equalizer f f ≅ X :=
+def equalizer.iso_source_of_self : equalizer f f ≅ X :=
 as_iso (equalizer.ι f f)
 
-@[simp] lemma equalizer.iso_source_of_self_hom [has_equalizer f f] :
+@[simp] lemma equalizer.iso_source_of_self_hom :
   (equalizer.iso_source_of_self f).hom = equalizer.ι f f :=
 rfl
 
-@[simp] lemma equalizer.iso_source_of_self_inv [has_equalizer f f] :
+@[simp] lemma equalizer.iso_source_of_self_inv :
   (equalizer.iso_source_of_self f).inv = equalizer.lift (𝟙 X) (by simp) :=
 rfl
 
@@ -643,19 +648,24 @@ is_iso_colimit_cocone_parallel_pair_of_eq ((cancel_mono _).1 (cofork.condition c
 
 end
 
+instance : has_coequalizer f f :=
+has_colimit.mk
+{ cocone := id_cofork rfl,
+  is_colimit := is_colimit_id_cofork rfl }
+
 /-- The coequalizer projection for `(f, f)` is an isomorphism. -/
-instance coequalizer.π_of_self [has_coequalizer f f] : is_iso (coequalizer.π f f) :=
+instance coequalizer.π_of_self : is_iso (coequalizer.π f f) :=
 coequalizer.π_of_eq rfl
 
 /-- The coequalizer of a morphism with itself is isomorphic to the target. -/
-def coequalizer.iso_target_of_self [has_coequalizer f f] : coequalizer f f ≅ Y :=
+def coequalizer.iso_target_of_self : coequalizer f f ≅ Y :=
 (as_iso (coequalizer.π f f)).symm
 
-@[simp] lemma coequalizer.iso_target_of_self_hom [has_coequalizer f f] :
+@[simp] lemma coequalizer.iso_target_of_self_hom :
   (coequalizer.iso_target_of_self f).hom = coequalizer.desc (𝟙 Y) (by simp) :=
 rfl
 
-@[simp] lemma coequalizer.iso_target_of_self_inv [has_coequalizer f f] :
+@[simp] lemma coequalizer.iso_target_of_self_inv :
   (coequalizer.iso_target_of_self f).inv = coequalizer.π f f :=
 rfl
 

src/category_theory/limits/shapes/kernels.lean

@@ -8,8 +8,8 @@ import category_theory.limits.shapes.zero
 /-!
 # Kernels and cokernels
 
-In a category with zero morphisms, the kernel of a morphism `f : X ⟶ Y` is the equalizer of `f`
-and `0 : X ⟶ Y`. (Similarly the cokernel is the coequalizer.)
+In a category with zero morphisms, the kernel of a morphism `f : X ⟶ Y` is
+the equalizer of `f` and `0 : X ⟶ Y`. (Similarly the cokernel is the coequalizer.)
 
 The basic definitions are
 * `kernel : (X ⟶ Y) → C`
@@ -177,21 +177,21 @@ def kernel.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : {l : W ⟶ kernel f /
 ⟨kernel.lift f k h, kernel.lift_ι _ _ _⟩
 
 /-- Every kernel of the zero morphism is an isomorphism -/
-instance kernel.ι_zero_is_iso [has_kernel (0 : X ⟶ Y)] :
+instance kernel.ι_zero_is_iso :
   is_iso (kernel.ι (0 : X ⟶ Y)) :=
 equalizer.ι_of_self _
 
 lemma eq_zero_of_epi_kernel [epi (kernel.ι f)] : f = 0 :=
 (cancel_epi (kernel.ι f)).1 (by simp)
 
 /-- The kernel of a zero morphism is isomorphic to the source. -/
-def kernel_zero_iso_source [has_kernel (0 : X ⟶ Y)] : kernel (0 : X ⟶ Y) ≅ X :=
+def kernel_zero_iso_source : kernel (0 : X ⟶ Y) ≅ X :=
 equalizer.iso_source_of_self 0
 
-@[simp] lemma kernel_zero_iso_source_hom [has_kernel (0 : X ⟶ Y)] :
+@[simp] lemma kernel_zero_iso_source_hom :
   kernel_zero_iso_source.hom = kernel.ι (0 : X ⟶ Y) := rfl
 
-@[simp] lemma kernel_zero_iso_source_inv [has_kernel (0 : X ⟶ Y)] :
+@[simp] lemma kernel_zero_iso_source_inv :
   kernel_zero_iso_source.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp) := rfl
 
 /-- If two morphisms are known to be equal, then their kernels are isomorphic. -/
@@ -328,7 +328,7 @@ section
 variables (X Y)
 
 /-- The kernel morphism of a zero morphism is an isomorphism -/
-def kernel.ι_of_zero [has_kernel (0 : X ⟶ Y)] : is_iso (kernel.ι (0 : X ⟶ Y)) :=
+def kernel.ι_of_zero : is_iso (kernel.ι (0 : X ⟶ Y)) :=
 equalizer.ι_of_self _
 
 end
@@ -436,21 +436,21 @@ def cokernel.desc' {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) :
 ⟨cokernel.desc f k h, cokernel.π_desc _ _ _⟩
 
 /-- The cokernel of the zero morphism is an isomorphism -/
-instance cokernel.π_zero_is_iso [has_colimit (parallel_pair (0 : X ⟶ Y) 0)] :
+instance cokernel.π_zero_is_iso :
   is_iso (cokernel.π (0 : X ⟶ Y)) :=
 coequalizer.π_of_self _
 
 lemma eq_zero_of_mono_cokernel [mono (cokernel.π f)] : f = 0 :=
 (cancel_mono (cokernel.π f)).1 (by simp)
 
 /-- The cokernel of a zero morphism is isomorphic to the target. -/
-def cokernel_zero_iso_target [has_cokernel (0 : X ⟶ Y)] : cokernel (0 : X ⟶ Y) ≅ Y :=
+def cokernel_zero_iso_target : cokernel (0 : X ⟶ Y) ≅ Y :=
 coequalizer.iso_target_of_self 0
 
-@[simp] lemma cokernel_zero_iso_target_hom [has_cokernel (0 : X ⟶ Y)] :
+@[simp] lemma cokernel_zero_iso_target_hom :
   cokernel_zero_iso_target.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp) := rfl
 
-@[simp] lemma cokernel_zero_iso_target_inv [has_cokernel (0 : X ⟶ Y)] :
+@[simp] lemma cokernel_zero_iso_target_inv :
   cokernel_zero_iso_target.inv = cokernel.π (0 : X ⟶ Y) := rfl
 
 /-- If two morphisms are known to be equal, then their cokernels are isomorphic. -/
@@ -580,7 +580,7 @@ section
 variables (X Y)
 
 /-- The cokernel of a zero morphism is an isomorphism -/
-def cokernel.π_of_zero [has_cokernel (0 : X ⟶ Y)] :
+def cokernel.π_of_zero :
   is_iso (cokernel.π (0 : X ⟶ Y)) :=
 coequalizer.π_of_self _
 
@@ -646,11 +646,11 @@ variables (C : Type u) [category.{v} C]
 
 variables [has_zero_morphisms C]
 
-/-- `has_kernels` represents a choice of kernel for every morphism -/
+/-- `has_kernels` represents the existence of kernels for every morphism. -/
 class has_kernels : Prop :=
 (has_limit : Π {X Y : C} (f : X ⟶ Y), has_kernel f)
 
-/-- `has_cokernels` represents a choice of cokernel for every morphism -/
+/-- `has_cokernels` represents the existence of cokernels for every morphism. -/
 class has_cokernels : Prop :=
 (has_colimit : Π {X Y : C} (f : X ⟶ Y), has_cokernel f)