chore(category_theory/limits): minor changes in equalizers and products (#3603)

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

Author: kim-em

src/algebra/category/Group/abelian.lean

@@ -35,14 +35,9 @@ equivalence_reflects_normal_epi (forget₂ (Module ℤ) AddCommGroup).inv $
 
 end
 
-local attribute [instance] has_equalizers_of_has_finite_limits
-local attribute [instance] has_coequalizers_of_has_finite_colimits
-
 /-- The category of abelian groups is abelian. -/
 instance : abelian AddCommGroup :=
-{ has_finite_products := by apply_instance,
-  has_kernels := by apply_instance,
-  has_cokernels := by apply_instance,
+{ has_finite_products := by { dsimp [has_finite_products], apply_instance },
   normal_mono := λ X Y, normal_mono,
   normal_epi := λ X Y, normal_epi }
 

src/algebra/category/Module/abelian.lean

@@ -64,11 +64,9 @@ def normal_epi (hf : epi f) : normal_epi f :=
             (linear_map.quot_ker_equiv_range f)) (linear_equiv.of_top _ (range_eq_top_of_epi _)))) $
       by { ext, refl } }
 
-local attribute [instance] has_equalizers_of_has_finite_limits
-
 /-- The category of R-modules is abelian. -/
 instance : abelian (Module R) :=
-{ has_finite_products := by apply_instance,
+{ has_finite_products := by { dsimp [has_finite_products], apply_instance },
   has_kernels := by apply_instance,
   has_cokernels := has_cokernels_Module,
   normal_mono := λ X Y, normal_mono,

src/category_theory/abelian/non_preadditive.lean

@@ -271,16 +271,16 @@ section
 local attribute [instance] has_limit_parallel_pair
 
 /-- A `non_preadditive_abelian` category has all equalizers. -/
-@[priority 100] instance : has_equalizers C :=
+@[priority 100] instance has_equalizers : has_equalizers C :=
 has_equalizers_of_has_limit_parallel_pair _
 
 end
 
 section
 local attribute [instance] has_colimit_parallel_pair
 
-/-- A `non_preadditive_abelian` category as all coequalizers. -/
-@[priority 100] instance : has_coequalizers C :=
+/-- A `non_preadditive_abelian` category has all coequalizers. -/
+@[priority 100] instance has_coequalizers : has_coequalizers C :=
 has_coequalizers_of_has_colimit_parallel_pair _
 
 end

src/category_theory/limits/lattice.lean

@@ -17,22 +17,22 @@ variables {α : Type u}
 @[priority 100] -- see Note [lower instance priority]
 instance has_finite_limits_of_semilattice_inf_top [semilattice_inf_top α] :
   has_finite_limits α :=
-{ has_limits_of_shape := λ J 𝒥₁ 𝒥₂, by exactI
+λ J 𝒥₁ 𝒥₂, by exactI
   { has_limit := λ F,
     { cone :=
       { X := finset.univ.inf F.obj,
         π := { app := λ j, ⟨⟨finset.inf_le (fintype.complete _)⟩⟩ } },
-      is_limit := { lift := λ s, ⟨⟨finset.le_inf (λ j _, le_of_hom (s.π.app j))⟩⟩ } } } }
+      is_limit := { lift := λ s, ⟨⟨finset.le_inf (λ j _, (s.π.app j).down.down)⟩⟩ } } }
 
 @[priority 100] -- see Note [lower instance priority]
 instance has_finite_colimits_of_semilattice_sup_bot [semilattice_sup_bot α] :
   has_finite_colimits α :=
-{ has_colimits_of_shape := λ J 𝒥₁ 𝒥₂, by exactI
+λ J 𝒥₁ 𝒥₂, by exactI
   { has_colimit := λ F,
     { cocone :=
       { X := finset.univ.sup F.obj,
         ι := { app := λ i, ⟨⟨finset.le_sup (fintype.complete _)⟩⟩ } },
-      is_colimit := { desc := λ s, ⟨⟨finset.sup_le (λ j _, le_of_hom (s.ι.app j))⟩⟩ } } } }
+      is_colimit := { desc := λ s, ⟨⟨finset.sup_le (λ j _, (s.ι.app j).down.down)⟩⟩ } } }
 
 -- It would be nice to only use the `Inf` half of the complete lattice, but
 -- this seems not to have been described separately.

src/category_theory/limits/opposites.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Floris van Doorn
 -/
-import category_theory.limits.limits
+import category_theory.limits.shapes.products
 import category_theory.discrete_category
 
 universes v u
