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

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

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

- Generators : Type u
The generators of a free group.

- MulEquiv' : FreeGroup (IsFreeGroup.Generators G) ≃* G
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.

`IsFreeGroup G`

means that `G`

isomorphic to a free group.

## Instances

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

## Instances For

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

## Instances For

The canonical injection of G's generators into G

## Instances For

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

## Instances For

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.

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.

## Instances For

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`

.

## Instances For

Being a free group transports across group isomorphisms.