biproducts, additive and abelian categories

theories/Algebra/AbGroups/AbHom.v

@@ -1,6 +1,8 @@
 Require Import Basics Types.
 Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import AbelianGroup Biproduct.
+Require Import Algebra.Groups.Group.
+Require Import Algebra.Homological.Additive.
 
 (** * Homomorphisms from a group to an abelian group form an abelian group. *)
 
@@ -117,3 +119,27 @@ Proof.
   rapply (conn_map_elim (Tr (-1)) f).
   exact (equiv_path_grouphomomorphism^-1 p).
 Defined.
+
+(** ** Additivity of AbGroup *)
+
+(** The group operation that is induced from the semiadditive structure agrees with the handcrafted operation on hom at the level of the underlying functions. *)  
+Definition ab_homo_add_is_semiadditive_add `{Funext}
+  {A B : AbGroup} (f g : A $-> B)
+  : ab_homo_add f g = sgop_hom A B f g :> (A -> B)
+  := 1.
+
+(** AbGroup is an additive category. *)
+Global Instance additive_ab `{Funext} : IsAdditive AbGroup.
+Proof.
+  snrapply Build_IsAdditive.
+  - exact _.
+  - exact _.
+  - intros A B f.
+    snrapply equiv_path_grouphomomorphism.
+    intros x.
+    exact (left_inverse (f x)).
+  - intros A B f.
+    snrapply equiv_path_grouphomomorphism.
+    intros x.
+    exact (right_inverse (f x)).
+Defined.

theories/Algebra/AbGroups/AbPushout.v

@@ -71,7 +71,7 @@ Proof.
   srapply path_sigma_hprop.
   refine (grp_quotient_rec_beta _ Y _ _ @ _).
   apply equiv_path_grouphomomorphism; intro bc.
-  exact (ab_biprod_rec_beta' (phi $o grp_quotient_map) bc).
+  exact (ab_biprod_rec_eta (phi $o grp_quotient_map) bc).
 Defined.
 
 (** Restricting [ab_pushout_rec] along [ab_pushout_inl] recovers the left inducing map. *)

theories/Algebra/AbGroups/Biproduct.v

@@ -3,6 +3,8 @@ Require Import WildCat.
 Require Import HSet.
 Require Import AbelianGroup.
 Require Import Modalities.ReflectiveSubuniverse.
+Require Import Algebra.Homological.Biproducts.
+Require Import Algebra.Homological.Additive.
 
 Local Open Scope mc_add_scope.
 
@@ -47,7 +49,7 @@ Proof.
   intros [f g]. exact (ab_biprod_rec f g).
 Defined.
 
-Proposition ab_biprod_rec_beta' {A B Y : AbGroup}
+Proposition ab_biprod_rec_eta {A B Y : AbGroup}
             (u : ab_biprod A B $-> Y)
   : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) == u.
 Proof.
@@ -58,29 +60,19 @@ Proof.
   - exact (left_identity b).
 Defined.
 
-Proposition ab_biprod_rec_beta `{Funext} {A B Y : AbGroup}
-            (u : ab_biprod A B $-> Y)
-  : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) = u.
-Proof.
-  apply equiv_path_grouphomomorphism.
-  exact (ab_biprod_rec_beta' u).
-Defined.
-
-Proposition ab_biprod_rec_inl_beta `{Funext} {A B Y : AbGroup}
+Proposition ab_biprod_rec_inl_beta {A B Y : AbGroup}
             (a : A $-> Y) (b : B $-> Y)
-  : (ab_biprod_rec a b) $o ab_biprod_inl = a.
+  : (ab_biprod_rec a b) $o ab_biprod_inl == a.
 Proof.
-  apply equiv_path_grouphomomorphism.
   intro x; simpl.
   rewrite (grp_homo_unit b).
   exact (right_identity (a x)).
 Defined.
 
