refactor(category_theory): remove all decidability instances (#14046)

Make the category theory library thoroughly classical: mostly this is ceasing carrying around decidability instances for the indexing types of biproducts, and for the object and morphism types in `fin_category`.

It appears there was no real payoff: the category theory library is already extremely non-constructive.
As I was running into occasional problems providing decidability instances (when writing construction involving reindexing biproducts), it seems easiest to just remove this vestigial constructiveness from the category theory library.
 


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

Author: kim-em

src/algebra/category/Group/biproducts.lean

@@ -114,13 +114,13 @@ We verify that the biproduct we've just defined is isomorphic to the AddCommGrou
 on the dependent function type
 -/
 @[simps hom_apply] noncomputable
-def biproduct_iso_pi [decidable_eq J] [fintype J] (f : J → AddCommGroup.{u}) :
+def biproduct_iso_pi [fintype J] (f : J → AddCommGroup.{u}) :
   (⨁ f : AddCommGroup) ≅ AddCommGroup.of (Π j, f j) :=
 is_limit.cone_point_unique_up_to_iso
   (biproduct.is_limit f)
   (product_limit_cone f).is_limit
 
-@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π [decidable_eq J] [fintype J]
+@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π [fintype J]
   (f : J → AddCommGroup.{u}) (j : J) :
   (biproduct_iso_pi f).inv ≫ biproduct.π f j = pi.eval_add_monoid_hom (λ j, f j) j :=
 is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk j)

src/algebra/category/Module/abelian.lean

@@ -69,7 +69,7 @@ def normal_epi (hf : epi f) : normal_epi f :=
 
 /-- The category of R-modules is abelian. -/
 instance : abelian (Module R) :=
