feat: change IsFreeGroup to a Prop (#7698)

Currently, the class `IsFreeGroup` contains data (namely, a specific set of generators). This is bad, as there are many sets of generators in a free group, and changing sets of generators happens all the time in geometric group theory. We switch to a design in which
* we define `FreeGroupBasis`, following the definition and API of bases of vector spaces. Most existing API around `IsFreeGroup` is transferred to lemmas taking a free group basis as a variable.
* The typeclass `IsFreeGroup` is Prop-valued, and requires only the existence of a free group basis.

Mathlib/GroupTheory/CoprodI.lean

@@ -991,21 +991,22 @@ theorem lift_injective_of_ping_pong : Function.Injective (lift f) := by
 
 end PingPongLemma
 
-/-- The free product of free groups is itself a free group -/
-@[simps!]  --Porting note: added `!`
-instance {ι : Type*} (G : ι → Type*) [∀ i, Group (G i)] [hG : ∀ i, IsFreeGroup (G i)] :
-    IsFreeGroup (CoprodI G) where
-  Generators := Σi, IsFreeGroup.Generators (G i)
-  MulEquiv' :=
-    MonoidHom.toMulEquiv
-      (FreeGroup.lift fun x : Σi, IsFreeGroup.Generators (G i) =>
-        CoprodI.of (IsFreeGroup.of x.2 : G x.1))
-      (CoprodI.lift fun i : ι =>
-        (IsFreeGroup.lift fun x : IsFreeGroup.Generators (G i) =>
-            FreeGroup.of (⟨i, x⟩ : Σi, IsFreeGroup.Generators (G i)) :
-          G i →* FreeGroup (Σi, IsFreeGroup.Generators (G i))))
-      (by ext; simp)
-      (by ext; simp)
+/-- Given a family of free groups with distinguished bases, then their free product is free, with
+a basis given by the union of the bases of the components. -/
+def FreeGroupBasis.coprodI {ι : Type*} {X : ι → Type*} {G : ι → Type*} [∀ i, Group (G i)]
+    (B : ∀ i, FreeGroupBasis (X i) (G i)) :
+    FreeGroupBasis (Σ i, X i) (CoprodI G) :=
+  ⟨MulEquiv.symm <| MonoidHom.toMulEquiv
+    (FreeGroup.lift fun x : Σ i, X i => CoprodI.of (B x.1 x.2))
+    (CoprodI.lift fun i : ι => (B i).lift fun x : X i =>
+              FreeGroup.of (⟨i, x⟩ : Σ i, X i))
+    (by ext; simp)
+    (by ext1 i; apply (B i).ext_hom; simp)⟩
+
+/-- The free product of free groups is itself a free group. -/
+instance {ι : Type*} (G : ι → Type*) [∀ i, Group (G i)] [∀ i, IsFreeGroup (G i)] :
+    IsFreeGroup (CoprodI G) :=
+  (FreeGroupBasis.coprodI (fun i ↦ IsFreeGroup.basis (G i))).isFreeGroup
 
 -- NB: One might expect this theorem to be phrased with ℤ, but ℤ is an additive group,
 -- and using `Multiplicative ℤ` runs into diamond issues.

Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

@@ -10,56 +10,175 @@ import Mathlib.GroupTheory.FreeGroup.Basic
 /-!
 # Free groups structures on arbitrary types
 
-This file defines a type class for type that are free groups, together with the usual operations.
-The type class can be instantiated by providing an isomorphism to the canonical free group, or by
-proving that the universal property holds.
+This file defines the notion of free basis of a group, which induces an isomorphism between the
+group and the free group generated by the basis.
+
+It also introduced a type class for groups which are free groups, i.e., for which some free basis
+exists.
 
 For the explicit construction of free groups, see `GroupTheory/FreeGroup`.
 
 ## Main definitions
 
-* `IsFreeGroup G` - a typeclass to indicate that `G` is free over some generators
-* `IsFreeGroup.of` - the canonical injection of `G`'s generators into `G`
-* `IsFreeGroup.lift` - the universal property of the free group
+* `FreeGroupBasis ι G` : a function from `ι` to `G` such that `G` is free over its image.
+  Equivalently, an isomorphism between `G` and `FreeGroup ι`.
+
+* `IsFreeGroup G` : a typeclass to indicate that `G` is free over some generators
+* `Generators G` : given a group satisfying `IsFreeGroup G`, some indexing type over
+  which `G` is free.
+* `IsFreeGroup.of` : the canonical injection of `G`'s generators into `G`
+* `IsFreeGroup.lift` : the universal property of the free group
 
 ## Main results
 
-* `IsFreeGroup.toFreeGroup` - any free group with generators `A` is equivalent to `FreeGroup A`.
-* `IsFreeGroup.unique_lift` - the universal property of a free group
-* `IsFreeGroup.ofUniqueLift` - constructing `IsFreeGroup` from the universal property
+* `FreeGroupBasis.isFreeGroup`: a group admitting a free group basis is free.
+* `IsFreeGroup.toFreeGroup`: any free group with generators `A` is equivalent to `FreeGroup A`.
+* `IsFreeGroup.unique_lift`: the universal property of a free group.
+* `FreeGroupBasis.ofUniqueLift`: a group satisfying the universal property of a free group admits
+ a free group basis.
 
 -/
 
 
 universe u
 
+open Function Set
+
+noncomputable section
+
+/-- A free group basis `FreeGroupBasis ι G` is a structure recording the isomorphism between a
+group `G` and the free group over `ι`. One may think of such a basis as a function from `ι` to `G`
+(which is registered through a `FunLike` instance) together with the fact that the morphism induced
+by this function from `FreeGroup ι` to `G` is an isomorphism. -/
+structure FreeGroupBasis (ι : Type*) (G : Type*) [Group G] where
+  /-- `FreeGroupBasis.ofRepr` constructs a basis given an equivalence with a free group. -/
+  ofRepr ::
+    /-- `repr` is the isomorphism between the group `G` and the free group generated by `ι`. -/
+    repr : G ≃* FreeGroup ι
+
+/-- A group is free if it admits a free group basis. In the definition, we require the basis to
+be in the same universe as `G`, although this property follows from the existence of a basis in
+any universe, see `FreeGroupBasis.isFreeGroup`. -/
+class IsFreeGroup (G : Type u) [Group G] : Prop where
+  nonempty_basis : ∃ (ι : Type u), Nonempty (FreeGroupBasis ι G)
+
+namespace FreeGroupBasis
+
+variable {ι ι' G H : Type*} [Group G] [Group H]
+
+/-- A free group basis for `G` over `ι` is associated to a map `ι → G` recording the images of
+the generators. -/
+instance funLike : FunLike (FreeGroupBasis ι G) ι (fun _ ↦ G) where
+  coe b := fun i ↦ b.repr.symm (FreeGroup.of i)
+  coe_injective' := by
+    rintro ⟨b⟩  ⟨b'⟩ hbb'
+    have H : (b.symm : FreeGroup ι →* G) = (b'.symm : FreeGroup ι →* G) := by
+      ext i; exact congr_fun hbb' i
+    have : b.symm = b'.symm := by ext x; exact FunLike.congr_fun H x
+    rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]
+
+@[simp] lemma repr_apply_coe (b : FreeGroupBasis ι G) (i : ι) : b.repr (b i) = FreeGroup.of i := by
+  change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i
+  simp
+
+/-- The canonical basis of the free group over `X`. -/
+def ofFreeGroup (X : Type*) : FreeGroupBasis X (FreeGroup X) := ofRepr (MulEquiv.refl _)
+
+@[simp] lemma ofFreeGroup_apply {X : Type*} (x : X) :
+    FreeGroupBasis.ofFreeGroup X x = FreeGroup.of x :=
+  rfl
+
+/-- Reindex a free group basis through a bijection of the indexing sets. -/
+protected def reindex (b : FreeGroupBasis ι G) (e : ι ≃ ι') : FreeGroupBasis ι' G :=
+  ofRepr (b.repr.trans (FreeGroup.freeGroupCongr e))
+
+@[simp] lemma reindex_apply (b : FreeGroupBasis ι G) (e : ι ≃ ι') (x : ι') :
+    b.reindex e x = b (e.symm x) := rfl
+
+/-- Pushing a free group basis through a group isomorphism. -/
+protected def map (b : FreeGroupBasis ι G) (e : G ≃* H) : FreeGroupBasis ι H :=
+  ofRepr (e.symm.trans b.repr)
+
+@[simp] lemma map_apply (b : FreeGroupBasis ι G) (e : G ≃* H) (x : ι) :
+    b.map e x = e (b x) := rfl
+
+protected lemma injective (b : FreeGroupBasis ι G) : Injective b :=
+  b.repr.symm.injective.comp FreeGroup.of_injective
+
+/-- A group admitting a free group basis is a free group. -/
+lemma isFreeGroup (b : FreeGroupBasis ι G) : IsFreeGroup G :=
+  ⟨range b, ⟨b.reindex (Equiv.ofInjective (↑b) b.injective)⟩⟩
+
+instance (X : Type*) : IsFreeGroup (FreeGroup X) :=
+  (ofFreeGroup X).isFreeGroup
 
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4:
-#[`MulEquiv] [] -/
-/- Porting Note regarding the comment above:
-The mathlib3 version makes `G` explicit in `IsFreeGroup.MulEquiv`. -/
+/-- Given a free group basis of `G` over `ι`, there is a canonical bijection between maps from `ι`
+to a group `H` and morphisms from `G` to `H`. -/
+@[simps!]
+def lift (b : FreeGroupBasis ι G) : (ι → H) ≃ (G →* H) :=
+  FreeGroup.lift.trans
+    { toFun := fun f => f.comp b.repr.toMonoidHom
+      invFun := fun f => f.comp b.repr.symm.toMonoidHom
+      left_inv := fun f => by
+        ext
+        simp
+      right_inv := fun f => by
+        ext
+        simp }
 
-/-- `IsFreeGroup G` means that `G` isomorphic to a free group. -/
-class IsFreeGroup (G : Type u) [Group G] where
-  /-- The generators of a free group. -/
-  Generators : Type u
-  /-- The multiplicative equivalence between "the" free group on the generators, and
-  the given group `G`.
-  Note: `IsFreeGroup.MulEquiv'` should not be used directly.
-  `IsFreeGroup.MulEquiv` should be used instead because it makes `G` an explicit variable.-/
-  MulEquiv' : FreeGroup Generators ≃* G
-#align is_free_group IsFreeGroup
+/-- If two morphisms on `G` coincide on the elements of a basis, then they coincide. -/
+lemma ext_hom (b : FreeGroupBasis ι G) (f g : G →* H) (h : ∀ i, f (b i) = g (b i)) : f = g :=
+  b.lift.symm.injective <| funext h
 
-instance (X : Type*) : IsFreeGroup (FreeGroup X) where
-  Generators := X
-  MulEquiv' := MulEquiv.refl _
+/-- If a group satisfies the universal property of a free group with respect to a given type, then
+it admits a free group basis based on this type. Here, the universal property is expressed as
+in `IsFreeGroup.lift` and its properties. -/
+def ofLift {G : Type u} [Group G] (X : Type u) (of : X → G)
+    (lift : ∀ {H : Type u} [Group H], (X → H) ≃ (G →* H))
+    (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) :
+    FreeGroupBasis X G where
+  repr := MulEquiv.symm <| MonoidHom.toMulEquiv (FreeGroup.lift of) (lift FreeGroup.of)
+      (by
+        apply FreeGroup.ext_hom; intro x
+        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of,
+          lift_of])
+      (by
+        let lift_symm_of : ∀ {H : Type u} [Group H], ∀ (f : G →* H) (a), lift.symm f a = f (of a) :=
+          by intro H _ f a; simp [← lift_of (lift.symm f)]
+        apply lift.symm.injective; ext x
+        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of,
+          lift_of, lift_symm_of])
+
+/-- If a group satisfies the universal property of a free group with respect to a given type, then
+it admits a free group basis based on this type. Here
+the universal property is expressed as in `IsFreeGroup.unique_lift`.  -/
+def ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G)
+    (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a) :
+    FreeGroupBasis X G :=
+  let lift {H : Type u} [Group H] : (X → H) ≃ (G →* H) :=
+    { toFun := fun f => Classical.choose (h f)
+      invFun := fun F => F ∘ of
+      left_inv := fun f => funext (Classical.choose_spec (h f)).left
+      right_inv := fun F => ((Classical.choose_spec (h (F ∘ of))).right F fun _ => rfl).symm }
+  let lift_of {H : Type u} [Group H] (f : X → H) (a : X) : lift f (of a) = f a :=
+    congr_fun (lift.symm_apply_apply f) a
+  ofLift X of @lift @lift_of
+
+end FreeGroupBasis
 
 namespace IsFreeGroup
 
 variable (G : Type*) [Group G] [IsFreeGroup G]
 
