refactor(category_theory/limits/shapes/finite_products): review API, …

…fix lint (#17623)

* Redefine `category_theory.limits.has_finite_products` to use `fin n` instead of any finite `Type`.
* Merge `has_limits_of_shape_discrete` with a more general `has_fintype_products`.
* Do similar changes to `*_coproducts`.

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 := ⟨λ n, 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/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⟩
+⟨λ n, has_limits_of_shape_of_reflective i⟩
 
 local attribute [instance, priority 10] reflective_products
 

src/category_theory/extensive.lean

@@ -486,8 +486,7 @@ end
 
 instance [has_pullbacks C] [finitary_extensive C] : finitary_extensive (D ⥤ C) :=
 begin
-  haveI : has_finite_coproducts (D ⥤ C) :=
-    ⟨λ J hJ, by exactI limits.functor_category_has_colimits_of_shape⟩,
+  haveI : has_finite_coproducts (D ⥤ C) := ⟨λ n, limits.functor_category_has_colimits_of_shape⟩,
   exact ⟨λ X Y c hc, is_van_kampen_colimit_of_evaluation _ c
     (λ x, finitary_extensive.van_kampen _ $ preserves_colimit.preserves hc)⟩
 end

src/category_theory/idempotents/biproducts.lean

@@ -74,10 +74,9 @@ end biproducts
 
 lemma karoubi_has_finite_biproducts [has_finite_biproducts C] :
   has_finite_biproducts (karoubi C) :=
-{ has_biproducts_of_shape := λ J hJ,
+{ out := λ n,
   { has_biproduct := λ F, begin
       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/constructions/finite_products_of_binary_products.lean

@@ -110,28 +110,14 @@ private lemma has_product_fin :
     apply has_limit.mk ⟨_, extend_fan_is_limit f (limit.is_limit _) (limit.is_limit _)⟩,
   end
 
-/--
-If `C` has a terminal object and binary products, then it has limits of shape
-`discrete (fin n)` for any `n : ℕ`.
-This is a helper lemma for `has_finite_products_of_has_binary_and_terminal`, which is more general
-than this.
--/
-private lemma has_limits_of_shape_fin (n : ℕ) :
-  has_limits_of_shape (discrete (fin n)) C :=
-{ has_limit := λ K,
+/-- 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 :=
 begin
+  refine ⟨λ n, ⟨λ K, _⟩⟩,
   letI := has_product_fin n (λ n, K.obj ⟨n⟩),
   let : discrete.functor (λ n, K.obj ⟨n⟩) ≅ K := discrete.nat_iso (λ ⟨i⟩, iso.refl _),
   apply has_limit_of_iso this,
-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
-  resetI,
-  apply has_limits_of_shape_of_equivalence (discrete.equivalence (fintype.equiv_fin J)).symm,
-  refine has_limits_of_shape_fin (fintype.card J),
-end⟩
+end
 
 end
 
@@ -286,28 +272,14 @@ private lemma has_coproduct_fin :
       ⟨_, extend_cofan_is_colimit f (colimit.is_colimit _) (colimit.is_colimit _)⟩,
   end
 
-/--
-If `C` has an initial object and binary coproducts, then it has colimits of shape
-`discrete (fin n)` for any `n : ℕ`.
-This is a helper lemma for `has_cofinite_products_of_has_binary_and_terminal`, which is more general
-than this.
--/
-private lemma has_colimits_of_shape_fin (n : ℕ) :
-  has_colimits_of_shape (discrete (fin n)) C :=
-{ has_colimit := λ K,
+/-- If `C` has an initial object and binary coproducts, then it has finite coproducts. -/
+lemma has_finite_coproducts_of_has_binary_and_initial : has_finite_coproducts C :=
 begin
+  refine ⟨λ n, ⟨λ K, _⟩⟩,
   letI := has_coproduct_fin n (λ n, K.obj ⟨n⟩),
   let : K ≅ discrete.functor (λ n, K.obj ⟨n⟩) := discrete.nat_iso (λ ⟨i⟩, iso.refl _),
   apply has_colimit_of_iso this,
-end }
-
-/-- If `C` has an initial object and binary coproducts, then it has finite coproducts. -/
-lemma has_finite_coproducts_of_has_binary_and_initial : has_finite_coproducts C :=
-⟨λ J 𝒥, begin
-  resetI,
-  apply has_colimits_of_shape_of_equivalence (discrete.equivalence (fintype.equiv_fin J)).symm,
-  refine has_colimits_of_shape_fin (fintype.card J),
-end⟩
+end
 
 end
 

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

@@ -139,7 +139,7 @@ lemma over_products_of_wide_pullbacks [has_wide_pullbacks.{w} 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⟩
+⟨λ n, over_product_of_wide_pullback⟩
 
 end construct_products
 

src/category_theory/limits/opposites.lean

@@ -343,16 +343,16 @@ lemma has_coproducts_of_opposite [has_products.{v₂} Cᵒᵖ] : has_coproducts.
 λ X, has_coproducts_of_shape_of_opposite X
 
 instance has_finite_coproducts_opposite [has_finite_products C] : has_finite_coproducts Cᵒᵖ :=
-{ out := λ J _, by exactI infer_instance }
+{ out := λ n, limits.has_coproducts_of_shape_opposite _ }
 
 lemma has_finite_coproducts_of_opposite [has_finite_products Cᵒᵖ] : has_finite_coproducts C :=
-{ out := λ J _, by exactI has_coproducts_of_shape_of_opposite J }
+{ out := λ n, has_coproducts_of_shape_of_opposite _ }
 
 instance has_finite_products_opposite [has_finite_coproducts C] : has_finite_products Cᵒᵖ :=
-{ out := λ J _, by exactI infer_instance }
+{ out := λ n, infer_instance }
 
 lemma has_finite_products_of_opposite [has_finite_coproducts Cᵒᵖ] : has_finite_products C :=
-{ out := λ J _, by exactI has_products_of_shape_of_opposite J }
+{ out := λ n, has_products_of_shape_of_opposite _ }
 
 instance has_equalizers_opposite [has_coequalizers C] : has_equalizers Cᵒᵖ :=
 begin

src/category_theory/limits/shapes/biproducts.lean

@@ -237,12 +237,12 @@ def biproduct.is_colimit (F : J → C) [has_biproduct F] :
 (get_biproduct_data F).is_bilimit.is_colimit
 
 @[priority 100]
-instance has_product_of_has_biproduct [has_biproduct F] : has_limit (discrete.functor F) :=
+instance has_product_of_has_biproduct [has_biproduct F] : has_product F :=
 has_limit.mk { cone := (biproduct.bicone F).to_cone,
   is_limit := biproduct.is_limit F, }
 
 @[priority 100]
-instance has_coproduct_of_has_biproduct [has_biproduct F] : has_colimit (discrete.functor F) :=
+instance has_coproduct_of_has_biproduct [has_biproduct F] : has_coproduct F :=
 has_colimit.mk { cocone := (biproduct.bicone F).to_cocone,
   is_colimit := biproduct.is_colimit F, }
 
@@ -254,27 +254,40 @@ a limit and a colimit, with the same cone points,
 of every function `F : J → C`.
 -/
 class has_biproducts_of_shape : Prop :=
-(has_biproduct : Π F : J → C, has_biproduct F)
+(has_biproduct : ∀ F : J → C, has_biproduct F)
 
 attribute [instance, priority 100] has_biproducts_of_shape.has_biproduct
 
 /-- `has_finite_biproducts C` represents a choice of biproduct for every family of objects in `C`
 indexed by a finite type. -/
 class has_finite_biproducts : Prop :=
-(has_biproducts_of_shape : Π (J : Type) [fintype J],
-  has_biproducts_of_shape J C)
+(out [] : ∀ n, has_biproducts_of_shape (fin n) C)
 
-attribute [instance, priority 100] has_finite_biproducts.has_biproducts_of_shape
+variables {J}
+
+lemma has_biproducts_of_shape_of_equiv {K : Type w'} [has_biproducts_of_shape K C] (e : J ≃ K) :
+  has_biproducts_of_shape J C :=
+⟨λ F, let ⟨⟨h⟩⟩ := has_biproducts_of_shape.has_biproduct (F ∘ e.symm), ⟨c, hc⟩ := h
+  in has_biproduct.mk $ by simpa only [(∘), e.symm_apply_apply]
+    using limit_bicone.mk (c.whisker e) ((c.whisker_is_bilimit_iff _).2 hc)⟩
+
+@[priority 100] instance has_biproducts_of_shape_finite [has_finite_biproducts C] [finite J] :
+  has_biproducts_of_shape J C :=
+begin
+  rcases finite.exists_equiv_fin J with ⟨n, ⟨e⟩⟩,
+  haveI := has_finite_biproducts.out C n,
+  exact has_biproducts_of_shape_of_equiv C e
+end
 
 @[priority 100]
 instance has_finite_products_of_has_finite_biproducts [has_finite_biproducts C] :
   has_finite_products C :=
-{ out := λ J _, ⟨λ F, by exactI has_limit_of_iso discrete.nat_iso_functor.symm⟩ }
+{ out := λ n, ⟨λ F, has_limit_of_iso discrete.nat_iso_functor.symm⟩ }
 
 @[priority 100]
 instance has_finite_coproducts_of_has_finite_biproducts [has_finite_biproducts C] :
   has_finite_coproducts C :=
-{ out := λ J _, ⟨λ F, by exactI has_colimit_of_iso discrete.nat_iso_functor⟩ }
+{ out := λ n, ⟨λ F, has_colimit_of_iso discrete.nat_iso_functor⟩ }
 
 variables {J C}
 

src/category_theory/limits/shapes/finite_products.lean

@@ -23,31 +23,27 @@ variables (C : Type u) [category.{v} C]
 
 /--
 A category has finite products if there is a chosen limit for every diagram
-with shape `discrete J`, where we have `[fintype J]`.
+with shape `discrete J`, where we have `[finite J]`.
+
+We require this condition only for `J = fin n` in the definition, then deduce a version for any
+`J : Type*` as a corollary of this definition.
 -/
--- We can't simply make this an abbreviation, as we do with other `has_Xs` limits typeclasses,
--- because of https://github.com/leanprover-community/lean/issues/429
 class has_finite_products : Prop :=
-(out (J : Type) [fintype J] : has_limits_of_shape (discrete J) C)
-
-instance has_limits_of_shape_discrete
-  (J : Type) [finite J] [has_finite_products C] :
-  has_limits_of_shape (discrete J) C :=
-by { casesI nonempty_fintype J, haveI := @has_finite_products.out C _ _ J, apply_instance }
+(out [] (n : ℕ) : has_limits_of_shape (discrete (fin n)) C)
 
 /-- If `C` has finite limits then it has finite products. -/
 @[priority 10]
 instance has_finite_products_of_has_finite_limits [has_finite_limits C] :
   has_finite_products C :=
-⟨λ J 𝒥, by { resetI, apply_instance }⟩
+⟨λ n, infer_instance⟩
 
-instance has_fintype_products [has_finite_products C] (ι : Type w) [finite ι] :
+instance has_limits_of_shape_discrete [has_finite_products C] (ι : Type w) [finite ι] :
   has_limits_of_shape (discrete ι) C :=
-by casesI nonempty_fintype ι; exact
-has_limits_of_shape_of_equivalence
-  (discrete.equivalence
-    (equiv.ulift.{0}.trans
-      (fintype.equiv_fin ι).symm))
+begin
+  rcases finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩,
+  haveI := has_finite_products.out C n,
+  exact has_limits_of_shape_of_equivalence (discrete.equivalence e.symm)
+end
 
 /-- We can now write this for powers. -/
 noncomputable example [has_finite_products C] (X : C) : C := ∏ (λ (i : fin 5), X)
@@ -56,40 +52,38 @@ noncomputable example [has_finite_products C] (X : C) : C := ∏ (λ (i : fin 5)
 If a category has all products then in particular it has finite products.
 -/
 lemma has_finite_products_of_has_products [has_products.{w} C] : has_finite_products C :=
-⟨λ J _, has_limits_of_shape_of_equivalence (discrete.equivalence (equiv.ulift.{w}))⟩
+⟨λ n, has_limits_of_shape_of_equivalence (discrete.equivalence equiv.ulift.{w})⟩
 
 /--
 A category has finite coproducts if there is a chosen colimit for every diagram
 with shape `discrete J`, where we have `[fintype J]`.
+
+We require this condition only for `J = fin n` in the definition, then deduce a version for any
+`J : Type*` as a corollary of this definition.
 -/
 class has_finite_coproducts : Prop :=
-(out (J : Type) [fintype J] : has_colimits_of_shape (discrete J) C)
+(out [] (n : ℕ) : has_colimits_of_shape (discrete (fin n)) C)
 
 attribute [class] has_finite_coproducts
 
-instance has_colimits_of_shape_discrete
-  (J : Type) [finite J] [has_finite_coproducts C] :
-  has_colimits_of_shape (discrete J) C :=
-by { casesI nonempty_fintype J, haveI := @has_finite_coproducts.out C _ _ J, apply_instance }
+instance has_colimits_of_shape_discrete [has_finite_coproducts C] (ι : Type w) [finite ι] :
+  has_colimits_of_shape (discrete ι) C :=
+begin
+  rcases finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩,
+  haveI := has_finite_coproducts.out C n,
+  exact has_colimits_of_shape_of_equivalence (discrete.equivalence e.symm)
+end
 
 /-- If `C` has finite colimits then it has finite coproducts. -/
 @[priority 10]
 instance has_finite_coproducts_of_has_finite_colimits [has_finite_colimits C] :
   has_finite_coproducts C :=
-⟨λ J 𝒥, by { resetI, apply_instance }⟩
-
-instance has_fintype_coproducts [has_finite_coproducts C] (ι : Type w) [fintype ι] :
-  has_colimits_of_shape (discrete ι) C :=
-by casesI nonempty_fintype ι; exact
-has_colimits_of_shape_of_equivalence
-  (discrete.equivalence
-    (equiv.ulift.{0}.trans
-      (fintype.equiv_fin ι).symm))
+⟨λ J, by apply_instance⟩
 
 /--
 If a category has all coproducts then in particular it has finite coproducts.
 -/
 lemma has_finite_coproducts_of_has_coproducts [has_coproducts.{w} C] : has_finite_coproducts C :=
-⟨λ J _, has_colimits_of_shape_of_equivalence (discrete.equivalence (equiv.ulift.{w}))⟩
+⟨λ J, has_colimits_of_shape_of_equivalence (discrete.equivalence (equiv.ulift.{w}))⟩
 
 end category_theory.limits

src/category_theory/preadditive/Mat.lean

@@ -144,23 +144,23 @@ even though the construction we give uses a sigma type.
 See however `iso_biproduct_embedding`.
 -/
 instance has_finite_biproducts : has_finite_biproducts (Mat_ C) :=
-{ has_biproducts_of_shape := λ J 𝒟, by exactI
+{ out := λ n,
   { has_biproduct := λ f,
     has_biproduct_of_total
-    { X := ⟨Σ j : J, (f j).ι, λ p, (f p.1).X p.2⟩,
+    { X := ⟨Σ j, (f j).ι, λ p, (f p.1).X p.2⟩,
       π := λ j x y,
       begin
         dsimp at x ⊢,
         refine if h : x.1 = j then _ else 0,
-        refine if h' : (@eq.rec J x.1 (λ j, (f j).ι) x.2 _ h) = y then _ else 0,
+        refine if h' : (@eq.rec (fin n) x.1 (λ j, (f j).ι) x.2 _ h) = y then _ else 0,
         apply eq_to_hom,
         substs h h', -- Notice we were careful not to use `subst` until we had a goal in `Prop`.
       end,
       ι := λ j x y,
       begin
         dsimp at y ⊢,
         refine if h : y.1 = j then _ else 0,
-        refine if h' : (@eq.rec J y.1 (λ j, (f j).ι) y.2 _ h) = x then _ else 0,
+        refine if h' : (@eq.rec _ y.1 (λ j, (f j).ι) y.2 _ h) = x then _ else 0,
         apply eq_to_hom,
         substs h h',
       end,

src/category_theory/preadditive/biproducts.lean

@@ -171,12 +171,12 @@ has_biproduct.mk
 /-- A preadditive category with finite products has finite biproducts. -/
 lemma has_finite_biproducts.of_has_finite_products [has_finite_products C] :
   has_finite_biproducts C :=
-⟨λ J _, { has_biproduct := λ F, by exactI has_biproduct.of_has_product _ }⟩
+⟨λ n, { has_biproduct := λ F, has_biproduct.of_has_product _ }⟩
 
 /-- A preadditive category with finite coproducts has finite biproducts. -/
 lemma has_finite_biproducts.of_has_finite_coproducts [has_finite_coproducts C] :
   has_finite_biproducts C :=
-⟨λ J _, { has_biproduct := λ F, by exactI has_biproduct.of_has_coproduct _ }⟩
+⟨λ n, { has_biproduct := λ F, has_biproduct.of_has_coproduct _ }⟩
 
 section
 variables {f : J → C} [has_biproduct f]

src/representation_theory/Action.lean

@@ -207,12 +207,12 @@ def functor_category_equivalence : Action V G ≌ (single_obj G ⥤ V) :=
 attribute [simps] functor_category_equivalence
 
 instance [has_finite_products V] : has_finite_products (Action V G) :=
-{ out := λ J _, by exactI
-  adjunction.has_limits_of_shape_of_equivalence (Action.functor_category_equivalence _ _).functor }
+{ out := λ n, adjunction.has_limits_of_shape_of_equivalence
+    (Action.functor_category_equivalence _ _).functor }
 
 instance [has_finite_limits V] : has_finite_limits (Action V G) :=
-{ out := λ J _ _, by exactI
-  adjunction.has_limits_of_shape_of_equivalence (Action.functor_category_equivalence _ _).functor }
+{ out := λ J _ _, by exactI adjunction.has_limits_of_shape_of_equivalence
+    (Action.functor_category_equivalence _ _).functor }
 
 instance [has_limits V] : has_limits (Action V G) :=
 adjunction.has_limits_of_equivalence (Action.functor_category_equivalence _ _).functor

src/topology/sheaves/abelian.lean

@@ -36,7 +36,7 @@ instance : abelian (Cᵒᵖ ⥤ D) := @abelian.functor_category_abelian.{v} Cᵒ
 
 -- This also needs to be specified manually, but I don't know why.
 instance : has_finite_products (Sheaf J D) :=
-{ out := λ j ij, { has_limit := by { introI, apply_instance } } }
+{ out := λ j, { has_limit := λ F, by apply_instance } }
 
 -- sheafification assumptions
 variables [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), has_multiequalizer (S.index P)]