tensor preserves coequalizers

theories/Algebra/AbGroups/AbHom.v

@@ -47,13 +47,22 @@ Defined.
 
 (** Using the cokernel and addition and negation for the homs of abelian groups, we can define the coequalizer of two group homomorphisms as the cokernel of their difference. *)
 Definition ab_coeq {A B : AbGroup} (f g : GroupHomomorphism A B)
-  := ab_cokernel (ab_homo_add g (negate_hom f)).
+  := ab_cokernel (ab_homo_add (negate_hom f) g).
 
 Definition ab_coeq_in {A B} {f g : A $-> B} : B $-> ab_coeq f g.
 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.
+  by exists x.
+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.
@@ -65,9 +74,9 @@ Proof.
   destruct H as [a q].
   destruct q; simpl.
   lhs nrapply grp_homo_op.
-  lhs nrapply ap.
+  lhs nrapply (ap (.* _)).
   1: apply grp_homo_inv.
-  apply grp_moveL_1M^-1.
+  apply grp_moveL_M1^-1.
   exact (p a)^.
 Defined.
 
@@ -85,6 +94,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

@@ -182,6 +182,16 @@ Proof.
     apply ab_tensor_prod_rec_helper; assumption.
 Defined.
 
+(** A special case that arises. *)
+Definition ab_tensor_prod_rec' {A B C : AbGroup}
+  (f : A -> (B $-> C))
+  (l : forall a a' b, f (a + a') b = f a b + f a' b)
+  : ab_tensor_prod A B $-> C.
+Proof.
+  refine (ab_tensor_prod_rec f _ l).
+  intro a; apply grp_homo_op.
+Defined.
+
 (** We give an induction principle for an hprop-valued type family [P].  It may be surprising at first that we only require [P] to hold for the simple tensors [tensor a b] and be closed under addition.  It automatically follows that [P 0] holds (since [tensor 0 0 = 0]) and that [P] is closed under negation (since [tensor -a b = - tensor a b]). This induction principle says that the simple tensors generate the tensor product as a semigroup. *)
 Definition ab_tensor_prod_ind_hprop {A B : AbGroup}
   (P : ab_tensor_prod A B -> Type)
@@ -375,15 +385,12 @@ Definition functor_ab_tensor_prod {A B A' B' : AbGroup}
   (f : A $-> A') (g : B $-> B')
   : ab_tensor_prod A B $-> ab_tensor_prod A' B'.
 Proof.
-  snrapply ab_tensor_prod_rec.
-  - intros a b.
-    exact (tensor (f a) (g b)).
-  - intros a b b'; hnf.
-    rewrite grp_homo_op.
-    by rewrite tensor_dist_l.
+  snrapply ab_tensor_prod_rec'.
+  - intro a.
+    exact (grp_homo_tensor_l (f a) $o g).
   - intros a a' b; hnf.
     rewrite grp_homo_op.
-    by rewrite tensor_dist_r.
+    nrapply tensor_dist_r.
 Defined.
 
 (** 2-functoriality of the tensor product. *)
@@ -489,30 +496,16 @@ Defined.
 (** In order to be more efficient whilst unfolding definitions, we break up the definition of a twist map into its components. *)
 
 Local Definition ab_tensor_prod_twist_map {A B C : AbGroup}
-  : A -> ab_tensor_prod B C -> ab_tensor_prod B (ab_tensor_prod A C).
+  : A -> (ab_tensor_prod B C $-> ab_tensor_prod B (ab_tensor_prod A C)).
 Proof.
   intros a.
-  snrapply ab_tensor_prod_rec.
-  - intros b c.
-    exact (tensor b (tensor a c)).
-  - intros b c c'; hnf.
-    lhs nrapply ap.
-    1: nrapply tensor_dist_l.
-    nrapply tensor_dist_l.
+  snrapply ab_tensor_prod_rec'.
+  - intros b.
+    exact (grp_homo_tensor_l b $o grp_homo_tensor_l a).
   - intros b b' c; hnf.
     nrapply tensor_dist_r.
 Defined.
 
-Arguments ab_tensor_prod_twist_map {A B C} _ _ /.
-
-Local Definition ab_tensor_prod_twist_map_additive_r {A B C : AbGroup}
-  (a : A) (b b' : ab_tensor_prod B C)
-  : ab_tensor_prod_twist_map a (b + b')
-    = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a b'.
-Proof.
-  intros; nrapply grp_homo_op.
-Defined.
-
 Local Definition ab_tensor_prod_twist_map_additive_l {A B C : AbGroup}
   (a a' : A) (b : ab_tensor_prod B C)
   : ab_tensor_prod_twist_map (a + a') b
@@ -532,9 +525,8 @@ Defined.
 Definition ab_tensor_prod_twist {A B C}
   : ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C).
 Proof.
-  snrapply ab_tensor_prod_rec.
+  snrapply ab_tensor_prod_rec'.
   - exact ab_tensor_prod_twist_map. 
-  - exact ab_tensor_prod_twist_map_additive_r.
   - exact ab_tensor_prod_twist_map_additive_l.
 Defined.
 
@@ -593,10 +585,8 @@ Proof.
   - nrapply grp_homo_tensor_r.
     exact 1%int.
   - snrapply isequiv_adjointify.
-    + snrapply ab_tensor_prod_rec.
+    + snrapply ab_tensor_prod_rec'.
       * exact grp_pow_homo.
-      * intros a z z'; cbn beta.
-        nrapply grp_homo_op.
       * intros a a' z; cbn beta.
         nrapply (grp_homo_op (ab_mul z)).
     + hnf.
@@ -688,4 +678,54 @@ 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 a'; cbn beta.
+      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. *)