+/-- A set of generators of a free group, chosen arbitrarily -/
+def Generators : Type _ := (IsFreeGroup.nonempty_basis (G := G)).choose
+
 /-- Any free group is isomorphic to "the" free group. -/
-def MulEquiv : FreeGroup (Generators G) ≃* G := IsFreeGroup.MulEquiv'
+irreducible_def MulEquiv : FreeGroup (Generators G) ≃* G :=
+  (IsFreeGroup.nonempty_basis (G := G)).choose_spec.some.repr.symm
+
+/-- A free group basis of a free group `G`, over the set `Generators G`. -/
+def basis : FreeGroupBasis (Generators G) G := FreeGroupBasis.ofRepr (MulEquiv G).symm
 
 /-- Any free group is isomorphic to "the" free group. -/
 @[simps!]
@@ -76,32 +195,14 @@ def of : Generators G → G :=
   (MulEquiv G).toFun ∘ FreeGroup.of
 #align is_free_group.of IsFreeGroup.of
 
-@[simp]
-theorem of_eq_freeGroup_of {A : Type u} : @of (FreeGroup A) _ _ = FreeGroup.of :=
-  rfl
-#align is_free_group.of_eq_free_group_of IsFreeGroup.of_eq_freeGroup_of
-
 variable {H : Type*} [Group H]
 
 /-- The equivalence between functions on the generators and group homomorphisms from a free group
 given by those generators. -/
 def lift : (Generators G → H) ≃ (G →* H) :=
