chore(category/abelian/pseudoelements): localize expensive typeclass (#…

…9156)

Per @fpvandoorn's [new linter](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/type-class.20loops.20in.20category.20theory).

src/category_theory/abelian/diagram_lemmas/four.lean

@@ -57,6 +57,8 @@ variables {V : Type u} [category.{v} V] [abelian V]
 local attribute [instance] preadditive.has_equalizers_of_has_kernels
 local attribute [instance] object_to_sort hom_to_fun
 
+open_locale pseudoelement
+
 namespace category_theory.abelian
 
 variables {A B C D A' B' C' D' : V}

src/category_theory/abelian/pseudoelements.lean

@@ -200,7 +200,14 @@ quotient.sound $ (pseudo_zero_aux R _).2 rfl
 /-- The zero pseudoelement is the class of a zero morphism -/
 def pseudo_zero {P : C} : P := ⟦(0 : P ⟶ P)⟧
 
-instance {P : C} : has_zero P := ⟨pseudo_zero⟩
+/--
+We can not use `pseudo_zero` as a global `has_zero` instance,
+as it would trigger on any type class search for `has_zero` applied to a `coe_sort`.
+This would be too expensive.
+-/
+def has_zero {P : C} : has_zero P := ⟨pseudo_zero⟩
+localized "attribute [instance] category_theory.abelian.pseudoelement.has_zero" in pseudoelement
+
 instance {P : C} : inhabited (pseudoelement P) := ⟨0⟩
 
 lemma pseudo_zero_def {P : C} : (0 : pseudoelement P) = ⟦(0 : P ⟶ P)⟧ := rfl
@@ -213,6 +220,8 @@ by { rw ←pseudo_zero_aux P a, exact quotient.eq }
 
 end zero
 
+open_locale pseudoelement
+
 /-- Morphisms map the zero pseudoelement to the zero pseudoelement -/
 @[simp] theorem apply_zero {P Q : C} (f : P ⟶ Q) : f 0 = 0 :=
 by { rw [pseudo_zero_def, pseudo_apply_mk], simp }