tensor products of abelian groups

theories/Algebra/AbGroups/Abelianization.v

@@ -52,10 +52,10 @@ From this we can show that Abel G is an abelian group.
 In fact this models the following HIT:
 
 HIT Abel (G : Group) := 
- | ab : G -> Abel G
- | ab_comm : forall x y z, ab (x * (y * z)) = ab (x * (z * y)).
+ | abel_in : G -> Abel G
+ | abel_in_comm : forall x y z, abel_in (x * (y * z)) = abel_in (x * (z * y)).
 
-We also derive ab and ab_comm from our coequalizer definition, and even prove the induction and computation rules for this HIT.
+We also derive [abel_in] and [abel_in_comm] from our coequalizer definition, and even prove the induction and computation rules for this HIT.
 
 This HIT was suggested by Dan Christensen.
 *)
@@ -80,15 +80,15 @@ Section Abel.
       (uncurry2 (fun a b c : G => a * (c * b)))).
 
   (** We have a natural map from G to Abel G. *)
-  Definition ab : G -> Abel.
+  Definition abel_in : G -> Abel.
   Proof.
     intro g.
     apply tr, coeq, g.
   Defined.
 
   (** This map satisfies the condition ab_comm. *)
-  Definition ab_comm a b c
-    : ab (a * (b * c)) = ab (a * (c * b)).
+  Definition abel_in_comm a b c
+    : abel_in (a * (b * c)) = abel_in (a * (c * b)).
   Proof.
     apply (ap tr).
     exact (cglue (a, b, c)).
@@ -99,7 +99,7 @@ Section Abel.
 
   (** We can derive the induction principle from the ones for truncation and the coequalizer. *)
   Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} 
-    (a : forall x, P (ab x)) (c : forall x y z, DPath P (ab_comm x y z)
+    (a : forall x, P (abel_in x)) (c : forall x y z, DPath P (abel_in_comm x y z)
       (a (x * (y * z))) (a (x * (z * y))))
     : forall (x : Abel), P x.
   Proof.
@@ -112,11 +112,11 @@ Section Abel.
   Defined.
 
   (** The computation rule can also be proven. *)
-  Definition Abel_ind_beta_ab_comm (P : Abel -> Type)
-    `{forall x, IsHSet (P x)}(a : forall x, P (ab x))
-    (c : forall x y z, DPath P (ab_comm x y z)
+  Definition Abel_ind_beta_abel_in_comm (P : Abel -> Type)
+    `{forall x, IsHSet (P x)}(a : forall x, P (abel_in x))
+    (c : forall x y z, DPath P (abel_in_comm x y z)
       (a (x * (y * z))) (a (x * (z * y))))
-    (x y z : G) : apD (Abel_ind P a c) (ab_comm x y z) = c x y z.
+    (x y z : G) : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z.
   Proof.
     refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _).
     rapply Coeq_ind_beta_cglue.
@@ -133,7 +133,7 @@ Section Abel.
 
   (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *)
   Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} 
-    (a : forall x, P (ab x)) : forall (x : Abel), P x.
+    (a : forall x, P (abel_in x)) : forall (x : Abel), P x.
   Proof.
     srapply (Abel_ind _ a).
     intros; apply path_ishprop.
@@ -152,9 +152,10 @@ End Abel.
 (** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *)
 Local Ltac Abel_ind_hprop x := snrapply Abel_ind_hprop; [exact _ | intro x].
 
-(** We make sure that G is implicit in the arguments of ab and ab_comm. *)
-Arguments ab {_}.
-Arguments ab_comm {_}.
+(** We make sure that G is implicit in the arguments of [abel_in
+ and [abel_in_comm]. *)
+Arguments abel_in {_}.
+Arguments abel_in_comm {_}.
 
 (** Now we can show that Abel G is in fact an abelian group. *)
 
@@ -163,7 +164,9 @@ Section AbelGroup.
   Context (G : Group).
 
   (** Firstly we derive the operation on Abel G. This is defined as follows:
-        ab x + ab y := ab (x y)
+      <<
+        abel_in x + abel_in y := abel_in (x * y)
+      >>
       But we need to also check that it preserves ab_comm in the appropriate way. *)
   Global Instance abel_sgop : SgOp (Abel G).
   Proof.
@@ -173,21 +176,21 @@ Section AbelGroup.
       revert a.
       srapply Abel_rec.
       { intro a.
-        exact (ab (a * b)). }
+        exact (abel_in (a * b)). }
       intros a c d; hnf.
       (* The pattern seems to be to alternate associativity and ab_comm. *)
       refine (ap _ (associativity _ _ _)^ @ _).
-      refine (ab_comm _ _ _ @ _).
+      refine (abel_in_comm _ _ _ @ _).
       refine (ap _ (associativity _ _ _) @ _).
