tensor products of abelian groups

theories/Algebra/AbGroups/AbelianGroup.v

@@ -100,6 +100,12 @@ Defined.
 Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup
   := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).
 
+Definition quotient_abgroup_map (G : AbGroup) (H : Subgroup G)
+  : GroupHomomorphism G (QuotientAbGroup G H).
+Proof.
+  snrapply grp_quotient_map.
+Defined.
+
 Definition quotient_abgroup_rec {G : AbGroup}
   (N : Subgroup G) (H : AbGroup)
   (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit)

theories/Algebra/AbGroups/Abelianization.v

@@ -275,6 +275,19 @@ Section AbelGroup.
   Proof.
     by unfold IsSemiGroupPreserving.
   Defined.
+
+  Global Instance ismonoidpreserving_ab : IsMonoidPreserving ab.
+  Proof.
+    split.
+    1: exact _.
+    reflexivity.
+  Defined.
+
+  (** [ab] preserves negation *)
+  Definition ab_negate x : ab (-x) = - ab x.
+  Proof.
+    exact (preserves_negate (f:=ab) x).
+  Defined.
 
 End AbelGroup.
 

theories/Algebra/AbGroups/FreeAbelianGroup.v

@@ -3,6 +3,7 @@ Require Import Types.Sigma Types.Forall Types.Paths.
 Require Import WildCat.Core WildCat.EquivGpd.
 Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Abelianization.
 Require Import Algebra.Groups.FreeGroup.
+Require Import Spaces.List.Core.
 
 (** * Free Abelian Groups *)
 
@@ -29,6 +30,9 @@ Global Instance isfreeabgroup_isfreeabgroupon (S : Type) (F_S : AbGroup) (i : S
 Definition FreeAbGroup (S : Type) : AbGroup
   := abel (FreeGroup S).
 
+Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S
+  := abel_unit _ o freegroup_in.
+
 (** 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)