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/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.
 
@@ -313,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/Categorical/MonoidObject.v

@@ -98,7 +98,7 @@ Section ComonoidObject.
   (** Coassociativity *)
   Definition co_coassoc {x : A} `{!IsComonoidObject x}
     : associator x x x $o fmap01 tensor x co_comult $o co_comult
-        $== fmap10 tensor co_comult x $o co_comult.
+      $== fmap10 tensor co_comult x $o co_comult.
   Proof.
     refine (cat_assoc _ _ _ $@ _).
     apply cate_moveR_Me.
@@ -146,11 +146,12 @@ Section ComonoidObject.
     - exact cco_cocomm.
   Defined.
 
-  Global Instance co_cco {x : A} `{!IsCocommutativeComonoidObject x}
+  Definition co_cco {x : A} `{!IsCocommutativeComonoidObject x}
     : IsComonoidObject x.
   Proof.
     apply cmo_mo.
   Defined.
+  Hint Immediate co_cco : typeclass_instances.
 
   (** Cocommutativity *)
   Definition cco_cocomm {x : A} `{!IsCocommutativeComonoidObject x}
@@ -200,7 +201,7 @@ Defined.
 
 (** ** Monoid enrichment *)
 
-(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. Equivalently, a hom [x $-> y] in a cartesian category where [x] is a comonoid object has the structure of a monoid. *)
+(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. *)
 
 Section MonoidEnriched.
   Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}
@@ -210,28 +211,29 @@ Section MonoidEnriched.
   Section Monoid.
     Context `{!IsMonoidObject _ _ y}.
 
-    Local Instance sgop_hom : SgOp (x $-> y)
+    Local Instance sgop_hom_mo : SgOp (x $-> y)
       := fun f g => mo_mult $o cat_binprod_corec f g.
 
-    Local Instance monunit_hom : MonUnit (x $-> y) := mo_unit $o mor_terminal _ _.
+    Local Instance monunit_hom_mo : MonUnit (x $-> y)
+      := mo_unit $o mor_terminal _ _.
 
-    Local Instance associative_hom : Associative sgop_hom.
+    Local Instance associative_hom_mo : Associative sgop_hom_mo.
     Proof.
       intros f g h.
-      unfold sgop_hom.
+      unfold sgop_hom_mo.
       rapply path_hom.
       refine ((_ $@L cat_binprod_fmap01_corec _ _ _)^$ $@ _).
       nrefine (cat_assoc_opp _ _ _ $@ _).
-      refine ((mo_assoc $@R _)^$ $@ _).
       nrefine (_ $@ (_ $@L cat_binprod_fmap10_corec _ _ _)).
+      refine ((mo_assoc $@R _)^$ $@ _).
       refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc _ _ _).
       nrapply cat_binprod_associator_corec.
     Defined.
 
-    Local Instance leftidentity_hom : LeftIdentity sgop_hom mon_unit.
+    Local Instance leftidentity_hom_mo : LeftIdentity sgop_hom_mo mon_unit.
     Proof.
       intros f.
-      unfold sgop_hom, mon_unit.
+      unfold sgop_hom_mo, mon_unit.
       rapply path_hom.
       refine ((_ $@L (cat_binprod_fmap10_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
       nrefine (((mo_left_unit $@ _) $@R _) $@ _).
@@ -243,29 +245,30 @@ Section MonoidEnriched.
       nrapply cat_binprod_beta_pr2.
     Defined.
 
-    Local Instance rightidentity_hom : RightIdentity sgop_hom mon_unit.
+    Local Instance rightidentity_hom_mo : RightIdentity sgop_hom_mo mon_unit.
     Proof.
       intros f.
-      unfold sgop_hom, mon_unit.
+      unfold sgop_hom_mo, mon_unit.
       rapply path_hom.
-      refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
+      refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$)
+        $@ cat_assoc_opp _ _ _ $@ _).
       nrefine (((mo_right_unit $@ _) $@R _) $@ _).
       1: nrapply cate_buildequiv_fun.
       nrapply cat_binprod_beta_pr1.
     Defined.
 
-    Local Instance issemigroup_hom : IsSemiGroup (x $-> y) := {}.
-    Local Instance ismonoid_hom : IsMonoid (x $-> y) := {}.
+    Local Instance issemigroup_hom_mo : IsSemiGroup (x $-> y) := {}.
+    Local Instance ismonoid_hom_mo : IsMonoid (x $-> y) := {}.
 
   End Monoid.
 
   Context `{!IsCommutativeMonoidObject _ _ y}.
-  Local Existing Instances sgop_hom monunit_hom ismonoid_hom.
+  Local Existing Instances sgop_hom_mo monunit_hom_mo ismonoid_hom_mo.
 
-  Local Instance commutative_hom : Commutative sgop_hom.
+  Local Instance commutative_hom : Commutative sgop_hom_mo.
   Proof.
     intros f g.
-    unfold sgop_hom.
+    unfold sgop_hom_mo.
     rapply path_hom.
     refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _ $@ (cmo_comm $@R _)).
     nrapply cat_binprod_swap_corec. 

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);
+}.
+