-  FreeGroup.lift.trans
-    { toFun := fun f => f.comp (MulEquiv G).symm.toMonoidHom
-      invFun := fun f => f.comp (MulEquiv G).toMonoidHom
-      left_inv := fun f => by
-        ext
-        simp
-      right_inv := fun f => by
-        ext
-        simp }
+  (basis G).lift
 #align is_free_group.lift IsFreeGroup.lift
 
-@[simp]
-theorem lift'_eq_freeGroup_lift {A : Type u} : @lift (FreeGroup A) _ _ H _ = FreeGroup.lift :=
-  rfl
-#align is_free_group.lift'_eq_free_group_lift IsFreeGroup.lift'_eq_freeGroup_lift
-
 @[simp]
 theorem lift_of (f : Generators G → H) (a : Generators G) : lift f (of a) = f a :=
   congr_fun (lift.symm_apply_apply f) a
@@ -112,8 +213,7 @@ theorem lift_symm_apply (f : G →* H) (a : Generators G) : (lift.symm f) a = f
   rfl
 #align is_free_group.lift_symm_apply IsFreeGroup.lift_symm_apply
 
-@[ext 1050] --Porting note: increased priority, but deliberately less than for example
---`FreeProduct.ext_hom`
+/- Do not register this as an ext lemma, as `Generators G` is not canonical. -/
 theorem ext_hom ⦃f g : G →* H⦄ (h : ∀ a : Generators G, f (of a) = g (of a)) : f = g :=
   lift.symm.injective (funext h)
 #align is_free_group.ext_hom IsFreeGroup.ext_hom
