From de2e27a8916453fd0c6ea70991d0aed762330f05 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 23 Jul 2024 13:49:18 +0200 Subject: [PATCH] tensor preserves coequalizers Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbHom.v | 68 +++++++++++++++++++++++ theories/Algebra/AbGroups/TensorProduct.v | 51 +++++++++++++++++ 2 files changed, 119 insertions(+) diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v index 368ae92f0bd..cdfaba8903c 100644 --- a/theories/Algebra/AbGroups/AbHom.v +++ b/theories/Algebra/AbGroups/AbHom.v @@ -85,6 +85,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} diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index ced3538649d..334fee26a2f 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -688,4 +688,55 @@ 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 product preserves 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. + +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. *)