feat(group_theory/free_abelian_group_finsupp): various equiv.of_free_…

…*_group lemmas (#11469)

Namely `equiv.of_free_abelian_group_linear_equiv`,
`equiv.of_free_abelian_group_equiv` and `equiv.of_free_group_equiv`
    
Co-authored-by: Adam Topaz <github@adamtopaz.com>

src/group_theory/free_abelian_group_finsupp.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 
 import group_theory.free_abelian_group
+import group_theory.is_free_group
 import data.finsupp.basic
 import data.equiv.module
 import linear_algebra.dimension
@@ -101,6 +102,36 @@ noncomputable def basis (α : Type*) :
   basis α ℤ (free_abelian_group α) :=
 ⟨(free_abelian_group.equiv_finsupp α).to_int_linear_equiv ⟩
 
+/-- Isomorphic free ablian groups (as modules) have equivalent bases. -/
+def equiv.of_free_abelian_group_linear_equiv {α β : Type*}
+  (e : free_abelian_group α ≃ₗ[ℤ] free_abelian_group β) :
+  α ≃ β :=
+let t : _root_.basis α ℤ (free_abelian_group β) := (free_abelian_group.basis α).map e
+  in t.index_equiv $ free_abelian_group.basis _
+
+/-- Isomorphic free abelian groups (as additive groups) have equivalent bases. -/
+def equiv.of_free_abelian_group_equiv {α β : Type*}
+  (e : free_abelian_group α ≃+ free_abelian_group β) :
+  α ≃ β :=
+equiv.of_free_abelian_group_linear_equiv e.to_int_linear_equiv
+
+/-- Isomorphic free groups have equivalent bases. -/
+def equiv.of_free_group_equiv {α β : Type*}
+  (e : free_group α ≃* free_group β) :
+  α ≃ β :=
+equiv.of_free_abelian_group_equiv e.abelianization_congr.to_additive
+
+open is_free_group
+/-- Isomorphic free groups have equivalent bases (`is_free_group` variant`). -/
+def equiv.of_is_free_group_equiv {G H : Type*}
+  [group G] [group H] [is_free_group G] [is_free_group H]
+  (e : G ≃* H) :
+  generators G ≃ generators H :=
+equiv.of_free_group_equiv $
+  mul_equiv.trans ((to_free_group G).symm) $
+  mul_equiv.trans e $
+  to_free_group H
+
 variable {X}
 
 /-- `coeff x` is the additive group homomorphism `free_abelian_group X →+ ℤ`

src/group_theory/free_group.lean

@@ -524,7 +524,11 @@ by rintros ⟨L⟩; exact list.rec_on L g.map_one
 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. -/
+/-- Equivalent types give rise to multiplicatively equivalent free groups.
+
+The converse can be found in `group_theory.free_abelian_group_finsupp`,
+as `equiv.of_free_group_equiv`
+ -/
 @[simps apply]
 def free_group_congr {α β} (e : α ≃ β) : free_group α ≃* free_group β :=
 { to_fun := map e, inv_fun := map e.symm,