# 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
theorem IsFreeGroup.nonempty_basis {G : Type u} [] [self : ] :
∃ (ι : Type u), Nonempty ()
instance FreeGroupBasis.instFunLike {ι : Type u_1} {G : Type u_3} [] :
FunLike () ι G

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

Equations
• FreeGroupBasis.instFunLike = { coe := fun (b : ) (i : ι) => b.repr.symm (), coe_injective' := }
@[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
• b.reindex e = { repr := b.repr.trans }
Instances For
@[simp]
theorem FreeGroupBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [] (b : ) (e : ι ι') (x : ι') :
(b.reindex e) 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
• b.map e = { repr := e.symm.trans b.repr }
Instances For
@[simp]
theorem FreeGroupBasis.map_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) (e : G ≃* H) (x : ι) :
(b.map e) 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.

Equations
• =
@[simp]
theorem FreeGroupBasis.lift_symm_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [] [] (b : ) :
∀ (a : G →* H) (a_1 : ι), b.lift.symm a a_1 = a (b.repr.symm (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), (b.lift 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
• FreeGroupBasis.ofLift X of lift lift_of = { repr := ((FreeGroup.lift of).toMulEquiv (lift FreeGroup.of) ).symm }
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
• = .choose
Instances For
theorem IsFreeGroup.mulEquiv_def (G : Type u_2) [] [] :
= .some.repr.symm
@[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 := .symm }
Instances For
@[simp]
theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [] [] :
∀ (a : G), = .symm a
@[simp]
theorem IsFreeGroup.toFreeGroup_symm_apply (G : Type u_1) [] [] :
∀ (a : ), .symm a = a
def IsFreeGroup.toFreeGroup (G : Type u_1) [] [] :

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

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

The canonical injection of G's generators into G

Equations
• IsFreeGroup.of = .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 = .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) :