@@ -127,47 +227,23 @@ theorem unique_lift (f : Generators G → H) : ∃! F : G →* H, ∀ a, F (of a
   simpa only [Function.funext_iff] using lift.symm.bijective.existsUnique f
 #align is_free_group.unique_lift IsFreeGroup.unique_lift
 
-/-- If a group satisfies the universal property of a free group, then it is a free group, where
-the universal property is expressed as in `IsFreeGroup.lift` and its properties. -/
-def ofLift {G : Type u} [Group G] (X : Type u) (of : X → G)
+/-- If a group satisfies the universal property of a free group with respect to a given type, then
+it is free. Here, the universal property is expressed as in `IsFreeGroup.lift` and its
+properties. -/
+lemma ofLift {G : Type u} [Group G] (X : Type u) (of : X → G)
     (lift : ∀ {H : Type u} [Group H], (X → H) ≃ (G →* H))
-    (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) : IsFreeGroup G
-    where
-  Generators := X
-  MulEquiv' :=
-    MonoidHom.toMulEquiv (FreeGroup.lift of) (lift FreeGroup.of)
-      (by
-        apply FreeGroup.ext_hom; intro x
-        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of,
-          lift_of])
-      (by
-        let lift_symm_of : ∀ {H : Type u} [Group H], ∀ (f : G →* H) (a), lift.symm f a = f (of a) :=
-          by intro H _ f a; simp [← lift_of (lift.symm f)]
-        apply lift.symm.injective; ext x
-        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of,
-          lift_of, lift_symm_of])
-#align is_free_group.of_lift IsFreeGroup.ofLift
+    (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) :
+    IsFreeGroup G :=
+  (FreeGroupBasis.ofLift X of lift lift_of).isFreeGroup
 
