feat(category/limits/shapes): fix biproducts (#3175)

This is a second attempt at #3102.

Previously the definition of a (binary) biproduct in a category with zero morphisms (but not necessarily) preadditive was just wrong.

The definition for a "bicone" was just something that was simultaneously a cone and a cocone, with the same cone points. It was a "biproduct bicone" if the cone was a limit cone and the cocone was a colimit cocone. However, this definition was not particularly useful. In particular, there was no way to prove that the two different `map` constructions providing a morphism `W ⊞ X ⟶ Y ⊞ Z` (i.e. by treating the biproducts either as cones, or as cocones) were actually equal. Blech.

So, I've added the axioms `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q` to `bicone P Q`. (Note these only require the exist of zero morphisms, not preadditivity.)

Now the two map constructions are equal.

I've then entirely removed the `has_preadditive_biproduct` typeclass. Instead we have
1. additional theorems providing `total`, when `preadditive C` is available
2. alternative constructors for `has_biproduct` that use `total` rather than `is_limit` and `is_colimit`.

This PR also introduces some abbreviations along the lines of `abbreviation has_binary_product (X Y : C) := has_limit (pair X Y)`, just to improve readability.



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

Author: kim-em

src/algebra/category/Group/biproducts.lean

@@ -33,8 +33,8 @@ instance has_limit_pair (G H : AddCommGroup.{u}) : has_limit.{u} (pair G H) :=
       ext; [rw ← w walking_pair.left, rw ← w walking_pair.right]; refl,
     end, } }
 
-instance (G H : AddCommGroup.{u}) : has_preadditive_binary_biproduct.{u} G H :=
-has_preadditive_binary_biproduct.of_has_limit_pair _ _
+instance (G H : AddCommGroup.{u}) : has_binary_biproduct.{u} G H :=
+has_binary_biproduct.of_has_binary_product _ _
 
 -- We verify that the underlying type of the biproduct we've just defined is definitionally
 -- the cartesian product of the underlying types:
@@ -140,13 +140,19 @@ open has_limit has_colimit
 
 variables [decidable_eq J] [fintype J]
 
-instance : has_bilimit F :=
+instance (f : J → AddCommGroup.{u}) : has_biproduct f :=
 { bicone :=
-  { X := AddCommGroup.of (Π j, F.obj j),
-    ι := discrete.nat_trans (λ j, add_monoid_hom.single (λ j, F.obj j) j),
-    π := discrete.nat_trans (λ j, add_monoid_hom.apply (λ j, F.obj j) j), },
-  is_limit := limit.is_limit F,
-  is_colimit := colimit.is_colimit F, }.
+  { X := AddCommGroup.of (Π j, f j),
+    ι := λ j, add_monoid_hom.single (λ j, f j) j,
+    π := λ j, add_monoid_hom.apply (λ j, f j) j,
+    ι_π := λ j j',
+    begin
+      ext, split_ifs,
+      { subst h, simp, },
+      { rw [eq_comm] at h, simp [h], },
+    end, },
+  is_limit := limit.is_limit (discrete.functor f),
+  is_colimit := colimit.is_colimit (discrete.functor f), }.
 
 -- We verify that the underlying type of the biproduct we've just defined is definitionally
 -- the dependent function type:

src/category_theory/abelian/basic.lean

@@ -326,7 +326,7 @@ end
 
 section
 local attribute [instance] preadditive.has_coequalizers_of_has_cokernels
-local attribute [instance] has_preadditive_binary_biproducts_of_has_binary_products
+local attribute [instance] has_binary_biproducts.of_has_binary_products
 
 /-- Any abelian category has pushouts -/
 def has_pushouts : has_pushouts.{v} C :=