-Proposition ab_biprod_rec_inr_beta `{Funext} {A B Y : AbGroup}
+Proposition ab_biprod_rec_inr_beta {A B Y : AbGroup}
             (a : A $-> Y) (b : B $-> Y)
-  : (ab_biprod_rec a b) $o ab_biprod_inr = b.
+  : (ab_biprod_rec a b) $o ab_biprod_inr == b.
 Proof.
-  apply equiv_path_grouphomomorphism.
   intro y; simpl.
   rewrite (grp_homo_unit a).
   exact (left_identity (b y)).
@@ -93,19 +85,22 @@ Proof.
   - intro phi.
     exact (phi $o ab_biprod_inl, phi $o ab_biprod_inr).
   - intro phi.
-    exact (ab_biprod_rec_beta phi).
+    apply equiv_path_grouphomomorphism.
+    exact (ab_biprod_rec_eta phi).
   - intros [a b].
     apply path_prod.
-    + apply ab_biprod_rec_inl_beta.
-    + apply ab_biprod_rec_inr_beta.
+    + apply equiv_path_grouphomomorphism.
+      apply ab_biprod_rec_inl_beta.
+    + apply equiv_path_grouphomomorphism.
+      apply ab_biprod_rec_inr_beta.
 Defined.
 
 (** Corecursion principle, inherited from Groups/Group.v. *)
 Definition ab_biprod_corec {A B X : AbGroup} (f : X $-> A) (g : X $-> B)
   : X $-> ab_biprod A B
   := grp_prod_corec f g.
 
-Definition ab_corec_beta {X Y A B : AbGroup} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
+Definition ab_corec_eta {X Y A B : AbGroup} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
   : ab_biprod_corec g0 g1 $o f $== ab_biprod_corec (g0 $o f) (g1 $o f)
   := fun _ => idpath.
 
@@ -190,17 +185,26 @@ Proof.
   - exact (left_identity _)^.
 Defined.
 
+Lemma ab_biprod_corec_eta' {A B X : AbGroup} (f g : ab_biprod A B $-> X)
+  : (f $o ab_biprod_inl $== g $o ab_biprod_inl)
+  -> (f $o ab_biprod_inr $== g $o ab_biprod_inr)
+  -> f $== g.
+Proof.
+  intros h k.
+  intros [a b].
+  refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
+  refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
+  exact (ap011 (+) (h a) (k b)).
+Defined.
+
 (* Maps out of biproducts are determined on the two inclusions. *)
 Lemma equiv_path_biprod_corec `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
   : ((phi $o ab_biprod_inl == psi $o ab_biprod_inl) * (phi $o ab_biprod_inr == psi $o ab_biprod_inr))
       <~> phi == psi.
 Proof.
   apply equiv_iff_hprop.
   - intros [h k].
-    intros [a b].
-    refine (ap phi (ab_biprod_decompose _ _) @ _ @ ap psi (ab_biprod_decompose _ _)^).
-    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-    exact (ap011 (+) (h a) (k b)).
+    apply ab_biprod_corec_eta'; assumption.
   - intro h.
     exact (fun a => h _, fun b => h _).
 Defined.
@@ -311,3 +315,30 @@ Proof.
   refine (abgroup_commutative _ _ _ @ _).
   exact (ap (fun a =>  a + snd x) (abgroup_commutative _ _ _)).
 Defined.
