From be352ce291657bce57d36bab981d318ba6282cd8 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 29 Aug 2024 00:59:02 +0300 Subject: [PATCH 1/3] free abelian groups take products to tensor products Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/Abelianization.v | 5 +- theories/Algebra/AbGroups/TensorProduct.v | 89 +++++++++++++++++++--- 2 files changed, 80 insertions(+), 14 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index d019f68e9b1..d86d100509f 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -324,7 +324,7 @@ Arguments abel G : simpl never. (** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *) Definition abel_unit {G : Group} - : GroupHomomorphism G (abel G) + : G $-> (abel G) := @Build_GroupHomomorphism G (abel G) abel_in _. Definition grp_homo_abel_rec {G : Group} {A : AbGroup} (f : G $-> A) @@ -423,8 +423,7 @@ Proof. snrapply Build_Is0Functor. intros A B f. snrapply grp_homo_abel_rec. - refine (_ $o f). - exact abel_unit. + refine (abel_unit $o f). Defined. Global Instance is1functor_abel : Is1Functor abel. diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 7bec4036651..982992ef3c8 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -347,6 +347,22 @@ Definition issig_Biadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} : _ <~> Biadditive A B C := ltac:(issig). +Definition biadditive_ab_tensor_prod {A B C : AbGroup} + : (ab_tensor_prod A B $-> C) -> Biadditive A B C. +Proof. + intros f. + exists (fun x y => f (tensor x y)). + snrapply Build_IsBiadditive. + - intros b a a'; simpl. + lhs nrapply (ap f). + 1: nrapply tensor_dist_r. + nrapply grp_homo_op. + - intros a a' b; simpl. + lhs nrapply (ap f). + 1: nrapply tensor_dist_l. + nrapply grp_homo_op. +Defined. + (** The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one corresondance with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups. *) Definition equiv_ab_tensor_prod_rec `{Funext} (A B C : AbGroup) : Biadditive A B C <~> (ab_tensor_prod A B $-> C). @@ -354,17 +370,7 @@ Proof. snrapply equiv_adjointify. - intros [f [l r]]. exact (ab_tensor_prod_rec f r (fun a a' b => l b a a')). - - intros f. - exists (fun x y => f (tensor x y)). - snrapply Build_IsBiadditive. - + intros b a a'; simpl. - lhs nrapply (ap f). - 1: nrapply tensor_dist_r. - nrapply grp_homo_op. - + intros a a' b; simpl. - lhs nrapply (ap f). - 1: nrapply tensor_dist_l. - nrapply grp_homo_op. + - snrapply biadditive_ab_tensor_prod. - intros f. snrapply equiv_path_grouphomomorphism. snrapply ab_tensor_prod_ind_homotopy. @@ -746,4 +752,65 @@ Proof. reflexivity. Defined. +(** ** Tensor Product of Free Abelian Groups *) + +Definition equiv_ab_tensor_prod_freeabgroup X Y + : FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y). +Proof. + transparent assert (f : (FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y))). + { snrapply grp_homo_abel_rec. + snrapply FreeGroup_rec. + intros [x y]. + exact (tensor (freeabgroup_in x) (freeabgroup_in y)). } + transparent assert (g : (ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y))). + { snrapply ab_tensor_prod_rec. + + intros x. + snrapply grp_homo_abel_rec. + snrapply FreeGroup_rec. + intros y; revert x. + unfold FreeAbGroup. + snrapply grp_homo_abel_rec. + snrapply FreeGroup_rec. + intros x. + apply abel_unit. + apply freegroup_in. + exact (x, y). + + intros x y y'. + snrapply grp_homo_op. + + intros x x'. + rapply Abel_ind_hprop. + snrapply (FreeGroup_ind_homotopy _ (f' := ab_homo_add _ _)). + intros y. + lhs nrapply FreeGroup_rec_beta. + lhs nrapply grp_homo_op. + snrapply (ap011 (+) _^ _^). + 1,2: nrapply FreeGroup_rec_beta. } + snrapply (cate_adjointify f g). + - snrapply ab_tensor_prod_ind_homotopy. + intros x. + change (f $o g $o grp_homo_tensor_l x $== grp_homo_tensor_l x). + rapply Abel_ind_hprop. + change (@abel_in ?G) with (grp_homo_map (@abel_unit G)). + repeat change (cat_comp (A:=AbGroup) ?f ?g) with (cat_comp (A:=Group) f g). + change (forall y, grp_homo_map ?f (abel_unit y) = grp_homo_map ?g (abel_unit y)) + with (cat_comp (A:=Group) f abel_unit $== cat_comp (A:=Group) g abel_unit). + rapply FreeGroup_ind_homotopy. + intros y; revert x. + change (f $o g $o grp_homo_tensor_r (freeabgroup_in y) $== grp_homo_tensor_r (freeabgroup_in y)). + rapply Abel_ind_hprop. + change (@abel_in ?G) with (grp_homo_map (@abel_unit G)). + repeat change (cat_comp (A:=AbGroup) ?f ?g) with (cat_comp (A:=Group) f g). + change (forall y, grp_homo_map ?f (abel_unit y) = grp_homo_map ?g (abel_unit y)) + with (cat_comp (A:=Group) f abel_unit $== cat_comp (A:=Group) g abel_unit). + rapply FreeGroup_ind_homotopy. + intros x. + reflexivity. + - rapply Abel_ind_hprop. + change (GpdHom (A:=Hom(A:=Group) (FreeGroup (X * Y)) _) + (cat_comp (A:=Group) (g $o f) (@abel_unit (FreeGroup (X * Y)))) + (@abel_unit (FreeGroup (X * Y)))). + snrapply FreeGroup_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 2e8241acf4973c29cbdc48c9936b18fc34795e08 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Fri, 6 Sep 2024 14:42:43 -0400 Subject: [PATCH 2/3] Abelianization, TensorProduct: minor simplifications --- theories/Algebra/AbGroups/Abelianization.v | 2 +- theories/Algebra/AbGroups/TensorProduct.v | 16 +++++++--------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index d86d100509f..cb48c8cd547 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -423,7 +423,7 @@ Proof. snrapply Build_Is0Functor. intros A B f. snrapply grp_homo_abel_rec. - refine (abel_unit $o f). + exact (abel_unit $o f). Defined. Global Instance is1functor_abel : Is1Functor abel. diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 982992ef3c8..33b4689ef36 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -757,26 +757,25 @@ Defined. Definition equiv_ab_tensor_prod_freeabgroup X Y : FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y). Proof. - transparent assert (f : (FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y))). - { snrapply grp_homo_abel_rec. + srefine (let f:=_ in let g:=_ in cate_adjointify f g _ _). + - snrapply grp_homo_abel_rec. snrapply FreeGroup_rec. intros [x y]. - exact (tensor (freeabgroup_in x) (freeabgroup_in y)). } - transparent assert (g : (ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y))). - { snrapply ab_tensor_prod_rec. + exact (tensor (freeabgroup_in x) (freeabgroup_in y)). + - snrapply ab_tensor_prod_rec. + intros x. snrapply grp_homo_abel_rec. snrapply FreeGroup_rec. intros y; revert x. unfold FreeAbGroup. - snrapply grp_homo_abel_rec. + snrapply grp_homo_abel_rec. snrapply FreeGroup_rec. intros x. apply abel_unit. apply freegroup_in. exact (x, y). + intros x y y'. - snrapply grp_homo_op. + snrapply grp_homo_op. + intros x x'. rapply Abel_ind_hprop. snrapply (FreeGroup_ind_homotopy _ (f' := ab_homo_add _ _)). @@ -784,8 +783,7 @@ Proof. lhs nrapply FreeGroup_rec_beta. lhs nrapply grp_homo_op. snrapply (ap011 (+) _^ _^). - 1,2: nrapply FreeGroup_rec_beta. } - snrapply (cate_adjointify f g). + 1,2: nrapply FreeGroup_rec_beta. - snrapply ab_tensor_prod_ind_homotopy. intros x. change (f $o g $o grp_homo_tensor_l x $== grp_homo_tensor_l x). From a00db48b53e6eeea6a5d4c33b5d32fcfa55f5334 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 7 Sep 2024 01:32:24 +0300 Subject: [PATCH 3/3] introduce FreeAbGroup_rec and simplify FreeAbGroup Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/FreeAbelianGroup.v | 11 +++++++++-- theories/Algebra/AbGroups/TensorProduct.v | 12 ++++-------- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/theories/Algebra/AbGroups/FreeAbelianGroup.v b/theories/Algebra/AbGroups/FreeAbelianGroup.v index 862a95065a9..1d3558b7b79 100644 --- a/theories/Algebra/AbGroups/FreeAbelianGroup.v +++ b/theories/Algebra/AbGroups/FreeAbelianGroup.v @@ -35,6 +35,14 @@ Arguments FreeAbGroup S : simpl never. Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S := abel_unit o freegroup_in. +Definition FreeAbGroup_rec {S : Type} {A : AbGroup} (f : S -> A) + : FreeAbGroup S $-> A + := grp_homo_abel_rec (FreeGroup_rec _ _ f). + +Definition FreeAbGroup_rec_beta_in {S : Type} {A : AbGroup} (f : S -> A) + : FreeAbGroup_rec f o freeabgroup_in == f + := fun _ => idpath. + (** The abelianization of a free group on a set is a free abelian group on that set. *) Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext} {S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A) @@ -55,8 +63,7 @@ Defined. Global Instance isfreeabgroup_freeabgroup `{Funext} (S : Type) : IsFreeAbGroup (FreeAbGroup S). Proof. - exists S. - exists (abel_unit (G:=FreeGroup S) o freegroup_in). + exists S, freeabgroup_in. srapply isfreeabgroupon_isabelianization_isfreegroup. Defined. diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 33b4689ef36..f68984a08f0 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -175,8 +175,7 @@ Definition ab_tensor_prod_rec {A B C : AbGroup} Proof. unfold ab_tensor_prod. snrapply grp_quotient_rec. - - snrapply grp_homo_abel_rec. - snrapply FreeGroup_rec. + - snrapply FreeAbGroup_rec. exact (uncurry f). - unfold normalsubgroup_subgroup. apply ab_tensor_prod_rec_helper; assumption. @@ -758,18 +757,15 @@ Definition equiv_ab_tensor_prod_freeabgroup X Y : FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y). Proof. srefine (let f:=_ in let g:=_ in cate_adjointify f g _ _). - - snrapply grp_homo_abel_rec. - snrapply FreeGroup_rec. + - snrapply FreeAbGroup_rec. intros [x y]. exact (tensor (freeabgroup_in x) (freeabgroup_in y)). - snrapply ab_tensor_prod_rec. + intros x. - snrapply grp_homo_abel_rec. - snrapply FreeGroup_rec. + snrapply FreeAbGroup_rec. intros y; revert x. unfold FreeAbGroup. - snrapply grp_homo_abel_rec. - snrapply FreeGroup_rec. + snrapply FreeAbGroup_rec. intros x. apply abel_unit. apply freegroup_in.