@@ -18,7 +18,10 @@ variables {C : Type u} [category.{v} C]
 variables {J : Type v} [small_category J]
 variable (F : J ⥤ Cᵒᵖ)
 
-instance has_limit_of_has_colimit_left_op [has_colimit F.left_op] : has_limit F :=
+/--
+If `F.left_op : Jᵒᵖ ⥤ C` has a chosen colimit, we can construct a chosen limit for `F : J ⥤ Cᵒᵖ`.
+-/
+def has_limit_of_has_colimit_left_op [has_colimit F.left_op] : has_limit F :=
 { cone := cone_of_cocone_left_op (colimit.cocone F.left_op),
   is_limit :=
   { lift := λ s, (colimit.desc F.left_op (cocone_left_op_of_cone s)).op,
@@ -41,14 +44,25 @@ instance has_limit_of_has_colimit_left_op [has_colimit F.left_op] : has_limit F
       refl,
     end } }
 
-instance has_limits_of_shape_op_of_has_colimits_of_shape [has_colimits_of_shape Jᵒᵖ C] :
+/--
+If `C` has chosen colimits of shape `Jᵒᵖ`, we can construct chosen limits in `Cᵒᵖ` of shape `J`.
+-/
+def has_limits_of_shape_op_of_has_colimits_of_shape [has_colimits_of_shape Jᵒᵖ C] :
   has_limits_of_shape J Cᵒᵖ :=
-{ has_limit := λ F, by apply_instance }
+{ has_limit := λ F, has_limit_of_has_colimit_left_op F }
+
+local attribute [instance] has_limits_of_shape_op_of_has_colimits_of_shape
 
-instance has_limits_op_of_has_colimits [has_colimits C] : has_limits Cᵒᵖ :=
+/--
+If `C` has chosen colimits, we can construct chosen limits for `Cᵒᵖ`.
+-/
+def has_limits_op_of_has_colimits [has_colimits C] : has_limits Cᵒᵖ :=
 { has_limits_of_shape := λ J 𝒥, by { resetI, apply_instance } }
 
-instance has_colimit_of_has_limit_left_op [has_limit F.left_op] : has_colimit F :=
+/--
+If `F.left_op : Jᵒᵖ ⥤ C` has a chosen limit, we can construct a chosen colimit for `F : J ⥤ Cᵒᵖ`.
+-/
+def has_colimit_of_has_limit_left_op [has_limit F.left_op] : has_colimit F :=
 { cocone := cocone_of_cone_left_op (limit.cone F.left_op),
   is_colimit :=
   { desc := λ s, (limit.lift F.left_op (cone_left_op_of_cocone s)).op,
@@ -68,27 +82,42 @@ instance has_colimit_of_has_limit_left_op [has_limit F.left_op] : has_colimit F
       refl,
     end } }
 
-instance has_colimits_of_shape_op_of_has_limits_of_shape [has_limits_of_shape Jᵒᵖ C] :
+/--
+If `C` has chosen colimits of shape `Jᵒᵖ`, we can construct chosen limits in `Cᵒᵖ` of shape `J`.
+-/
+def has_colimits_of_shape_op_of_has_limits_of_shape [has_limits_of_shape Jᵒᵖ C] :
   has_colimits_of_shape J Cᵒᵖ :=
-{ has_colimit := λ F, by apply_instance }
+{ has_colimit := λ F, has_colimit_of_has_limit_left_op F }
 
-instance has_colimits_op_of_has_limits [has_limits C] : has_colimits Cᵒᵖ :=
+local attribute [instance] has_colimits_of_shape_op_of_has_limits_of_shape
+
+/--
+If `C` has chosen limits, we can construct chosen colimits for `Cᵒᵖ`.
+-/
+def has_colimits_op_of_has_limits [has_limits C] : has_colimits Cᵒᵖ :=
 { has_colimits_of_shape := λ J 𝒥, by { resetI, apply_instance } }
 
 variables (X : Type v)
-instance has_coproducts_opposite [has_limits_of_shape (discrete X) C] :
-  has_colimits_of_shape (discrete X) Cᵒᵖ :=
+/--
+If `C` has products indexed by `X`, then `Cᵒᵖ` has coproducts indexed by `X`.
+-/
+def has_coproducts_opposite [has_products_of_shape X C] :
+  has_coproducts_of_shape X Cᵒᵖ :=
 begin
   haveI : has_limits_of_shape (discrete X)ᵒᵖ C :=