+
+(** ** AbGroup has binary biproducts *)
+
+Global Instance hasbinarybiproducts_ab : HasBinaryBiproducts AbGroup.
+Proof.
+  intros A B.
+  snrapply Build_BinaryBiproduct.
+  - exact (ab_biprod A B).
+  - exact ab_biprod_pr1.
+  - exact ab_biprod_pr2.
+  - exact (fun _ => ab_biprod_corec).
+  - exact (fun _ f _ => Id f).
+  - exact (fun _ _ g => Id g).
+  - exact (fun _ _ _ p q a => path_prod' (p a) (q a)).
+  - exact ab_biprod_inl.
+  - exact ab_biprod_inr.
+  - exact (fun _ => ab_biprod_rec).
+  - exact (fun _ => ab_biprod_rec_inl_beta).
+  - exact (fun _ => ab_biprod_rec_inr_beta).
+  - exact (fun _ => ab_biprod_corec_eta').
+  - cbn; reflexivity.
+  - cbn; reflexivity.
+  - cbn; reflexivity.
+  - cbn; reflexivity.
+Defined.
+
+Global Instance issemiadditive_ab `{Funext} : IsSemiAdditive AbGroup := {}.

theories/Algebra/AbSES/Core.v

@@ -625,7 +625,7 @@ Proposition projection_split_beta {B A : AbGroup} (E : AbSES B A)
   : projection_split_iso E h o (inclusion _) == ab_biprod_inl.
 Proof.
   intro a.
-  refine (ap _ (ab_corec_beta _ _ _ _) @ _).
+  refine (ap _ (ab_corec_eta _ _ _ _) @ _).
   refine (ab_biprod_functor_beta _ _ _ _ _ @ _).
   nrapply path_prod'.
   2: rapply cx_isexact.

theories/Algebra/Homological/Abelian.v

@@ -0,0 +1,143 @@
+Require Import Basics.Overture Basics.Tactics Basics.Equivalences.
+Require Import WildCat.Core WildCat.Equiv WildCat.PointedCat WildCat.Opposite.
+Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring.
+Require Import Algebra.Homological.Additive.
+Require Import canonical_names.
+
+(** * Abelian Categories *)
+
+Local Open Scope mc_scope.
+Local Open Scope mc_add_scope.
+
+(** ** Kernels and cokernels *)
+
+(** *** Kernels *)
+
+Class Kernel {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) := {
+  cat_ker_obj : A;
+  cat_ker : cat_ker_obj $-> a;
+
+  cat_ker_zero : f $o cat_ker $== zero_morphism;
+
+  cat_ker_corec {x} (g : x $-> a) : f $o g $== zero_morphism -> x $-> cat_ker_obj;
+
+  cat_ker_corec_beta {x} (g : x $-> a) (p : f $o g $== zero_morphism)
+    : cat_ker $o cat_ker_corec g p $== g;
+
+  monic_cat_ker : Monic cat_ker;
+}.
+
+Arguments cat_ker_obj {A _ _ _ _ _ a b} f {_}.
+Arguments cat_ker_corec {A _ _ _ _ _ a b f _ x} g p.
+Arguments cat_ker {A _ _ _ _ _ a b} f {_}.
+Arguments cat_ker_zero {A _ _ _ _ _ a b} f {_}.
+Arguments monic_cat_ker {A _ _ _ _ _ a b} f {_}.
+
+(** Kernels of monomorphisms are zero. *)
+Definition ker_zero_monic {A : Type} `{IsPointedCat A}
+  {a b : A} (f : a $-> b) `{!Kernel f}
+  : Monic f -> cat_ker f $== zero_morphism.
+Proof.
+  intros monic.
+  nrapply monic.
+  refine (cat_ker_zero f $@ _^$).
+  apply cat_zero_r.
+Defined.
+
+(** Maps with zero kernel are monic. *)
+Definition monic_ker_zero {A : Type} `{IsAdditive A}
+  {a b : A} (f : a $-> b) `{!Kernel f}
+  : cat_ker f $== zero_morphism -> Monic f.
+Proof.
+  intros ker_zero c g h p.
+  nrapply GpdHom_path.
+  apply path_hom in p.
+  change (@paths (AbHom c a) g h).
+  change (@paths (AbHom c b) (f $o g) (f $o h)) in p.
+  apply grp_moveL_1M.
+  apply grp_moveL_1M in p.
+  apply GpdHom_path in p.
+  apply path_hom.
+  refine ((cat_ker_corec_beta (g + (-h)) _)^$ $@ (ker_zero $@R _) $@ cat_zero_l _).
+  refine (addcat_dist_l _ _ _ $@ _ $@ p).
+  apply GpdHom_path.
+  f_ap.
+  apply path_hom.
+  symmetry.
+  nrapply addcat_comp_negate_r.
+Defined.
+
+(** *** Cokernels *)
+
+Class Cokernel {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b)
+  := cokernel_kernel_op :: Kernel (A := A^op) (f : Hom (A:= A^op) b a).
+
+Arguments Cokernel {A _ _ _ _ _ a b} f.
+
+Definition cat_coker_obj {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b)
+  `{!Cokernel f} : A
+  := cat_ker_obj (A:=A^op) (a:=b) f.
+
+Definition cat_coker {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b)
+  `{!Cokernel f} : b $-> cat_coker_obj f
+  := cat_ker (A:=A^op) (a:=b) (b:=a) f.
+
+Definition cat_coker_zero {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b)
+  `{!Cokernel f} : cat_coker f $o f $== zero_morphism
+  := cat_ker_zero (A:=A^op) (a:=b) f.
+
+Definition cat_coker_rec {A : Type} `{IsPointedCat A} {a b : A} {f : a $-> b}
+  `{!Cokernel f} {x} (g : b $-> x)
+  : g $o f $== zero_morphism -> cat_coker_obj f $-> x
+  := cat_ker_corec (A:=A^op) (a:=b) (b:=a) g.
+
+Definition cat_coker_rec_beta {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b)
+  `{!Cokernel f} {x} (g : b $-> x) (p : g $o f $== zero_morphism)
+  : cat_coker_rec g p $o cat_coker f $== g
+  := cat_ker_corec_beta (A:=A^op) (a:=b) (b:=a) g p.
+
+Definition epic_cat_coker {A : Type} `{IsPointedCat A}
+  {a b : A} (f : a $-> b) `{!Cokernel f}
+  : Epic (cat_coker f)
+  := monic_cat_ker (A:=A^op) (a:=b) (b:=a) f.
+
+Definition coker_zero_epic {A : Type} `{IsPointedCat A}
+  {a b : A} (f : a $-> b) `{!Cokernel f}
+  : Epic f -> cat_coker f $== zero_morphism
+  := ker_zero_monic (A:=A^op) (a:=b) f.
+
+Definition epic_coker_zero {A : Type} `{IsAdditive A}
+  {a b : A} (f : a $-> b) {k : Cokernel f}
+  : cat_coker f $== zero_morphism -> Epic f
+  := monic_ker_zero (A:=A^op) (a:=b) (b:=a) f.
+
+(** ** Preabelian categories *)
+
+Class IsPreAbelian {A : Type} `{IsAdditive A} := {
+  preabelian_has_kernels :: forall {a b : A} (f : a $-> b), Kernel f;
+  preabelian_has_cokernels :: forall {a b : A} (f : a $-> b), Cokernel f;
+}.
+
+Definition cat_coker_ker_ker_coker {A : Type} `{IsPreAbelian A}
+  {a b : A} (f : a $-> b)
+  : cat_coker_obj (cat_ker f) $-> cat_ker_obj (cat_coker f).
+Proof.
+  snrapply cat_coker_rec.
+  - snrapply cat_ker_corec.
+    + exact f.
+    + nrapply cat_coker_zero.
+  - snrapply monic_cat_ker.
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    refine ((_ $@R _) $@ _).
+    1: nrapply cat_ker_corec_beta.
+    refine (_ $@ (cat_zero_r _)^$).
+    nrapply cat_ker_zero.
+Defined.
+
+(** ** Abelian categories *)
+
+Class IsAbelian {A : Type} `{IsPreAbelian A} := {
+  catie_preabelian_canonical_map : forall a b (f : a $-> b),
+    CatIsEquiv (cat_coker_ker_ker_coker f);
+}.
+