# Documentation

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

# Free groups structures on arbitrary types #

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 #

• 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 #

• 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.
structure FreeGroupBasis (ι : Type u_1) (G : Type u_2) [] :
Type (max u_1 u_2)

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.

• ofRepr :: (
• repr : G ≃*

repr is the isomorphism between the group G and the free group generated by ι.

• )
Instances For
class IsFreeGroup (G : Type u) [] :

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.

Instances
instance FreeGroupBasis.funLike {ι : Type u_1} {G : Type u_3} [] :
FunLike () ι fun (x : ι) => G

A free group basis for G over ι is associated to a map ι → G recording the images of the generators.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem FreeGroupBasis.repr_apply_coe {ι : Type u_1} {G : Type u_3} [] (b : ) (i : ι) :
b.repr (b i) =

The canonical basis of the free group over X.

Equations
• = { repr := }
Instances For
@[simp]
theorem FreeGroupBasis.ofFreeGroup_apply {X : Type u_5} (x : X) :
def FreeGroupBasis.reindex {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [] (b : ) (e : ι ι') :

Reindex a free group basis through a bijection of the indexing sets.

Equations
Instances For
@[simp]
theorem FreeGroupBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [] (b : ) (e : ι ι') (x : ι') :
() x = b (e.symm x)
def FreeGroupBasis.map {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) (e : G ≃* H) :

Pushing a free group basis through a group isomorphism.

Equations
Instances For
@[simp]
theorem FreeGroupBasis.map_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) (e : G ≃* H) (x : ι) :
() x = e (b x)
theorem FreeGroupBasis.injective {ι : Type u_1} {G : Type u_3} [] (b : ) :
theorem FreeGroupBasis.isFreeGroup {ι : Type u_1} {G : Type u_3} [] (b : ) :

A group admitting a free group basis is a free group.

@[simp]
theorem FreeGroupBasis.lift_symm_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) :
∀ (a : G →* H) (a_1 : ι), .symm a a_1 = a ((MulEquiv.symm b.repr) (FreeGroup.of a_1))
@[simp]
theorem FreeGroupBasis.lift_apply_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) :
∀ (a : ιH) (a_1 : G), ( a) a_1 = (FreeGroup.lift a) (b.repr a_1)
def FreeGroupBasis.lift {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) :
(ιH) (G →* H)

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem FreeGroupBasis.ext_hom {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) (f : G →* H) (g : G →* H) (h : ∀ (i : ι), f (b i) = g (b i)) :
f = g

If two morphisms on G coincide on the elements of a basis, then they coincide.

def FreeGroupBasis.ofLift {G : Type u} [] (X : Type u) (of : XG) (lift : {H : Type u} → [inst : ] → (XH) (G →* H)) (lift_of : ∀ {H : Type u} [inst : ] (f : XH) (a : X), (lift f) (of a) = f a) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FreeGroupBasis.ofUniqueLift {G : Type u} [] (X : Type u) (of : XG) (h : ∀ {H : Type u} [inst : ] (f : XH), ∃! (F : G →* H), ∀ (a : X), F (of a) = f a) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def IsFreeGroup.Generators (G : Type u_1) [] [] :
Type u_1

A set of generators of a free group, chosen arbitrarily

Equations
Instances For
theorem IsFreeGroup.MulEquiv_def (G : Type u_2) [] [] :
= MulEquiv.symm (Nonempty.some (_ : Nonempty (FreeGroupBasis (Exists.choose (_ : ∃ (ι : Type u_2), Nonempty ())) G))).repr
@[irreducible]
def IsFreeGroup.MulEquiv (G : Type u_2) [] [] :

Any free group is isomorphic to "the" free group.

Equations
Instances For
def IsFreeGroup.basis (G : Type u_1) [] [] :

A free group basis of a free group G, over the set Generators G.

Equations
• = { repr := }
Instances For
@[simp]
theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [] [] :
∀ (a : G), =
@[simp]
theorem IsFreeGroup.toFreeGroup_symm_apply (G : Type u_1) [] [] :
∀ (a : ), = a
def IsFreeGroup.toFreeGroup (G : Type u_1) [] [] :

Any free group is isomorphic to "the" free group.

Equations
Instances For
def IsFreeGroup.of {G : Type u_1} [] [] :

The canonical injection of G's generators into G

Equations
• IsFreeGroup.of = .toEquiv.toFun FreeGroup.of
Instances For
def IsFreeGroup.lift {G : Type u_1} [] [] {H : Type u_2} [] :
() (G →* H)

The equivalence between functions on the generators and group homomorphisms from a free group given by those generators.

Equations
• IsFreeGroup.lift =
Instances For
@[simp]
theorem IsFreeGroup.lift_of {G : Type u_1} [] [] {H : Type u_2} [] (f : ) (a : ) :
(IsFreeGroup.lift f) () = f a
@[simp]
theorem IsFreeGroup.lift_symm_apply {G : Type u_1} [] [] {H : Type u_2} [] (f : G →* H) (a : ) :
IsFreeGroup.lift.symm f a = f ()
theorem IsFreeGroup.ext_hom {G : Type u_1} [] [] {H : Type u_2} [] ⦃f : G →* H ⦃g : G →* H (h : ∀ (a : ), f () = g ()) :
f = g
theorem IsFreeGroup.unique_lift {G : Type u_1} [] [] {H : Type u_2} [] (f : ) :
∃! (F : G →* H), ∀ (a : ), F () = f a

The universal property of a free group: A function from the generators of G to another group extends in a unique way to a homomorphism from G.

Note that since IsFreeGroup.lift is expressed as a bijection, it already expresses the universal property.

theorem IsFreeGroup.ofLift {G : Type u} [] (X : Type u) (of : XG) (lift : {H : Type u} → [inst : ] → (XH) (G →* H)) (lift_of : ∀ {H : Type u} [inst : ] (f : XH) (a : X), (lift f) (of a) = f a) :

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.

theorem IsFreeGroup.ofUniqueLift {G : Type u} [] (X : Type u) (of : XG) (h : ∀ {H : Type u} [inst : ] (f : XH), ∃! (F : G →* H), ∀ (a : X), F (of a) = f a) :

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.

theorem IsFreeGroup.ofMulEquiv {G : Type u_1} [] {H : Type u_2} [] [] (e : G ≃* H) :