-    has_limits_of_shape_of_equivalence (discrete.opposite X).symm, apply_instance
+    has_limits_of_shape_of_equivalence (discrete.opposite X).symm,
+  apply_instance
 end
 
-instance has_products_opposite [has_colimits_of_shape (discrete X) C] :
-  has_limits_of_shape (discrete X) Cᵒᵖ :=
+/--
+If `C` has coproducts indexed by `X`, then `Cᵒᵖ` has products indexed by `X`.
+-/
+def has_products_opposite [has_coproducts_of_shape X C] :
+  has_products_of_shape X Cᵒᵖ :=
 begin
   haveI : has_colimits_of_shape (discrete X)ᵒᵖ C :=
-    has_colimits_of_shape_of_equivalence (discrete.opposite X).symm, apply_instance
+    has_colimits_of_shape_of_equivalence (discrete.opposite X).symm,
+  apply_instance
 end
 
-
 end category_theory.limits

src/category_theory/limits/shapes/binary_products.lean

@@ -402,24 +402,20 @@ end coprod_lemmas
 variables (C)
 
 /-- `has_binary_products` represents a choice of product for every pair of objects. -/
-class has_binary_products :=
-(has_limits_of_shape : has_limits_of_shape (discrete walking_pair) C)
+abbreviation has_binary_products := has_limits_of_shape (discrete walking_pair) C
 
 /-- `has_binary_coproducts` represents a choice of coproduct for every pair of objects. -/
-class has_binary_coproducts :=
-(has_colimits_of_shape : has_colimits_of_shape (discrete walking_pair) C)
-
-attribute [instance] has_binary_products.has_limits_of_shape has_binary_coproducts.has_colimits_of_shape
+abbreviation has_binary_coproducts := has_colimits_of_shape (discrete walking_pair) C
 
 /-- If `C` has all limits of diagrams `pair X Y`, then it has all binary products -/
 def has_binary_products_of_has_limit_pair [Π {X Y : C}, has_limit (pair X Y)] :
   has_binary_products C :=
-{ has_limits_of_shape := { has_limit := λ F, has_limit_of_iso (diagram_iso_pair F).symm } }
+{ has_limit := λ F, has_limit_of_iso (diagram_iso_pair F).symm }
 
 /-- If `C` has all colimits of diagrams `pair X Y`, then it has all binary coproducts -/
 def has_binary_coproducts_of_has_colimit_pair [Π {X Y : C}, has_colimit (pair X Y)] :
   has_binary_coproducts C :=
-{ has_colimits_of_shape := { has_colimit := λ F, has_colimit_of_iso (diagram_iso_pair F) } }
+{ has_colimit := λ F, has_colimit_of_iso (diagram_iso_pair F) }
 
 section prod_functor
 variables {C} [has_binary_products C]

src/category_theory/limits/shapes/biproducts.lean

@@ -123,20 +123,20 @@ 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 with decidable equality. -/
 class has_finite_biproducts :=
