tensor products of abelian groups

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jul 9, 2024 · bc8b278 · bc8b278
1 parent c6a8dc4
commit bc8b278
Show file tree

Hide file tree

Showing 6 changed files with 762 additions and 1 deletion.
diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/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)

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
@@ -269,6 +269,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.