introduce FreeAbGroup_rec and simplify FreeAbGroup

Signed-off-by: Ali Caglayan <[email protected]>

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.
 

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.