From b3f62bf474a41a984199200f4cb142ea3a6aa0c4 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 23 Jul 2024 13:49:18 +0200 Subject: [PATCH 1/6] tensor preserves coequalizers Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbHom.v | 78 +++++++++++++++++++++++ theories/Algebra/AbGroups/TensorProduct.v | 52 +++++++++++++++ 2 files changed, 130 insertions(+) diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v index 368ae92f0bd..8773c0feb75 100644 --- a/theories/Algebra/AbGroups/AbHom.v +++ b/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} diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index ced3538649d..bc6a4edda94 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/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. *) From 30f43c013e412ce157c514c1ee28a6c66c8a774b Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 24 Jul 2024 09:46:33 -0400 Subject: [PATCH 2/6] AbHom: make definition of coeq match definition of in_cosetL --- theories/Algebra/AbGroups/AbHom.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v index 8773c0feb75..b17076a97d5 100644 --- a/theories/Algebra/AbGroups/AbHom.v +++ b/theories/Algebra/AbGroups/AbHom.v @@ -47,7 +47,7 @@ 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. @@ -60,8 +60,7 @@ Proof. intros x. nrapply qglue. apply tr. - exists x. - apply ab_comm. + by exists x. Defined. Definition ab_coeq_rec {A B : AbGroup} {f g : A $-> B} @@ -75,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. From bb8d0514a691926b542c477d763b6003d8893a85 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 24 Jul 2024 09:49:24 -0400 Subject: [PATCH 3/6] TensorProduct: introduce and use ab_tensor_prod_rec' --- theories/Algebra/AbGroups/TensorProduct.v | 56 +++++++++-------------- 1 file changed, 22 insertions(+), 34 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index bc6a4edda94..e956c979be9 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/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. @@ -704,14 +694,12 @@ Proof. + refine (_^$ $@ fmap02 ab_tensor_prod _ _ $@ _). 1,3: rapply fmap01_comp. nrapply ab_coeq_glue. - - snrapply ab_tensor_prod_rec. + - 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'. + + intros a a'; cbn beta. srapply ab_coeq_ind_hprop. intros x. exact (ap (ab_coeq_in From 5e1146162f73dad1e094a844ddebac16cf423b7e Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 24 Jul 2024 16:36:45 +0200 Subject: [PATCH 4/6] make Monoidal.braide global Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 4 ++-- theories/WildCat/Monoidal.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index e956c979be9..53c80460b10 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -721,10 +721,10 @@ 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 _). + refine (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: rapply braide. 1,2: symmetry; nrapply ab_tensor_swap_natural. Defined. diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v index 188cb90b53a..cddad657443 100644 --- a/theories/WildCat/Monoidal.v +++ b/theories/WildCat/Monoidal.v @@ -251,7 +251,7 @@ Section SymmetricBraid. := catie_adjointify (braid a b) (braid b a) (braid_braid a b) (braid_braid b a). (** [braide] is the bundled equivalence whose underlying map is [braid]. *) - Local Definition braide a b + Definition braide a b : F a b $<~> F b a := Build_CatEquiv (braid a b). From a0daafac0cd3851fcde3f9711edd8e31071f2184 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 25 Jul 2024 12:07:04 +0200 Subject: [PATCH 5/6] show grp_iso_ab_tensor_prod_coeq_{l,r} commute in obv triangle resp. Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 24 ++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 53c80460b10..7d378633ae6 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -683,7 +683,7 @@ Global Instance issymmmetricmonoidal_ab_tensor_prod (** 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) +Definition grp_iso_ab_tensor_prod_coeq_l A {B C} (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. @@ -716,16 +716,34 @@ Proof. reflexivity. Defined. +(* TODO: comment and better name? *) +Definition tensor_prod_coeq_l_comm_sq A {B C} (f g : B $-> C) + : grp_iso_ab_tensor_prod_coeq_l A f g $o ab_coeq_in + $== fmap01 ab_tensor_prod A ab_coeq_in. +Proof. + 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) +Definition grp_iso_ab_tensor_prod_coeq_r {A B} (f g : A $-> B) C : ab_coeq (fmap10 ab_tensor_prod f C) (fmap10 ab_tensor_prod g C) $<~> ab_tensor_prod (ab_coeq f g) C. Proof. refine (braide _ _ $oE _). - nrefine (grp_iso_ab_tensor_prod_coeq_l f g $oE _). + nrefine (grp_iso_ab_tensor_prod_coeq_l _ f g $oE _). snrapply grp_iso_ab_coeq. 1,2: rapply braide. 1,2: symmetry; nrapply ab_tensor_swap_natural. Defined. +(** TODO: comment and better name? *) +Definition tensor_prod_coeq_r_comm_sq {A B} (f g : A $-> B) C + : grp_iso_ab_tensor_prod_coeq_r f g C $o ab_coeq_in + $== fmap10 ab_tensor_prod ab_coeq_in C. +Proof. + snrapply ab_tensor_prod_ind_homotopy. + reflexivity. +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. *) From 08a6986f50d3912ee73228810d0c841e5fb974c0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 25 Jul 2024 08:48:02 -0400 Subject: [PATCH 6/6] TensorProduct: update comments and names --- theories/Algebra/AbGroups/TensorProduct.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 7d378633ae6..7bec4036651 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -716,8 +716,8 @@ Proof. reflexivity. Defined. -(* TODO: comment and better name? *) -Definition tensor_prod_coeq_l_comm_sq A {B C} (f g : B $-> C) +(** The equivalence respects the natural maps from [ab_tensor_prod A C]. *) +Definition ab_tensor_prod_coeq_l_triangle A {B C} (f g : B $-> C) : grp_iso_ab_tensor_prod_coeq_l A f g $o ab_coeq_in $== fmap01 ab_tensor_prod A ab_coeq_in. Proof. @@ -737,8 +737,8 @@ Proof. 1,2: symmetry; nrapply ab_tensor_swap_natural. Defined. -(** TODO: comment and better name? *) -Definition tensor_prod_coeq_r_comm_sq {A B} (f g : A $-> B) C +(** The equivalence respects the natural maps from [ab_tensor_prod B C]. *) +Definition ab_tensor_prod_coeq_r_triangle {A B} (f g : A $-> B) C : grp_iso_ab_tensor_prod_coeq_r f g C $o ab_coeq_in $== fmap10 ab_tensor_prod ab_coeq_in C. Proof.