tensor preserves coequalizers

Signed-off-by: Ali Caglayan <[email protected]>

theories/Algebra/AbGroups/AbHom.v

@@ -54,6 +54,16 @@ Proof.
   snrapply grp_quotient_map.
 Defined.
 
+Definition ab_coeq_glue {A B} {f g : A $-> B}
+  : ab_coeq_in (f:=f) (g:=g) $o f $== ab_coeq_in $o g.
+Proof.
+  intros x.
+  nrapply qglue.
+  apply tr.
+  exists x.
+  apply ab_comm.
+Defined.
+
 Definition ab_coeq_rec {A B : AbGroup} {f g : A $-> B}
   {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g) 
   : ab_coeq f g $-> C.
@@ -85,6 +95,74 @@ Proof.
   exact i.
 Defined.
 
+Definition ab_coeq_ind_homotopy {A B C f g}
+  {l r : @ab_coeq A B f g $-> C}
+  (p : l $o ab_coeq_in $== r $o ab_coeq_in) 
+  : l $== r.
+Proof.
+  srapply ab_coeq_ind_hprop.
+  exact p.
+Defined.
+
+Definition functor_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
+  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
+  : ab_coeq f g $-> ab_coeq f' g'.
+Proof.
+  snrapply ab_coeq_rec.
+  1: exact (ab_coeq_in $o b).
+  refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
+  refine ((_ $@L p^$) $@ _ $@ (_ $@L q)).
+  refine (cat_assoc_opp _ _ _ $@ (_ $@R a) $@ cat_assoc _ _ _).
+  nrapply ab_coeq_glue.
+Defined.
+
+Definition functor2_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
+  {a a' : A $-> A'} {b b' : B $-> B'}
+  (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
+  (p' : f' $o a' $== b' $o f) (q' : g' $o a' $== b' $o g)
+  (s : b $== b')
+  : functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'.
+Proof.
+  snrapply ab_coeq_ind_homotopy.
+  intros x.
+  exact (ap ab_coeq_in (s x)).
+Defined.
+
+Definition functor_ab_coeq_compose {A B} {f g : A $-> B}
+  {A' B'} {f' g' : A' $-> B'} 
+  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
+  {A'' B''} {f'' g'' : A'' $-> B''}
+  (a' : A' $-> A'') (b' : B' $-> B'')
+  (p' : f'' $o a' $== b' $o f') (q' : g'' $o a' $== b' $o g')
+  : functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q
+  $== functor_ab_coeq (a' $o a) (b' $o b) (hconcat p p') (hconcat q q').
+Proof.
+  snrapply ab_coeq_ind_homotopy.
+  simpl; reflexivity.
+Defined.
+
+Definition functor_ab_coeq_id {A B} (f g : A $-> B)
+  : functor_ab_coeq (f:=f) (g:=g) (Id _) (Id _) (hrefl _) (hrefl _) $== Id _.
+Proof.
+  snrapply ab_coeq_ind_homotopy.
+  reflexivity.
+Defined.
+
+Definition grp_iso_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
+  (a : A $<~> A') (b : B $<~> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
+  : ab_coeq f g $<~> ab_coeq f' g'.
+Proof.
+  snrapply cate_adjointify.
+  - exact (functor_ab_coeq a b p q).
+  - exact (functor_ab_coeq a^-1$ b^-1$ (hinverse _ _ p) (hinverse _ _ q)).
+  - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
+      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
+    rapply cate_isretr.
+  - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
+      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
+    rapply cate_issect.
+Defined.
+
 (** ** The bifunctor [ab_hom] *)
 
 Global Instance is0functor_ab_hom01 `{Funext} {A : Group^op}

theories/Algebra/AbGroups/TensorProduct.v

@@ -688,4 +688,56 @@ Global Instance issymmmetricmonoidal_ab_tensor_prod
   : IsSymmetricMonoidal AbGroup ab_tensor_prod abgroup_Z
   := {}.
 
+(** ** Preservation of Coequalizers *)
+
+(** The tensor product of abelian groups preserves coequalizers, meaning that the coequalizer of two tensored groups is the tensor of the coequalizer. We show this is the case on the left and the right. *)
+
+(** Tensor products preserve coequalizers on the right. *)
+Definition grp_iso_ab_tensor_prod_coeq_l {A B C : AbGroup} (f g : B $-> C)
+  : ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)
+    $<~> ab_tensor_prod A (ab_coeq f g).
+Proof.
+  snrapply cate_adjointify.
+  - snrapply ab_coeq_rec.
+    + rapply (fmap01 ab_tensor_prod A).
+      nrapply ab_coeq_in.
+    + refine (_^$ $@ fmap02 ab_tensor_prod _ _ $@ _).
+      1,3: rapply fmap01_comp.
+      nrapply ab_coeq_glue.
+  - snrapply ab_tensor_prod_rec.
+    + intros a.
+      snrapply functor_ab_coeq.
+      1,2: snrapply (grp_homo_tensor_l a).
+      1,2: hnf; reflexivity.
+    + intros a b b'.
+      snrapply grp_homo_op.
+    + intros a a'.
+      srapply ab_coeq_ind_hprop.
+      intros x.
+      exact (ap (ab_coeq_in
+        (f:=fmap01 ab_tensor_prod A f)
+        (g:=fmap01 ab_tensor_prod A g))
+        (tensor_dist_r a a' x)).
+  - snrapply ab_tensor_prod_ind_homotopy.
+    intros a.
+    srapply ab_coeq_ind_hprop.
+    intros c.
+    reflexivity.
+  - snrapply ab_coeq_ind_homotopy.
+    snrapply ab_tensor_prod_ind_homotopy.
+    reflexivity.
+Defined.
+
+(** Tensor products preserve coequalizers on the left. *)
+Definition grp_iso_ab_tensor_prod_coeq_r {A B C : AbGroup} (f g : A $-> B)
+  : ab_coeq (fmap10 ab_tensor_prod f C) (fmap10 ab_tensor_prod g C)
+    $<~> ab_tensor_prod (ab_coeq f g) C.
+Proof.
+  refine (Monoidal.braide _ _ $oE _).
+  nrefine (grp_iso_ab_tensor_prod_coeq_l f g $oE _).
+  snrapply grp_iso_ab_coeq.
+  1,2: rapply Monoidal.braide.
+  1,2: symmetry; nrapply ab_tensor_swap_natural.
+Defined.
+
 (** TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tensor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts. *)