[WIP] Add biproduct infrastructure for additive categories

theories/Categories/Additive/Biproducts.v

@@ -0,0 +1,199 @@
+(** * Biproducts in categories with zero objects
+
+    Objects that are simultaneously products and coproducts, fundamental
+    to additive category theory.
+*)
+
+From HoTT Require Import Basics Types.
+From HoTT.Categories Require Import Category Functor.
+From HoTT.Categories.Additive Require Import ZeroObjects.
+
+(** * Biproduct structures *)
+
+(** ** Biproduct data
+
+    The data of a biproduct consists of an object together with injection
+    and projection morphisms.
+*)
+
+Record BiproductData {C : PreCategory} (X Y : object C)
+  : Type
+  := {
+  biproduct_obj : object C;
+
+  (* Coproduct structure: injections *)
+  inl : morphism C X biproduct_obj;
+  inr : morphism C Y biproduct_obj;
+
+  (* Product structure: projections *)
+  outl : morphism C biproduct_obj X;
+  outr : morphism C biproduct_obj Y
+}.
+
+Coercion biproduct_obj : BiproductData >-> object.
+
+Arguments biproduct_obj {C X Y} b : rename.
+Arguments inl {C X Y} b : rename.
+Arguments inr {C X Y} b : rename.
+Arguments outl {C X Y} b : rename.
+Arguments outr {C X Y} b : rename.
+
+(** ** Biproduct axioms
+
+    The axioms that make biproduct data into an actual biproduct.
+    These ensure the projection-injection pairs behave correctly.
+*)
+
+Record IsBiproduct {C : PreCategory} `{Z : ZeroObject C} {X Y : object C} 
+                   (B : BiproductData X Y)
+  : Type
+  := {
+  (* Projection-injection identities *)
+  beta_l : (outl B o inl B = 1)%morphism;
+  beta_r : (outr B o inr B = 1)%morphism;
+
+  (* Mixed terms are zero *)
+  mixed_l : (outl B o inr B)%morphism = zero_morphism Y X;
+  mixed_r : (outr B o inl B)%morphism = zero_morphism X Y
+}.
+
+Arguments beta_l {C Z X Y B} i : rename.
+Arguments beta_r {C Z X Y B} i : rename.
+Arguments mixed_l {C Z X Y B} i : rename.
+Arguments mixed_r {C Z X Y B} i : rename.
+
+(** ** Universal property of biproducts
+
+    The universal property states that morphisms into/out of the biproduct
+    are uniquely determined by their components.
+*)
+
+Record HasBiproductUniversal {C : PreCategory} {X Y : object C}
+  (B : BiproductData X Y)
+  : Type
+  := {
+  (* Universal property as a coproduct *)
+  coprod_universal : forall (W : object C) 
+    (f : morphism C X W) (g : morphism C Y W),
+    Contr {h : morphism C B W & 
+           ((h o inl B = f)%morphism * (h o inr B = g)%morphism)};
+
+  (* Universal property as a product *)
+  prod_universal : forall (W : object C) 
+    (f : morphism C W X) (g : morphism C W Y),
+    Contr {h : morphism C W B & 
+           ((outl B o h = f)%morphism * (outr B o h = g)%morphism)}
+}.
+
+Arguments coprod_universal {C X Y B} u W f g : rename.
+Arguments prod_universal {C X Y B} u W f g : rename.
+
+(** ** Complete biproduct structure
+
+    A biproduct is biproduct data together with the proof that it satisfies
+    the biproduct axioms and universal property.
+*)
+
+Class Biproduct {C : PreCategory} `{Z : ZeroObject C} (X Y : object C)
+  : Type
+  := {
+  biproduct_data : BiproductData X Y;
+  biproduct_is : IsBiproduct biproduct_data;
+  biproduct_universal : HasBiproductUniversal biproduct_data
+}.
+
+Coercion biproduct_data : Biproduct >-> BiproductData.
+
+Arguments biproduct_data {C Z X Y} b : rename.
+Arguments biproduct_is {C Z X Y} b : rename.
+Arguments biproduct_universal {C Z X Y} b : rename.
+
+(** * Biproduct operations *)
+
+Section BiproductOperations.
+  Context {C : PreCategory} `{Z : ZeroObject C} {X Y : object C}.
+  Variable (B : Biproduct X Y).
+
+  (** ** Uniqueness from universal property *)
+
+  (** Extract the unique morphism from the coproduct universal property. *)
+  Definition biproduct_coprod_mor (W : object C) 
+    (f : morphism C X W) (g : morphism C Y W)
+    : morphism C (biproduct_data B) W
+    := pr1 (@center _ (coprod_universal (biproduct_universal B) W f g)).
+
+  Lemma biproduct_coprod_beta_l (W : object C) 
+    (f : morphism C X W) (g : morphism C Y W)
+    : (biproduct_coprod_mor W f g o inl (biproduct_data B) = f)%morphism.
+  Proof.
+    unfold biproduct_coprod_mor.
+    set (c := @center _ (coprod_universal (biproduct_universal B) W f g)).
+    destruct c as [h [Hl Hr]].
+    exact Hl.
+  Qed.
+
+  Lemma biproduct_coprod_beta_r (W : object C) 
+    (f : morphism C X W) (g : morphism C Y W)
+    : (biproduct_coprod_mor W f g o inr (biproduct_data B) = g)%morphism.
+  Proof.
+    unfold biproduct_coprod_mor.
+    set (c := @center _ (coprod_universal (biproduct_universal B) W f g)).
+    destruct c as [h [Hl Hr]].
+    exact Hr.
+  Qed.
+
+  (** Extract the unique morphism from the product universal property. *)
+  Definition biproduct_prod_mor (W : object C) 
+    (f : morphism C W X) (g : morphism C W Y)
+    : morphism C W (biproduct_data B)
+    := pr1 (@center _ (prod_universal (biproduct_universal B) W f g)).
+
+  Lemma biproduct_prod_beta_l (W : object C) 
+    (f : morphism C W X) (g : morphism C W Y)
+    : (outl (biproduct_data B) o biproduct_prod_mor W f g = f)%morphism.
+  Proof.
+    unfold biproduct_prod_mor.
+    set (c := @center _ (prod_universal (biproduct_universal B) W f g)).
+    destruct c as [h [Hl Hr]].
+    exact Hl.
+  Qed.
+
+  Lemma biproduct_prod_beta_r (W : object C) 
+    (f : morphism C W X) (g : morphism C W Y)
+    : (outr (biproduct_data B) o biproduct_prod_mor W f g = g)%morphism.
+  Proof.
+    unfold biproduct_prod_mor.
+    set (c := @center _ (prod_universal (biproduct_universal B) W f g)).
+    destruct c as [h [Hl Hr]].
+    exact Hr.
+  Qed.
+
+  (** ** Uniqueness properties *)
+
+  Lemma biproduct_coprod_unique (W : object C) 
+    (f : morphism C X W) (g : morphism C Y W)
+    (h : morphism C (biproduct_data B) W)
+    : (h o inl (biproduct_data B) = f)%morphism -> 
+      (h o inr (biproduct_data B) = g)%morphism ->
+      h = biproduct_coprod_mor W f g.
+  Proof.
+    intros Hl Hr.
+    unfold biproduct_coprod_mor.
+    set (c := @center _ (coprod_universal (biproduct_universal B) W f g)).
+    assert (p : (h; (Hl, Hr)) = c).
+    1: apply (@path_contr _ (coprod_universal (biproduct_universal B) W f g)).
+    exact (ap pr1 p).
+  Qed.
+
+End BiproductOperations.
+
+(** * Export hints *)
+
+Hint Resolve 
+  biproduct_coprod_beta_l biproduct_coprod_beta_r
+  biproduct_prod_beta_l biproduct_prod_beta_r
+  : biproduct.
+
+Hint Rewrite 
+  @zero_morphism_left @zero_morphism_right
+  : biproduct_simplify.