From 609da93df0259d973973b216e2b9dae72663fe2a Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 14 Sep 2018 17:56:16 +0200
Subject: [PATCH] small additions to group theory

---
 hott/algebra/group_theory.hlean     |  4 ++--
 hott/algebra/homotopy_group.hlean   |  2 +-
 hott/algebra/inf_group_theory.hlean | 17 ++++++++++++-----
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean
index b43137bc1..3dc578550 100644
--- a/hott/algebra/group_theory.hlean
+++ b/hott/algebra/group_theory.hlean
@@ -433,7 +433,7 @@ namespace group
     by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv,
                 +left_inv f, mul.left_inv]
 
-    definition group_equiv_closed : group B :=
+    definition group_equiv_closed [constructor] : group B :=
     ⦃group,
       mul          := group_equiv_mul,
       mul_assoc    := group_equiv_mul_assoc,
@@ -451,7 +451,7 @@ namespace group
     definition group_equiv_mul_comm (b b' : B) : group_equiv_mul f b b' = group_equiv_mul f b' b :=
     by rewrite [↑group_equiv_mul, mul.comm]
 
-    definition ab_group_equiv_closed : ab_group B :=
+    definition ab_group_equiv_closed [constructor] : ab_group B :=
     ⦃ab_group, group_equiv_closed f,
       mul_comm := group_equiv_mul_comm f⦄
   end
diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index 37e0727d0..0d0785427 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -203,7 +203,7 @@ namespace eq
   /- todo: use is_succ -/
   definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B)
     : πg[n+1] A ≃g πg[n+1] B :=
-  gtrunc_isomorphism_gtrunc (gloopn_isomorphism (n+1) f)
+  gtrunc_isomorphism_gtrunc (gloopn_isomorphism_gloopn (n+1) f)
 
   definition homotopy_group_add (A : Type*) (n m : ℕ) :
     πg[n+m+1] A ≃g πg[n+1] (Ω[m] A) :=
diff --git a/hott/algebra/inf_group_theory.hlean b/hott/algebra/inf_group_theory.hlean
index 232b5a40d..63b3e3fd4 100644
--- a/hott/algebra/inf_group_theory.hlean
+++ b/hott/algebra/inf_group_theory.hlean
@@ -171,7 +171,7 @@ namespace group
     by rewrite [↑inf_group_equiv_mul, ↑inf_group_equiv_one, ↑inf_group_equiv_inv,
                 +left_inv f, mul.left_inv]
 
-    definition inf_group_equiv_closed : inf_group B :=
+    definition inf_group_equiv_closed [constructor] : inf_group B :=
     ⦃inf_group,
       mul          := inf_group_equiv_mul,
       mul_assoc    := inf_group_equiv_mul_assoc,
@@ -183,6 +183,13 @@ namespace group
 
   end
 
+  definition InfGroup_equiv_closed [constructor] (A : InfGroup) {B : Type} (f : A ≃ B) : InfGroup :=
+  InfGroup.mk B (inf_group_equiv_closed f _)
+
+  definition InfGroup_equiv_closed_isomorphism [constructor] (A : InfGroup) {B : Type} (f : A ≃ B) :
+    A ≃∞g InfGroup_equiv_closed A f :=
+  inf_isomorphism_of_equiv f (λa a', ap f (ap011 mul (to_left_inv f a) (to_left_inv f a'))⁻¹)
+
   section
     variables {A B : Type} (f : A ≃ B) (H : ab_inf_group A)
     include H
@@ -370,15 +377,15 @@ namespace group
   notation `Ωg→` := gap1
   notation `Ωg→[`:95 n:0 `]`:0 := gapn n
 
-  definition gloop_isomorphism {A B : Type*} (f : A ≃* B) : Ωg A ≃∞g Ωg B :=
+  definition gloop_isomorphism_gloop {A B : Type*} (f : A ≃* B) : Ωg A ≃∞g Ωg B :=
   inf_isomorphism.mk (Ωg→ f) (to_is_equiv (loop_pequiv_loop f))
 
-  definition gloopn_isomorphism (n : ℕ) [H : is_succ n] {A B : Type*} (f : A ≃* B) :
+  definition gloopn_isomorphism_gloopn (n : ℕ) [H : is_succ n] {A B : Type*} (f : A ≃* B) :
     Ωg[n] A ≃∞g Ωg[n] B :=
   inf_isomorphism.mk (Ωg→[n] f) (to_is_equiv (loopn_pequiv_loopn n f))
 
-  notation `Ωg≃` := gloop_isomorphism
-  notation `Ωg≃[`:95 n:0 `]`:0 := gloopn_isomorphism
+  notation `Ωg≃` := gloop_isomorphism_gloop
+  notation `Ωg≃[`:95 n:0 `]`:0 := gloopn_isomorphism_gloopn
 
   definition gloopn_succ_in (n : ℕ) [H : is_succ n] (A : Type*) : Ωg[succ n] A ≃∞g Ωg[n] (Ω A) :=
   inf_isomorphism_of_equiv (loopn_succ_in n A) (by induction H with n; exact loopn_succ_in_con)