-{ has_finite_products := ⟨λ J _ _, limits.has_limits_of_shape_of_has_limits⟩,
+{ has_finite_products := ⟨λ J _, limits.has_limits_of_shape_of_has_limits⟩,
   has_kernels := limits.has_kernels_of_has_equalizers (Module R),
   has_cokernels := has_cokernels_Module,
   normal_mono_of_mono := λ X Y, normal_mono,

src/algebra/category/Module/biproducts.lean

@@ -117,13 +117,13 @@ We verify that the biproduct we've just defined is isomorphic to the `Module R`
 on the dependent function type
 -/
 @[simps hom_apply] noncomputable
-def biproduct_iso_pi [decidable_eq J] [fintype J] (f : J → Module.{v} R) :
+def biproduct_iso_pi [fintype J] (f : J → Module.{v} R) :
   (⨁ f : Module.{v} R) ≅ Module.of R (Π j, f j) :=
 is_limit.cone_point_unique_up_to_iso
   (biproduct.is_limit f)
   (product_limit_cone f).is_limit
 
-@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π [decidable_eq J] [fintype J]
+@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π [fintype J]
   (f : J → Module.{v} R) (j : J) :
   (biproduct_iso_pi f).inv ≫ biproduct.π f j = (linear_map.proj j : (Π j, f j) →ₗ[R] f j) :=
 is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk j)

src/category_theory/closed/ideal.lean

@@ -110,7 +110,7 @@ variables {C : Type u₁} {D : Type u₂} [category.{v₁} C] [category.{v₁} D
 variables (i : D ⥤ C)
 
 lemma reflective_products [has_finite_products C] [reflective i] : has_finite_products D :=
-⟨λ J 𝒥₁ 𝒥₂, by exactI has_limits_of_shape_of_reflective i⟩
+⟨λ J 𝒥, by exactI has_limits_of_shape_of_reflective i⟩
 
 local attribute [instance, priority 10] reflective_products
 

src/category_theory/fin_category.lean

@@ -13,33 +13,32 @@ import category_theory.opposites
 A category is finite in this sense if it has finitely many objects, and finitely many morphisms.
 
 ## Implementation
-
-We also ask for decidable equality of objects and morphisms, but it may be reasonable to just
-go classical in future.
+Prior to #14046, `fin_category` required a `decidable_eq` instance on the object and morphism types.
+This does not seem to have had any practical payoff (i.e. making some definition constructive)
+so we have removed these requirements to avoid
+having to supply instances or delay with non-defeq conflicts between instances.
 -/
 
 universes v u
+open_locale classical
+noncomputable theory
 
 namespace category_theory
 
 instance discrete_fintype {α : Type*} [fintype α] : fintype (discrete α) :=
 fintype.of_equiv α (discrete_equiv.symm)
 
-instance discrete_hom_fintype {α : Type*} [decidable_eq α] (X Y : discrete α) : fintype (X ⟶ Y) :=
+instance discrete_hom_fintype {α : Type*} (X Y : discrete α) : fintype (X ⟶ Y) :=
 by { apply ulift.fintype }
 
 /-- A category with a `fintype` of objects, and a `fintype` for each morphism space. -/
 class fin_category (J : Type v) [small_category J] :=
-(decidable_eq_obj : decidable_eq J . tactic.apply_instance)
 (fintype_obj : fintype J . tactic.apply_instance)
-(decidable_eq_hom : Π (j j' : J), decidable_eq (j ⟶ j') . tactic.apply_instance)
 (fintype_hom : Π (j j' : J), fintype (j ⟶ j') . tactic.apply_instance)
 
-attribute [instance] fin_category.decidable_eq_obj fin_category.fintype_obj
-                     fin_category.decidable_eq_hom fin_category.fintype_hom
+attribute [instance] fin_category.fintype_obj fin_category.fintype_hom
 
--- We need a `decidable_eq` instance here to construct `fintype` on the morphism spaces.
-instance fin_category_discrete_of_decidable_fintype (J : Type v) [decidable_eq J] [fintype J] :
+instance fin_category_discrete_of_fintype (J : Type v) [fintype J] :
   fin_category (discrete J) :=
 { }
 
@@ -97,9 +96,7 @@ The opposite of a finite category is finite.
 -/
 instance fin_category_opposite {J : Type v} [small_category J] [fin_category J] :
   fin_category Jᵒᵖ :=
-{ decidable_eq_obj := equiv.decidable_eq equiv_to_opposite.symm,
-  fintype_obj := fintype.of_equiv _ equiv_to_opposite,
-  decidable_eq_hom := λ j j', equiv.decidable_eq (op_equiv j j'),
+{ fintype_obj := fintype.of_equiv _ equiv_to_opposite,
   fintype_hom := λ j j', fintype.of_equiv _ (op_equiv j j').symm, }
 
 end category_theory

src/category_theory/idempotents/biproducts.lean

@@ -42,7 +42,7 @@ namespace biproducts
 /-- The `bicone` used in order to obtain the existence of
 the biproduct of a functor `J ⥤ karoubi C` when the category `C` is additive. -/
 @[simps]
-def bicone [has_finite_biproducts C] {J : Type v} [decidable_eq J] [fintype J]
+def bicone [has_finite_biproducts C] {J : Type v} [fintype J]
   (F : J → karoubi C) : bicone F :=
 { X :=
   { X := biproduct (λ j, (F j).X),
@@ -74,9 +74,10 @@ end biproducts
 
 lemma karoubi_has_finite_biproducts [has_finite_biproducts C] :
   has_finite_biproducts (karoubi C) :=
-{ has_biproducts_of_shape := λ J hJ₁ hJ₂,
+{ has_biproducts_of_shape := λ J hJ,
   { has_biproduct := λ F, begin
-      letI := hJ₂,
+      classical,
+      letI := hJ,
       apply has_biproduct_of_total (biproducts.bicone F),
       ext1, ext1,
       simp only [id_eq, comp_id, biproducts.bicone_X_p, biproduct.ι_map],

src/category_theory/limits/bicones.lean

@@ -23,7 +23,10 @@ This is used in `category_theory.flat_functors.preserves_finite_limits_of_flat`.
 
 universes v₁ u₁
 
+noncomputable theory
+
 open category_theory.limits
+open_locale classical
 
 namespace category_theory
 section bicone
@@ -38,11 +41,11 @@ inductive bicone
 
 instance : inhabited (bicone J) := ⟨bicone.left⟩
 
-instance fin_bicone [fintype J] [decidable_eq J] : fintype (bicone J) :=
+instance fin_bicone [fintype J] : fintype (bicone J) :=
 { elems := [bicone.left, bicone.right].to_finset ∪ finset.image bicone.diagram (fintype.elems J),
   complete := λ j, by { cases j; simp, exact fintype.complete j, }, }
 
-variables [category.{v₁} J] [∀ (j k : J), decidable_eq (j ⟶ k)]
+variables [category.{v₁} J]
 
 /-- The homs for a walking `bicone J`. -/
 inductive bicone_hom : bicone J → bicone J → Type (max u₁ v₁)
@@ -80,7 +83,7 @@ variables (J : Type v₁) [small_category J]
 /--
 Given a diagram `F : J ⥤ C` and two `cone F`s, we can join them into a diagram `bicone J ⥤ C`.
 -/
-@[simps] def bicone_mk [∀ (j k : J), decidable_eq (j ⟶ k)] {C : Type u₁} [category.{v₁} C]
+@[simps] def bicone_mk {C : Type u₁} [category.{v₁} C]
   {F : J ⥤ C} (c₁ c₂ : cone F) : bicone J ⥤ C :=
 { obj := λ X, bicone.cases_on X c₁.X c₂.X (λ j, F.obj j),
   map := λ X Y f, by
@@ -113,8 +116,8 @@ begin
             { cases f, simp only [finset.mem_image], use f_f, simpa using fintype.complete _, } },
 end
 
-instance bicone_small_category [∀ (j k : J), decidable_eq (j ⟶ k)] :
-  small_category (bicone J) := category_theory.bicone_category J
+instance bicone_small_category : small_category (bicone J) :=
+category_theory.bicone_category J
 
 instance bicone_fin_category [fin_category J] : fin_category (bicone J) := {}
 end small_category

src/category_theory/limits/constructions/finite_products_of_binary_products.lean

@@ -133,7 +133,7 @@ end }
 
 /-- If `C` has a terminal object and binary products, then it has finite products. -/
 lemma has_finite_products_of_has_binary_and_terminal : has_finite_products C :=
-⟨λ J 𝒥₁ 𝒥₂, begin
+⟨λ J 𝒥, begin
   resetI,
   let e := fintype.equiv_fin J,
   apply has_limits_of_shape_of_equivalence (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
@@ -313,7 +313,7 @@ end }
 
 /-- If `C` has an initial object and binary coproducts, then it has finite coproducts. -/
 lemma has_finite_coproducts_of_has_binary_and_terminal : has_finite_coproducts C :=
-⟨λ J 𝒥₁ 𝒥₂, begin
+⟨λ J 𝒥, begin
   resetI,
   let e := fintype.equiv_fin J,
   apply has_colimits_of_shape_of_equivalence (discrete.equivalence (e.trans equiv.ulift.symm)).symm,

src/category_theory/limits/constructions/over/products.lean

@@ -139,7 +139,7 @@ lemma over_products_of_wide_pullbacks [has_wide_pullbacks C] {B : C} :
 /-- Given all finite wide pullbacks in `C`, construct finite products in `C/B`. -/
 lemma over_finite_products_of_finite_wide_pullbacks [has_finite_wide_pullbacks C] {B : C} :
   has_finite_products (over B) :=
-⟨λ J 𝒥₁ 𝒥₂, by exactI over_product_of_wide_pullback⟩
+⟨λ J 𝒥, by exactI over_product_of_wide_pullback⟩
 
 end construct_products
 

src/category_theory/limits/lattice.lean

@@ -75,7 +75,7 @@ lemma finite_colimit_eq_finset_univ_sup [semilattice_sup α] [order_bot α] (F :
 /--
 A finite product in the category of a `semilattice_inf` with `order_top` is the same as the infimum.
 -/
-lemma finite_product_eq_finset_inf [semilattice_inf α] [order_top α] {ι : Type u} [decidable_eq ι]
+lemma finite_product_eq_finset_inf [semilattice_inf α] [order_top α] {ι : Type u}
   [fintype ι] (f : ι → α) : (∏ f) = (fintype.elems ι).inf f :=
 begin
   transitivity,
@@ -90,7 +90,7 @@ end
 A finite coproduct in the category of a `semilattice_sup` with `order_bot` is the same as the
 supremum.
 -/
-lemma finite_coproduct_eq_finset_sup [semilattice_sup α] [order_bot α] {ι : Type u} [decidable_eq ι]
+lemma finite_coproduct_eq_finset_sup [semilattice_sup α] [order_bot α] {ι : Type u}
   [fintype ι] (f : ι → α) : (∐ f) = (fintype.elems ι).sup f :=
 begin
   transitivity,