diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index d019f68e9b1..cb48c8cd547 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. + exact (abel_unit $o f). Defined. Global Instance is1functor_abel : Is1Functor abel. 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 7bec4036651..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. @@ -347,6 +346,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 +369,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 +751,60 @@ 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. + srefine (let f:=_ in let g:=_ in cate_adjointify f g _ _). + - snrapply FreeAbGroup_rec. + intros [x y]. + exact (tensor (freeabgroup_in x) (freeabgroup_in y)). + - snrapply ab_tensor_prod_rec. + + intros x. + snrapply FreeAbGroup_rec. + intros y; revert x. + unfold FreeAbGroup. + snrapply FreeAbGroup_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 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. *)