@@ -337,7 +337,7 @@ end
 namespace pullback_to_biproduct_is_kernel
 variables [limits.has_pullbacks.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
 
-local attribute [instance] has_preadditive_binary_biproducts_of_has_binary_products
+local attribute [instance] has_binary_biproducts.of_has_binary_products
 
 /-! This section contains a slightly technical result about pullbacks and biproducts.
     We will need it in the proof that the pullback of an epimorphism is an epimorpism. -/
@@ -362,7 +362,7 @@ def is_limit_pullback_to_biproduct : is_limit (pullback_to_biproduct_fork f g) :
 fork.is_limit.mk _
   (λ s, pullback.lift (fork.ι s ≫ biprod.fst) (fork.ι s ≫ biprod.snd) $
     sub_eq_zero.1 $ by rw [category.assoc, category.assoc, ←comp_sub, sub_eq_add_neg, ←comp_neg,
-      biprod.fst_add_snd, kernel_fork.condition s])
+      ←biprod.desc_eq, kernel_fork.condition s])
   (λ s,
   begin
     ext; rw [fork.ι_of_ι, category.assoc],
@@ -376,7 +376,7 @@ end pullback_to_biproduct_is_kernel
 namespace biproduct_to_pushout_is_cokernel
 variables [limits.has_pushouts.{v} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
 
-local attribute [instance] has_preadditive_binary_biproducts_of_has_binary_products
+local attribute [instance] has_binary_biproducts.of_has_binary_products
 
 /-- The canonical map `Y ⊞ Z ⟶ pushout f g` -/
 abbreviation biproduct_to_pushout : Y ⊞ Z ⟶ pushout f g :=
@@ -394,7 +394,7 @@ def is_colimit_biproduct_to_pushout : is_colimit (biproduct_to_pushout_cofork f
 cofork.is_colimit.mk _
   (λ s, pushout.desc (biprod.inl ≫ cofork.π s) (biprod.inr ≫ cofork.π s) $
     sub_eq_zero.1 $ by rw [←category.assoc, ←category.assoc, ←sub_comp, sub_eq_add_neg, ←neg_comp,
-      biprod.inl_add_inr, cofork.condition s, has_zero_morphisms.zero_comp])
+      ←biprod.lift_eq, cofork.condition s, has_zero_morphisms.zero_comp])
   (λ s, by ext; simp)
   (λ s m h, by ext; simp [cofork.π_eq_app_one, ←h walking_parallel_pair.one] )
 
@@ -403,7 +403,7 @@ end biproduct_to_pushout_is_cokernel
 section epi_pullback
 variables [limits.has_pullbacks.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
 
-local attribute [instance] has_preadditive_binary_biproducts_of_has_binary_products
+local attribute [instance] has_binary_biproducts.of_has_binary_products
 
 /-- In an abelian category, the pullback of an epimorphism is an epimorphism.
     Proof from [aluffi2016, IX.2.3], cf. [borceux-vol2, 1.7.6] -/
@@ -479,7 +479,7 @@ end epi_pullback
 section mono_pushout
 variables [limits.has_pushouts.{v} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
 
-local attribute [instance] has_preadditive_binary_biproducts_of_has_binary_products
+local attribute [instance] has_binary_biproducts.of_has_binary_products
 
 instance mono_pushout_of_mono_f [mono f] : mono (pushout.inr : Z ⟶ pushout f g) :=
 mono_of_cancel_zero _ $ λ R e h,

src/category_theory/limits/shapes/binary_products.lean

@@ -38,6 +38,34 @@ instance fintype_walking_pair : fintype walking_pair :=
 { elems := {left, right},
   complete := λ x, by { cases x; simp } }
 
+/--
+The equivalence swapping left and right.
+-/
+def walking_pair.swap : walking_pair ≃ walking_pair :=
+{ to_fun := λ j, walking_pair.rec_on j right left,
+  inv_fun := λ j, walking_pair.rec_on j right left,
+  left_inv := λ j, by { cases j; refl, },
+  right_inv := λ j, by { cases j; refl, }, }
+
+@[simp] lemma walking_pair.swap_apply_left : walking_pair.swap left = right := rfl
+@[simp] lemma walking_pair.swap_apply_right : walking_pair.swap right = left := rfl
+@[simp] lemma walking_pair.swap_symm_apply_tt : walking_pair.swap.symm left = right := rfl
+@[simp] lemma walking_pair.swap_symm_apply_ff : walking_pair.swap.symm right = left := rfl
+
+/--
+An equivalence from `walking_pair` to `bool`, sometimes useful when reindexing limits.
+-/
+def walking_pair.equiv_bool : walking_pair ≃ bool :=
+{ to_fun := λ j, walking_pair.rec_on j tt ff, -- to match equiv.sum_equiv_sigma_bool
+  inv_fun := λ b, bool.rec_on b right left,
+  left_inv := λ j, by { cases j; refl, },
+  right_inv := λ b, by { cases b; refl, }, }
+
+@[simp] lemma walking_pair.equiv_bool_apply_left : walking_pair.equiv_bool left = tt := rfl
+@[simp] lemma walking_pair.equiv_bool_apply_right : walking_pair.equiv_bool right = ff := rfl
+@[simp] lemma walking_pair.equiv_bool_symm_apply_tt : walking_pair.equiv_bool.symm tt = left := rfl
+@[simp] lemma walking_pair.equiv_bool_symm_apply_ff : walking_pair.equiv_bool.symm ff = right := rfl
+
 variables {C : Type u} [category.{v} C]
 
 /-- The diagram on the walking pair, sending the two points to `X` and `Y`. -/
@@ -143,109 +171,114 @@ def binary_cofan.is_colimit.desc' {W X Y : C} {s : binary_cofan X Y} (h : is_col
   (g : Y ⟶ W) : {l : s.X ⟶ W // s.inl ≫ l = f ∧ s.inr ≫ l = g} :=
 ⟨h.desc $ binary_cofan.mk f g, h.fac _ _, h.fac _ _⟩
 
+/-- An abbreviation for `has_limit (pair X Y)`. -/
+abbreviation has_binary_product (X Y : C) := has_limit (pair X Y)
+/-- An abbreviation for `has_colimit (pair X Y)`. -/
+abbreviation has_binary_coproduct (X Y : C) := has_colimit (pair X Y)
+
 /-- If we have chosen a product of `X` and `Y`, we can access it using `prod X Y` or
     `X ⨯ Y`. -/
-abbreviation prod (X Y : C) [has_limit (pair X Y)] := limit (pair X Y)
+abbreviation prod (X Y : C) [has_binary_product X Y] := limit (pair X Y)
 
 /-- If we have chosen a coproduct of `X` and `Y`, we can access it using `coprod X Y ` or
     `X ⨿ Y`. -/
-abbreviation coprod (X Y : C) [has_colimit (pair X Y)] := colimit (pair X Y)
+abbreviation coprod (X Y : C) [has_binary_coproduct X Y] := colimit (pair X Y)
 
 notation X ` ⨯ `:20 Y:20 := prod X Y
 notation X ` ⨿ `:20 Y:20 := coprod X Y
 
 /-- The projection map to the first component of the product. -/
-abbreviation prod.fst {X Y : C} [has_limit (pair X Y)] : X ⨯ Y ⟶ X :=
+abbreviation prod.fst {X Y : C} [has_binary_product X Y] : X ⨯ Y ⟶ X :=
 limit.π (pair X Y) walking_pair.left
 
 /-- The projecton map to the second component of the product. -/
-abbreviation prod.snd {X Y : C} [has_limit (pair X Y)] : X ⨯ Y ⟶ Y :=
+abbreviation prod.snd {X Y : C} [has_binary_product X Y] : X ⨯ Y ⟶ Y :=
 limit.π (pair X Y) walking_pair.right
 
 /-- The inclusion map from the first component of the coproduct. -/
-abbreviation coprod.inl {X Y : C} [has_colimit (pair X Y)] : X ⟶ X ⨿ Y :=
+abbreviation coprod.inl {X Y : C} [has_binary_coproduct X Y] : X ⟶ X ⨿ Y :=
 colimit.ι (pair X Y) walking_pair.left
 
 /-- The inclusion map from the second component of the coproduct. -/
-abbreviation coprod.inr {X Y : C} [has_colimit (pair X Y)] : Y ⟶ X ⨿ Y :=
+abbreviation coprod.inr {X Y : C} [has_binary_coproduct X Y] : Y ⟶ X ⨿ Y :=
 colimit.ι (pair X Y) walking_pair.right
 
-@[ext] lemma prod.hom_ext {W X Y : C} [has_limit (pair X Y)] {f g : W ⟶ X ⨯ Y}
+@[ext] lemma prod.hom_ext {W X Y : C} [has_binary_product X Y] {f g : W ⟶ X ⨯ Y}
   (h₁ : f ≫ prod.fst = g ≫ prod.fst) (h₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g :=
 binary_fan.is_limit.hom_ext (limit.is_limit _) h₁ h₂
 
-@[ext] lemma coprod.hom_ext {W X Y : C} [has_colimit (pair X Y)] {f g : X ⨿ Y ⟶ W}
+@[ext] lemma coprod.hom_ext {W X Y : C} [has_binary_coproduct X Y] {f g : X ⨿ Y ⟶ W}
   (h₁ : coprod.inl ≫ f = coprod.inl ≫ g) (h₂ : coprod.inr ≫ f = coprod.inr ≫ g) : f = g :=
 binary_cofan.is_colimit.hom_ext (colimit.is_colimit _) h₁ h₂
 
 /-- If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y`
     induces a morphism `prod.lift f g : W ⟶ X ⨯ Y`. -/
-abbreviation prod.lift {W X Y : C} [has_limit (pair X Y)] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⨯ Y :=
+abbreviation prod.lift {W X Y : C} [has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⨯ Y :=
 limit.lift _ (binary_fan.mk f g)
 
 /-- If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and
     `g : Y ⟶ W` induces a morphism `coprod.desc f g : X ⨿ Y ⟶ W`. -/
-abbreviation coprod.desc {W X Y : C} [has_colimit (pair X Y)] (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ Y ⟶ W :=
+abbreviation coprod.desc {W X Y : C} [has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ Y ⟶ W :=
 colimit.desc _ (binary_cofan.mk f g)
 
 @[simp, reassoc]
-lemma prod.lift_fst {W X Y : C} [has_limit (pair X Y)] (f : W ⟶ X) (g : W ⟶ Y) :
+lemma prod.lift_fst {W X Y : C} [has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) :
   prod.lift f g ≫ prod.fst = f :=
 limit.lift_π _ _
 
 @[simp, reassoc]
-lemma prod.lift_snd {W X Y : C} [has_limit (pair X Y)] (f : W ⟶ X) (g : W ⟶ Y) :
+lemma prod.lift_snd {W X Y : C} [has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) :
   prod.lift f g ≫ prod.snd = g :=
 limit.lift_π _ _
 
 /- The redundant simp lemma linter says that simp can prove the reassoc version of this lemma. -/
 @[reassoc, simp]
-lemma prod.lift_comp_comp {V W X Y : C} [has_limit (pair X Y)] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
+lemma prod.lift_comp_comp {V W X Y : C} [has_binary_product X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
   prod.lift (f ≫ g) (f ≫ h) = f ≫ prod.lift g h :=
 by tidy
 
 @[simp, reassoc]
-lemma coprod.inl_desc {W X Y : C} [has_colimit (pair X Y)] (f : X ⟶ W) (g : Y ⟶ W) :
+lemma coprod.inl_desc {W X Y : C} [has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
   coprod.inl ≫ coprod.desc f g = f :=
 colimit.ι_desc _ _
 
 @[simp, reassoc]
-lemma coprod.inr_desc {W X Y : C} [has_colimit (pair X Y)] (f : X ⟶ W) (g : Y ⟶ W) :
+lemma coprod.inr_desc {W X Y : C} [has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
   coprod.inr ≫ coprod.desc f g = g :=
 colimit.ι_desc _ _
 
 /- The redundant simp lemma linter says that simp can prove the reassoc version of this lemma. -/
 @[reassoc, simp]
-lemma coprod.desc_comp_comp {V W X Y : C} [has_colimit (pair X Y)] (f : V ⟶ W) (g : X ⟶ V)
+lemma coprod.desc_comp_comp {V W X Y : C} [has_binary_coproduct X Y] (f : V ⟶ W) (g : X ⟶ V)
   (h : Y ⟶ V) : coprod.desc (g ≫ f) (h ≫ f) = coprod.desc g h ≫ f :=
 by tidy
 
-instance prod.mono_lift_of_mono_left {W X Y : C} [has_limit (pair X Y)] (f : W ⟶ X) (g : W ⟶ Y)
+instance prod.mono_lift_of_mono_left {W X Y : C} [has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y)
   [mono f] : mono (prod.lift f g) :=
 mono_of_mono_fac $ prod.lift_fst _ _
 
-instance prod.mono_lift_of_mono_right {W X Y : C} [has_limit (pair X Y)] (f : W ⟶ X) (g : W ⟶ Y)
+instance prod.mono_lift_of_mono_right {W X Y : C} [has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y)
   [mono g] : mono (prod.lift f g) :=
 mono_of_mono_fac $ prod.lift_snd _ _
 
-instance coprod.epi_desc_of_epi_left {W X Y : C} [has_colimit (pair X Y)] (f : X ⟶ W) (g : Y ⟶ W)
+instance coprod.epi_desc_of_epi_left {W X Y : C} [has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W)
   [epi f] : epi (coprod.desc f g) :=
 epi_of_epi_fac $ coprod.inl_desc _ _
 
-instance coprod.epi_desc_of_epi_right {W X Y : C} [has_colimit (pair X Y)] (f : X ⟶ W) (g : Y ⟶ W)
+instance coprod.epi_desc_of_epi_right {W X Y : C} [has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W)
   [epi g] : epi (coprod.desc f g) :=
 epi_of_epi_fac $ coprod.inr_desc _ _
 
 /-- If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y`
     induces a morphism `l : W ⟶ X ⨯ Y` satisfying `l ≫ prod.fst = f` and `l ≫ prod.snd = g`. -/
-def prod.lift' {W X Y : C} [has_limit (pair X Y)] (f : W ⟶ X) (g : W ⟶ Y) :
+def prod.lift' {W X Y : C} [has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) :
   {l : W ⟶ X ⨯ Y // l ≫ prod.fst = f ∧ l ≫ prod.snd = g} :=
 ⟨prod.lift f g, prod.lift_fst _ _, prod.lift_snd _ _⟩
 
 /-- If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and
     `g : Y ⟶ W` induces a morphism `l : X ⨿ Y ⟶ W` satisfying `coprod.inl ≫ l = f` and
     `coprod.inr ≫ l = g`. -/
-def coprod.desc' {W X Y : C} [has_colimit (pair X Y)] (f : X ⟶ W) (g : Y ⟶ W) :
+def coprod.desc' {W X Y : C} [has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
   {l : X ⨿ Y ⟶ W // coprod.inl ≫ l = f ∧ coprod.inr ≫ l = g} :=
 ⟨coprod.desc f g, coprod.inl_desc _ _, coprod.inr_desc _ _⟩
 
@@ -255,12 +288,41 @@ abbreviation prod.map {W X Y Z : C} [has_limits_of_shape.{v} (discrete walking_p
   (f : W ⟶ Y) (g : X ⟶ Z) : W ⨯ X ⟶ Y ⨯ Z :=
 lim.map (map_pair f g)
 
+/-- If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
+    `g : X ≅ Z` induces a isomorphism `prod.map_iso f g : W ⨯ X ≅ Y ⨯ Z`. -/
+abbreviation prod.map_iso {W X Y Z : C} [has_limits_of_shape.{v} (discrete walking_pair) C]
+  (f : W ≅ Y) (g : X ≅ Z) : W ⨯ X ≅ Y ⨯ Z :=
+lim.map_iso (map_pair_iso f g)
+
+-- Note that the next two `simp` lemmas are proved by `simp`,
+-- but nevertheless are useful,
+-- because they state the right hand side in terms of `prod.map`
+-- rather than `lim.map`.
+@[simp] lemma prod.map_iso_hom {W X Y Z : C} [has_limits_of_shape.{v} (discrete walking_pair) C]
+  (f : W ≅ Y) (g : X ≅ Z) : (prod.map_iso f g).hom = prod.map f.hom g.hom := by simp
+
+@[simp] lemma prod.map_iso_inv {W X Y Z : C} [has_limits_of_shape.{v} (discrete walking_pair) C]
+  (f : W ≅ Y) (g : X ≅ Z) : (prod.map_iso f g).inv = prod.map f.inv g.inv := by simp
+
 /-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of morphisms `f : W ⟶ Y` and
     `g : W ⟶ Z` induces a morphism `coprod.map f g : W ⨿ X ⟶ Y ⨿ Z`. -/
 abbreviation coprod.map {W X Y Z : C} [has_colimits_of_shape.{v} (discrete walking_pair) C]
   (f : W ⟶ Y) (g : X ⟶ Z) : W ⨿ X ⟶ Y ⨿ Z :=
 colim.map (map_pair f g)
 
+/-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
+    `g : W ≅ Z` induces a isomorphism `coprod.map_iso f g : W ⨿ X ≅ Y ⨿ Z`. -/
+abbreviation coprod.map_iso {W X Y Z : C} [has_colimits_of_shape.{v} (discrete walking_pair) C]
+  (f : W ≅ Y) (g : X ≅ Z) : W ⨿ X ≅ Y ⨿ Z :=
+colim.map_iso (map_pair_iso f g)
+
+@[simp] lemma coprod.map_iso_hom {W X Y Z : C} [has_colimits_of_shape.{v} (discrete walking_pair) C]
+  (f : W ≅ Y) (g : X ≅ Z) : (coprod.map_iso f g).hom = coprod.map f.hom g.hom := by simp
+
+@[simp] lemma coprod.map_iso_inv {W X Y Z : C} [has_colimits_of_shape.{v} (discrete walking_pair) C]
+  (f : W ≅ Y) (g : X ≅ Z) : (coprod.map_iso f g).inv = coprod.map f.inv g.inv := by simp
+
+
 section prod_lemmas
 variable [has_limits_of_shape.{v} (discrete walking_pair) C]