Merge pull request #2021 from Alizter/ab-tensor

tensor products of abelian groups

theories/Algebra/AbGroups/AbPushout.v

@@ -28,7 +28,7 @@ Proof.
   - intros [x y] q; strip_truncations; simpl.
     destruct q as [a q]. cbn in q.
     refine (ap (uncurry (fun x y => b x + c y)) q^ @ _).
-    unfold uncurry; cbn.
+    cbn.
     refine (ap011 sg_op (preserves_negate _) (p a)^ @ _).
     exact (left_inverse _).
 Defined.

theories/Algebra/AbGroups/AbelianGroup.v

@@ -38,6 +38,12 @@ Global Instance negate_abgroup (A : AbGroup) : Negate A := group_inverse.
 Definition ab_comm {A : AbGroup} (x y : A) : x + y = y + x
   := commutativity x y.
 
+Definition ab_neg_op {A : AbGroup} (x y : A) : - (x + y) = -x - y.
+Proof.
+  lhs nrapply grp_inv_op.
+  apply ab_comm.
+Defined.
+
 (** ** Paths between abelian groups *)
 
 Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}}
@@ -100,6 +106,8 @@ Defined.
 Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup
   := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).
 
+Arguments QuotientAbGroup G H : simpl never.
+
 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

@@ -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,8 +99,8 @@ 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 (x * (y * z))) (a (x * (z * y))))
+    (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.
     srapply Trunc_ind.
@@ -111,37 +111,48 @@ Section Abel.
     apply c.
   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)
-      (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.
+  (** The computation rule on point constructors holds definitionally. *)
+  Definition Abel_ind_beta_abel_in (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 : G)
+    : Abel_ind P a c (abel_in x) = a x
+    := idpath.
+
+  (** The computation rule on paths. *)
+  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) (abel_in_comm x y z) = c x y z.
   Proof.
     refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _).
     rapply Coeq_ind_beta_cglue.
   Defined.
 
   (** We also have a recursion princple. *)
-  Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P)
+  Definition Abel_rec (P : Type) `{IsHSet P}
+    (a : G -> P)
     (c : forall x y z, a (x * (y * z)) = a (x * (z * y)))
     : Abel -> P.
   Proof.
     apply (Abel_ind _ a).
     intros; apply dp_const, c.
   Defined.
 
-  (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *)
+  (** 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.
   Defined.
 
   (** And its recursion version. *)
   Definition Abel_rec_hprop (P : Type) `{IsHProp P}
-    (a : G -> P) : Abel -> P.
+    (a : G -> P)
+    : Abel -> P.
   Proof.
     apply (Abel_rec _ a).
     intros; apply path_ishprop.
@@ -152,9 +163,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 +175,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 +187,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 +219,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 +244,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,16 +289,16 @@ 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.
 
 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.
@@ -300,23 +319,20 @@ 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. *)
-Definition abel_unit (X : Group)
-  : GroupHomomorphism X (abel X).
-Proof.
-  snrapply @Build_GroupHomomorphism.
-  + exact ab.
-  + exact _.
-Defined.
+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)
+  := @Build_GroupHomomorphism G (abel G) abel_in _.
 
 Definition grp_homo_abel_rec {G : Group} {A : AbGroup} (f : G $-> A)
   : abel G $-> A.
 Proof.
   snrapply Build_GroupHomomorphism.
   { srapply (Abel_rec _ _ f).
     intros x y z.
-    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-    apply (ap (_ *.)).
+    nrapply grp_homo_op_agree; trivial.
     refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
     apply commutativity. }
   intros y.
@@ -327,7 +343,7 @@ Defined.
 
 (** Finally we can prove that our construction abel is an abelianization. *)
 Global Instance isabelianization_abel {G : Group}
-  : IsAbelianization (abel G) (abel_unit G).
+  : IsAbelianization (abel G) abel_unit.
 Proof.
   intros A. constructor.
   { intros h.
@@ -377,8 +393,8 @@ Global Instance issurj_isabelianization {G : Group}
   : IsAbelianization A eta -> IsSurjection eta.
 Proof.
   intros k.
-  pose (homotopic_isabelianization A (abel G) eta (abel_unit G)) as p.
-  refine (@cancelL_isequiv_conn_map _ _ _ _ _ _ _
+  pose (homotopic_isabelianization A (abel G) eta abel_unit) as p.
+  exact (@cancelL_isequiv_conn_map _ _ _ _ _ _ _
     (conn_map_homotopic _ _ _ p _)).
 Defined.
 

theories/Algebra/AbGroups/Biproduct.v

@@ -191,8 +191,7 @@ Proof.
   intros h k.
   intros [a b].
   refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
-  refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-  exact (ap011 (+) (h a) (k b)).
+  exact (grp_homo_op_agree f g (h a) (k b)).
 Defined.
 
 (* Maps out of biproducts are determined on the two inclusions. *)

theories/Algebra/AbGroups/Cyclic.v

@@ -48,8 +48,7 @@ Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
 Proof.
   induction n as [|n H].
   1: easy.
-  refine (grp_pow_natural _ _ _ @ _); simpl.
-  by rewrite grp_unit_r.
+  exact (grp_pow_natural _ _ _).
 Defined.
 
 (** [ab_Z1] is projective. *)
@@ -65,8 +64,7 @@ Proof.
   apply path_homomorphism_from_free_group.
   simpl.
   intros [].
-  refine (_ @ a.2).
-  exact (ap p (grp_unit_r _)).
+  exact a.2.
 Defined.
 
 (** The map sending the generator to [1 : Int]. *)

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,11 @@ Global Instance isfreeabgroup_isfreeabgroupon (S : Type) (F_S : AbGroup) (i : S
 Definition FreeAbGroup (S : Type) : AbGroup
   := abel (FreeGroup S).
 
+Arguments FreeAbGroup S : simpl never.
+
+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)
@@ -50,6 +56,6 @@ Global Instance isfreeabgroup_freeabgroup `{Funext} (S : Type)
   : IsFreeAbGroup (FreeAbGroup S).
 Proof.
   exists S.
-  exists (abel_unit (FreeGroup S) o freegroup_in).
+  exists (abel_unit (G:=FreeGroup S) o freegroup_in).
   srapply isfreeabgroupon_isabelianization_isfreegroup.
 Defined.