-      refine (ab_comm _ _ _ @ _).
+      refine (abel_in_comm _ _ _ @ _).
       refine (ap _ (associativity _ _ _)^ @ _).
-      refine (ab_comm _ _ _ @ _).
+      refine (abel_in_comm _ _ _ @ _).
       refine (ap _ (associativity _ _ _)). }
     intros b c d.
     revert a.
     Abel_ind_hprop a; simpl.
     refine (ap _ (associativity _ _ _) @ _).
-    refine (ab_comm _ _ _ @ _).
+    refine (abel_in_comm _ _ _ @ _).
     refine (ap _ (associativity _ _ _)^).
   Defined.
 
@@ -205,7 +208,7 @@ Section AbelGroup.
   Global Instance abel_issemigroup : IsSemiGroup (Abel G) := {}.
 
   (** We define the unit as ab of the unit of G *)
-  Global Instance abel_mon_unit : MonUnit (Abel G) := ab mon_unit.
+  Global Instance abel_mon_unit : MonUnit (Abel G) := abel_in mon_unit.
 
   (** By using Abel_ind_hprop we can prove the left and right identity laws. *)
   Global Instance abel_leftidentity : LeftIdentity abel_sgop abel_mon_unit.
@@ -230,25 +233,30 @@ Section AbelGroup.
     Abel_ind_hprop y.
     revert x.
     Abel_ind_hprop x.
-    refine ((ap ab (left_identity _))^ @ _).
-    refine (_ @ (ap ab (left_identity _))).
-    apply ab_comm.
+    refine ((ap abel_in (left_identity _))^ @ _).
+    refine (_ @ (ap abel_in (left_identity _))).
+    apply abel_in_comm.
   Defined.
 
   (** Now we can define the negation. This is just
-        - (ab g) := (ab (g^-1))
+      <<
+        - (abel_in g) := abel_in (- g)
+      >>
       However when checking that it respects ab_comm we have to show the following:
-        ab (- z * - y * - x) = ab (- y * - z * - x)
-      there is no obvious way to do this, but we note that ab (x * y) is exactly the definition of ab x + ab y! Hence by commutativity we can show this. *)
+      <<
+        abel_in (- z * - y * - x) = abel_in (- y * - z * - x)
+      >>
+      there is no obvious way to do this, but we note that [abel_in (x * y)] is exactly the definition of [abel_in x + abel_in y]! Hence by commutativity we can show this. *)
   Global Instance abel_negate : Negate (Abel G).
   Proof.
     srapply Abel_rec.
     { intro g.
-      exact (ab (-g)). }
+      exact (abel_in (-g)). }
     intros x y z; cbn.
     rewrite ?negate_sg_op.
-    change (ab(- z) * ab(- y) * ab (- x) = ab (- y) * ab (- z) * ab(- x)).
-    by rewrite (commutativity (ab (-z)) (ab (-y))).
+    change (abel_in (- z) * abel_in (- y) * abel_in (- x)
+      = abel_in (- y) * abel_in (- z) * abel_in (- x)).
+    by rewrite (commutativity (abel_in (-z)) (abel_in (-y))).
   Defined.
 
   (** Again by Abel_ind_hprop and the corresponding laws for G we can prove the left and right inverse laws. *)
@@ -270,29 +278,23 @@ Section AbelGroup.
   (** And since the operation is commutative, an abelian group. *)
   Global Instance isabgroup_abel : IsAbGroup (Abel G) := {}.
 
-  (** By definition, the map ab is also a group homomorphism. *)
-  Global Instance issemigrouppreserving_ab : IsSemiGroupPreserving ab.
+  (** By definition, the map [abel_in] is also a group homomorphism. *)
+  Global Instance issemigrouppreserving_abel_in : IsSemiGroupPreserving abel_in.
   Proof.
     by unfold IsSemiGroupPreserving.
   Defined.
 
-  Global Instance ismonoidpreserving_ab : IsMonoidPreserving ab.
+  Global Instance ismonoidpreserving_abel_in : IsMonoidPreserving abel_in.
   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.
 
-(** We can easily prove that ab is a surjection. *)
-Global Instance issurj_ab {G : Group} : IsSurjection (@ab G).
+(** We can easily prove that [abel_in] is a surjection. *)
+Global Instance issurj_abel_in {G : Group} : IsSurjection (@abel_in G).
 Proof.
   apply BuildIsSurjection.
   Abel_ind_hprop x.
@@ -313,12 +315,12 @@ Proof.
   - exact _.
 Defined.
 
-(** The unit of this map is the map ab which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *)
+(** 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 (X : Group)
   : GroupHomomorphism X (abel X).
 Proof.
   snrapply @Build_GroupHomomorphism.
-  + exact ab.
+  + exact abel_in.
   + exact _.
 Defined.