-(has_biproducts_of_shape : Π (J : Type v) [fintype J] [decidable_eq J],
+(has_biproducts_of_shape : Π (J : Type v) [decidable_eq J] [fintype J],
   has_biproducts_of_shape J C)
 
 attribute [instance, priority 100] has_finite_biproducts.has_biproducts_of_shape
 
 @[priority 100]
 instance has_finite_products_of_has_finite_biproducts [has_finite_biproducts C] :
   has_finite_products C :=
-⟨λ J _ _, ⟨λ F, by exactI has_limit_of_iso discrete.nat_iso_functor.symm⟩⟩
+λ J _ _, ⟨λ F, by exactI 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 :=
-⟨λ J _ _, ⟨λ F, by exactI has_colimit_of_iso discrete.nat_iso_functor⟩⟩
+λ J _ _, ⟨λ F, by exactI has_colimit_of_iso discrete.nat_iso_functor⟩
 
 variables {J C}
 
@@ -421,24 +421,14 @@ instance has_binary_biproduct.has_colimit_pair [has_binary_biproduct P Q] :
 { cocone := has_binary_biproduct.bicone.to_cocone,
   is_colimit := has_binary_biproduct.is_colimit, }
 
-@[priority 100]
-instance has_limits_of_shape_walking_pair [has_binary_biproducts C] :
-  has_limits_of_shape (discrete walking_pair) C :=
-{ has_limit := λ F, has_limit_of_iso (diagram_iso_pair F).symm }
-@[priority 100]
-instance has_colimits_of_shape_walking_pair [has_binary_biproducts C] :
-  has_colimits_of_shape (discrete walking_pair) C :=
-{ has_colimit := λ F, has_colimit_of_iso (diagram_iso_pair F) }
-
 @[priority 100]
 instance has_binary_products_of_has_binary_biproducts [has_binary_biproducts C] :
   has_binary_products C :=
-⟨by apply_instance⟩
-
+{ has_limit := λ F, has_limit_of_iso (diagram_iso_pair F).symm }
 @[priority 100]
 instance has_binary_coproducts_of_has_binary_biproducts [has_binary_biproducts C] :
   has_binary_coproducts C :=
-⟨by apply_instance⟩
+{ has_colimit := λ F, has_colimit_of_iso (diagram_iso_pair F) }
 
 /--
 The isomorphism between the specified binary product and the specified binary coproduct for
@@ -637,7 +627,7 @@ namespace category_theory.limits
 
 section preadditive
 variables {C : Type u} [category.{v} C] [preadditive C]
-variables {J : Type v} [fintype J] [decidable_eq J]
+variables {J : Type v} [decidable_eq J] [fintype J]
 
 open category_theory.preadditive
 open_locale big_operators

src/category_theory/limits/shapes/constructions/binary_products.lean

@@ -24,21 +24,20 @@ open category_theory category_theory.category category_theory.limits
 def has_binary_products_of_terminal_and_pullbacks
   (C : Type u) [𝒞 : category.{v} C] [has_terminal C] [has_pullbacks C] :
   has_binary_products C :=
-{ has_limits_of_shape :=
-  { has_limit := λ F,
-    { cone :=
-      { X := pullback (terminal.from (F.obj walking_pair.left))
-                      (terminal.from (F.obj walking_pair.right)),
-        π := discrete.nat_trans (λ x, walking_pair.cases_on x pullback.fst pullback.snd)},
-      is_limit :=
-      { lift := λ c, pullback.lift ((c.π).app walking_pair.left)
-                                   ((c.π).app walking_pair.right)
-                                   (subsingleton.elim _ _),
-        fac' := λ s c, walking_pair.cases_on c (limit.lift_π _ _) (limit.lift_π _ _),
-        uniq' := λ s m J,
-                 begin
-                   rw [←J, ←J],
-                   ext;
-                   rw limit.lift_π;
-                   refl
-                 end } } } }
+{ has_limit := λ F,
+  { cone :=
+    { X := pullback (terminal.from (F.obj walking_pair.left))
+                    (terminal.from (F.obj walking_pair.right)),
+      π := discrete.nat_trans (λ x, walking_pair.cases_on x pullback.fst pullback.snd)},
+    is_limit :=
+    { lift := λ c, pullback.lift ((c.π).app walking_pair.left)
+                                  ((c.π).app walking_pair.right)
+                                  (subsingleton.elim _ _),
+      fac' := λ s c, walking_pair.cases_on c (limit.lift_π _ _) (limit.lift_π _ _),
+      uniq' := λ s m J,
+                begin
+                  rw [←J, ←J],
+                  ext;
+                  rw limit.lift_π;
+                  refl
+                end } } }

src/category_theory/limits/shapes/constructions/equalizers.lean

@@ -75,9 +75,8 @@ open has_equalizers_of_pullbacks_and_binary_products
 -- This is not an instance, as it is not always how one wants to construct equalizers!
 def has_equalizers_of_pullbacks_and_binary_products :
   has_equalizers C :=
-{ has_limits_of_shape :=
-  { has_limit := λ F,
-    { cone := equalizer_cone F,
-      is_limit := equalizer_cone_is_limit F } } }
+{ has_limit := λ F,
+  { cone := equalizer_cone F,
+    is_limit := equalizer_cone_is_limit F } }
 
 end category_theory.limits

src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean

@@ -122,7 +122,7 @@ def limits_from_equalizers_and_products
 -- This is not an instance, as it is not always how one wants to construct finite limits!
 def finite_limits_from_equalizers_and_finite_products
   [has_finite_products C] [has_equalizers C] : has_finite_limits C :=
-{ has_limits_of_shape := λ J _ _, by exactI
-  { has_limit := λ F, has_limit.of_cones_iso (diagram F) F (cones_iso F) } }
+λ J _ _, by exactI
+  { has_limit := λ F, has_limit.of_cones_iso (diagram F) F (cones_iso F) }
 
 end category_theory.limits