-/-- If a group satisfies the universal property of a free group, then it is a free group, where
-the universal property is expressed as in `IsFreeGroup.unique_lift`.  -/
-noncomputable def ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G)
+/-- If a group satisfies the universal property of a free group with respect to a given type, then
+it is free. Here the universal property is expressed as in `IsFreeGroup.unique_lift`.  -/
+lemma ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G)
     (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a) :
     IsFreeGroup G :=
-  let lift {H : Type u} [Group H] : (X → H) ≃ (G →* H) :=
-    { toFun := fun f => Classical.choose (h f)
-      invFun := fun F => F ∘ of
-      left_inv := fun f => funext (Classical.choose_spec (h f)).left
-      right_inv := fun F => ((Classical.choose_spec (h (F ∘ of))).right F fun _ => rfl).symm }
-  let lift_of {H : Type u} [Group H] (f : X → H) (a : X) : lift f (of a) = f a :=
-    congr_fun (lift.symm_apply_apply f) a
-  ofLift X of @lift @lift_of
-#align is_free_group.of_unique_lift IsFreeGroup.ofUniqueLift
-
-/-- Being a free group transports across group isomorphisms. -/
-def ofMulEquiv {H : Type _} [Group H] (h : G ≃* H) : IsFreeGroup H
-    where
-  Generators := Generators G
-  MulEquiv' := (MulEquiv G).trans h
-#align is_free_group.of_mul_equiv IsFreeGroup.ofMulEquiv
+  (FreeGroupBasis.ofUniqueLift X of h).isFreeGroup
+
+lemma ofMulEquiv [IsFreeGroup G] (e : G ≃* H) : IsFreeGroup H :=
+  ((basis G).map e).isFreeGroup
 
 end IsFreeGroup

Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean

@@ -121,7 +121,7 @@ instance actionGroupoidIsFree {G A : Type u} [Group G] [IsFreeGroup G] [MulActio
     · suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id _ by
         -- Porting note: `MonoidHom.ext_iff` has been deprecated.
         exact FunLike.ext_iff.mp this
-      ext
+      apply IsFreeGroup.ext_hom (fun x ↦ ?_)
       rw [MonoidHom.comp_apply, hF']
       rfl
     · rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b⟩ ⟨e, h : IsFreeGroup.of e • a = b⟩
@@ -222,7 +222,7 @@ def functorOfMonoidHom {X} [Monoid X] (f : End (root' T) →* X) : G ⥤ Categor
 /-- Given a free groupoid and an arborescence of its generating quiver, the vertex
     group at the root is freely generated by loops coming from generating arrows
     in the complement of the tree. -/
-def endIsFree : IsFreeGroup (End (root' T)) :=
+lemma endIsFree : IsFreeGroup (End (root' T)) :=
   IsFreeGroup.ofUniqueLift ((wideSubquiverEquivSetTotal <| wideSubquiverSymmetrify T)ᶜ : Set _)
     (fun e => loopOfHom T (of e.val.hom))
     (by