feat(group_theory/free_group): promote free_group_congr to a mul_equiv (

#11373)

Also some various golfs and cleanups

src/group_theory/free_group.lean

@@ -353,6 +353,10 @@ quot.lift f H (mk L) = f L := rfl
   (H : ∀ L₁ L₂, red.step L₁ L₂ → f L₁ = f L₂) :
 quot.lift_on (mk L) f H = f L := rfl
 
+@[simp] lemma quot_map_mk (β : Type v) (f : list (α × bool) → list (β × bool))
+  (H : (red.step ⇒ red.step) f f) :
+quot.map f H (mk L) = mk (f L) := rfl
+
 instance : has_one (free_group α) := ⟨mk []⟩
 lemma one_eq_mk : (1 : free_group α) = mk [] := rfl
 
@@ -483,41 +487,25 @@ section map
 
 variables {β : Type v} (f : α → β) {x y : free_group α}
 
-/-- Given `f : α → β`, the canonical map `list (α × bool) → list (β × bool)`. -/
-def map.aux (L : list (α × bool)) : list (β × bool) :=
-L.map $ λ x, (f x.1, x.2)
-
-/-- Any function from `α` to `β` extends uniquely
-to a group homomorphism from the free group
-over `α` to the free group over `β`. Note that this is the bare function;
-for the group homomorphism use `map`. -/
-def map.to_fun (x : free_group α) : free_group β :=
-x.lift_on (λ L, mk $ map.aux f L) $
-λ L₁ L₂ H, quot.sound $ by cases H; simp [map.aux]
-
 /-- Any function from `α` to `β` extends uniquely
 to a group homomorphism from the free group
 ver `α` to the free group over `β`. -/
-def map : free_group α →* free_group β := monoid_hom.mk' (map.to_fun f)
-begin
-  rintros ⟨L₁⟩ ⟨L₂⟩,
-  simp [map.to_fun, map.aux]
-end
-
---by rintros ⟨L₁⟩ ⟨L₂⟩; simp [map, map.aux]
+def map : free_group α →* free_group β :=
+monoid_hom.mk'
+  (quot.map (list.map $ λ x, (f x.1, x.2)) $ λ L₁ L₂ H, by cases H; simp)
+  (by { rintros ⟨L₁⟩ ⟨L₂⟩, simp })
 
 variable {f}
 
 @[simp] lemma map.mk : map f (mk L) = mk (L.map (λ x, (f x.1, x.2))) :=
 rfl
 
-@[simp] lemma map.id : map id x = x :=
-have H1 : (λ (x : α × bool), x) = id := rfl,
-by rcases x with ⟨L⟩; simp [H1]
+@[simp] lemma map.id (x : free_group α) : map id x = x :=
+by rcases x with ⟨L⟩; simp [list.map_id']
 
-@[simp] lemma map.id' : map (λ z, z) x = x := map.id
+@[simp] lemma map.id' (x : free_group α) : map (λ z, z) x = x := map.id x
 
-theorem map.comp {γ : Type w} {f : α → β} {g : β → γ} {x} :
+theorem map.comp {γ : Type w} (f : α → β) (g : β → γ) (x) :
   map g (map f x) = map (g ∘ f) x :=
 by rcases x with ⟨L⟩; simp
 
@@ -532,15 +520,28 @@ by rintros ⟨L⟩; exact list.rec_on L g.map_one
   (show g (of x * mk t) = map f (of x * mk t),
      by simp [g.map_mul, hg, ih]))
 
-/-- Equivalent types give rise to equivalent free groups. -/
-def free_group_congr {α β} (e : α ≃ β) : free_group α ≃ free_group β :=
-⟨map e, map e.symm,
- λ x, by simp [function.comp, map.comp],
- λ x, by simp [function.comp, map.comp]⟩
-
 theorem map_eq_lift : map f x = lift (of ∘ f) x :=
 eq.symm $ map.unique _ $ λ x, by simp
 
+/-- Equivalent types give rise to multiplicatively equivalent free groups. -/
+@[simps apply]
+def free_group_congr {α β} (e : α ≃ β) : free_group α ≃* free_group β :=
+{ to_fun := map e, inv_fun := map e.symm,
+  left_inv := λ x, by simp [function.comp, map.comp],
+  right_inv := λ x, by simp [function.comp, map.comp],
+  map_mul' := monoid_hom.map_mul _ }
+
+@[simp] lemma free_group_congr_refl : free_group_congr (equiv.refl α) = mul_equiv.refl _ :=
+mul_equiv.ext map.id
+
+@[simp] lemma free_group_congr_symm {α β} (e : α ≃ β) :
+  (free_group_congr e).symm = free_group_congr e.symm :=
+rfl
+
+lemma free_group_congr_trans {α β γ} (e : α ≃ β) (f : β ≃ γ) :
+  (free_group_congr e).trans (free_group_congr f) = free_group_congr (e.trans f) :=
+mul_equiv.ext $ map.comp _ _
+
 end map
 
 section prod