feat(category_theory): preadditive binary biproducts (leanprover-comm…

…unity#2747)

This PR introduces "preadditive binary biproducts", which correspond to the second definition of biproducts given in leanprover-community#2177.

* Preadditive binary biproducts are binary biproducts.
* In a preadditive category, a binary product is a preadditive binary biproduct.
* This directly implies that `AddCommGroup` has preadditive binary biproducts. The existence of binary coproducts in `AddCommGroup` is then a consequence of abstract nonsense.

src/algebra/category/Group/biproducts.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.Group.basic
+import algebra.category.Group.preadditive
 import category_theory.limits.shapes.biproducts
 import algebra.pi_instances
 
@@ -32,34 +33,16 @@ 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 has_colimit_pair (G H : AddCommGroup.{u}) : has_colimit.{u} (pair G H) :=
-{ cocone :=
-  { X := AddCommGroup.of (G × H),
-    ι := { app := λ j, walking_pair.cases_on j (add_monoid_hom.inl G H) (add_monoid_hom.inr G H) }},
-  is_colimit :=
-  { desc := λ s, add_monoid_hom.coprod (s.ι.app walking_pair.left) (s.ι.app walking_pair.right),
-    fac' := by { rintros s (⟨⟩|⟨⟩); { ext x, dsimp, simp, } },
-    uniq' := λ s m w,
-    begin
-      ext,
-      rw [←w, ←w],
-      simp [←add_monoid_hom.map_add],
-    end, }, }
-
-instance (G H : AddCommGroup.{u}) : has_binary_biproduct.{u} G H :=
-{ bicone :=
-  { X := AddCommGroup.of (G × H),
-    π₁ := add_monoid_hom.fst G H,
-    π₂ := add_monoid_hom.snd G H,
-    ι₁ := add_monoid_hom.inl G H,
-    ι₂ := add_monoid_hom.inr G H, },
-  is_limit := limit.is_limit (pair G H),
-  is_colimit := colimit.is_colimit (pair G H), }
+instance (G H : AddCommGroup.{u}) : has_preadditive_binary_biproduct.{u} G H :=
+has_preadditive_binary_biproduct.of_has_limit_pair _ _
 
 -- We verify that the underlying type of the biproduct we've just defined is definitionally
 -- the cartesian product of the underlying types:
 example (G H : AddCommGroup.{u}) : ((G ⊞ H : AddCommGroup.{u}) : Type u) = (G × H) := rfl
 
+-- Furthermore, our biproduct will automatically function as a coproduct.
+example (G H : AddCommGroup.{u}) : has_colimit.{u} (pair G H) := by apply_instance
+
 variables {J : Type u} (F : (discrete J) ⥤ AddCommGroup.{u})
 
 namespace has_limit

src/category_theory/limits/shapes/biproducts.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import category_theory.epi_mono
 import category_theory.limits.shapes.binary_products
+import category_theory.preadditive
 
 /-!
 # Biproducts and binary biproducts
@@ -31,8 +32,10 @@ and iso `limit F ≅ colimit F`, and produces `has_bilimit F`.
 
 TODO: perhaps it makes sense to unify the treatment of zero objects with this a bit.
 
-TODO: later, in pre-additive categories, we should give the equational characterisation
-of biproducts.
+In addition to biproducts and binary biproducts, we define the notion of preadditive binary
+biproduct, which is a preadditive version of binary biproducts. We show that a preadditive binary
+biproduct is a binary biproduct and construct preadditive binary biproducts both from binary
+products and from binary coproducts.
 
 ## Notation
 As `⊕` is already taken for the sum of types, we introduce the notation `X ⊞ Y` for
@@ -314,4 +317,131 @@ instance biprod.snd_epi {X Y : C} [has_binary_biproduct.{v} X Y] :
 -- If someone is interested, they could provide the constructions:
 --   has_binary_biproducts ↔ has_finite_biproducts
 
+section preadditive
+variables [preadditive.{v} C]
+
+open category_theory.preadditive
+
+/-- A preadditive binary biproduct is a bicone on two objects `X` and `Y` satisfying a set of five
+    axioms expressing the properties of a biproduct in additive terms. The notion of preadditive
+    binary biproduct is strictly stronger than the notion of binary biproduct (but it in any
+    preadditive category, the existence of a binary biproduct implies the existence of a
+    preadditive binary biproduct: a biproduct is, in particular, a product, and every product gives
+    rise to a preadditive binary biproduct, see `has_preadditive_binary_biproduct.of_has_limit_pair`). -/
+class has_preadditive_binary_biproduct (X Y : C) :=
+(bicone : binary_bicone.{v} X Y)
+(ι₁_π₁' : bicone.ι₁ ≫ bicone.π₁ = 𝟙 X . obviously)
+(ι₂_π₂' : bicone.ι₂ ≫ bicone.π₂ = 𝟙 Y . obviously)
+(ι₂_π₁' : bicone.ι₂ ≫ bicone.π₁ = 0 . obviously)
+(ι₁_π₂' : bicone.ι₁ ≫ bicone.π₂ = 0 . obviously)
+(total' : bicone.π₁ ≫ bicone.ι₁ + bicone.π₂ ≫ bicone.ι₂ = 𝟙 bicone.X . obviously)
+
+restate_axiom has_preadditive_binary_biproduct.ι₁_π₁'
+restate_axiom has_preadditive_binary_biproduct.ι₂_π₂'
+restate_axiom has_preadditive_binary_biproduct.ι₂_π₁'
+restate_axiom has_preadditive_binary_biproduct.ι₁_π₂'
+restate_axiom has_preadditive_binary_biproduct.total'
+attribute [simp, reassoc] has_preadditive_binary_biproduct.ι₁_π₁
+  has_preadditive_binary_biproduct.ι₂_π₂ has_preadditive_binary_biproduct.ι₂_π₁
+  has_preadditive_binary_biproduct.ι₁_π₂
+attribute [simp] has_preadditive_binary_biproduct.total
+
+section
+local attribute [tidy] tactic.case_bash
+
+/-- A preadditive binary biproduct is a binary biproduct. -/
+@[priority 100]
+instance (X Y : C) [has_preadditive_binary_biproduct.{v} X Y] : has_binary_biproduct.{v} X Y :=
+{ bicone := has_preadditive_binary_biproduct.bicone,
+  is_limit :=
+  { lift := λ s, binary_fan.fst s ≫ has_preadditive_binary_biproduct.bicone.ι₁ +
+      binary_fan.snd s ≫ has_preadditive_binary_biproduct.bicone.ι₂,
+    uniq' := λ s m h, by erw [←category.comp_id m, ←has_preadditive_binary_biproduct.total,
+      comp_add, reassoc_of (h walking_pair.left), reassoc_of (h walking_pair.right)] },
+  is_colimit :=
+  { desc := λ s, has_preadditive_binary_biproduct.bicone.π₁ ≫ binary_cofan.inl s +
+      has_preadditive_binary_biproduct.bicone.π₂ ≫ binary_cofan.inr s,
+    uniq' := λ s m h, by erw [←category.id_comp m, ←has_preadditive_binary_biproduct.total,
+      add_comp, category.assoc, category.assoc, h walking_pair.left, h walking_pair.right] } }
+
+end
+
+section
+variables (X Y : C) [has_preadditive_binary_biproduct.{v} X Y]
+
+@[simp, reassoc] lemma biprod.inl_fst : (biprod.inl : X ⟶ X ⊞ Y) ≫ biprod.fst = 𝟙 X :=
+has_preadditive_binary_biproduct.ι₁_π₁
+@[simp, reassoc] lemma biprod.inr_snd : (biprod.inr : Y ⟶ X ⊞ Y) ≫ biprod.snd = 𝟙 Y :=
+has_preadditive_binary_biproduct.ι₂_π₂
+@[simp, reassoc] lemma biprod.inr_fst : (biprod.inr : Y ⟶ X ⊞ Y) ≫ biprod.fst = 0 :=
+has_preadditive_binary_biproduct.ι₂_π₁
+@[simp, reassoc] lemma biprod.inl_snd : (biprod.inl : X ⟶ X ⊞ Y) ≫ biprod.snd = 0 :=
+has_preadditive_binary_biproduct.ι₁_π₂
+@[simp] lemma biprod.total : biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y) :=
+has_preadditive_binary_biproduct.total
+
+lemma biprod.inl_add_inr {T : C} {f : T ⟶ X} {g : T ⟶ Y} :
+  f ≫ biprod.inl + g ≫ biprod.inr = biprod.lift f g := rfl
+
+lemma biprod.fst_add_snd {T : C} {f : X ⟶ T} {g : Y ⟶ T} :
+  biprod.fst ≫ f + biprod.snd ≫ g = biprod.desc f g := rfl
+
+@[simp, reassoc] lemma biprod.lift_desc {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} :
+  biprod.lift f g ≫ biprod.desc h i = f ≫ h + g ≫ i :=
+by simp [←biprod.inl_add_inr, ←biprod.fst_add_snd]
+
+end
+
+section has_limit_pair
+
+/-- In a preadditive category, if the product of `X` and `Y` exists, then the preadditive binary
+    biproduct of `X` and `Y` exists. -/
+def has_preadditive_binary_biproduct.of_has_limit_pair (X Y : C) [has_limit.{v} (pair X Y)] :
+  has_preadditive_binary_biproduct.{v} X Y :=
+{ bicone :=
+  { X := X ⨯ Y,
+    π₁ := category_theory.limits.prod.fst,
+    π₂ := category_theory.limits.prod.snd,
+    ι₁ := prod.lift (𝟙 X) 0,
+    ι₂ := prod.lift 0 (𝟙 Y) } }
+
+/-- In a preadditive category, if the coproduct of `X` and `Y` exists, then the preadditive binary
+    biproduct of `X` and `Y` exists. -/
+def has_preadditive_binary_biproduct.of_has_colimit_pair (X Y : C) [has_colimit.{v} (pair X Y)] :
+  has_preadditive_binary_biproduct.{v} X Y :=
+{ bicone :=
+  { X := X ⨿ Y,
+    π₁ := coprod.desc (𝟙 X) 0,
+    π₂ := coprod.desc 0 (𝟙 Y),
+    ι₁ := category_theory.limits.coprod.inl,
+    ι₂ := category_theory.limits.coprod.inr } }
+
+end has_limit_pair
+
+section
+variable (C)
+
+/-- A preadditive category `has_preadditive_binary_biproducts` if the preadditive binary biproduct
+    exists for every pair of objects. -/
+class has_preadditive_binary_biproducts :=
+(has_preadditive_binary_biproduct : Π (X Y : C), has_preadditive_binary_biproduct.{v} X Y)
+
+attribute [instance, priority 100] has_preadditive_binary_biproducts.has_preadditive_binary_biproduct
+
+/-- If a preadditive category has all binary products, then it has all preadditive binary
+    biproducts. -/
+def has_preadditive_binary_biproducts_of_has_binary_products [has_binary_products.{v} C] :
+  has_preadditive_binary_biproducts.{v} C :=
+⟨λ X Y, has_preadditive_binary_biproduct.of_has_limit_pair X Y⟩
+
+/-- If a preadditive category has all binary coproducts, then it has all preadditive binary
+    biproducts. -/
+def has_preadditive_binary_biproducts_of_has_binary_coproducts [has_binary_coproducts.{v} C] :
+  has_preadditive_binary_biproducts.{v} C :=
+⟨λ X Y, has_preadditive_binary_biproduct.of_has_colimit_pair X Y⟩
+
+end
+
+end preadditive
+
 end category_theory.limits