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

The generators of a free group.

Generators : Type uThe 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

## Equations

- instIsFreeGroupFreeGroupInstGroupFreeGroup X = { Generators := X, MulEquiv' := MulEquiv.refl (FreeGroup X) }

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

## Equations

- IsFreeGroup.MulEquiv G = IsFreeGroup.MulEquiv'

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

## Equations

The canonical injection of G's generators into G

## Equations

- IsFreeGroup.of = (IsFreeGroup.MulEquiv G).toEquiv.toFun ∘ FreeGroup.of

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

## Equations

- One or more equations did not get rendered due to their size.

The universal property of a free group: A functions 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.

## Equations

- One or more equations did not get rendered due to their size.

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`

.

## Equations

- One or more equations did not get rendered due to their size.

Being a free group transports across group isomorphisms.

## Equations

- IsFreeGroup.ofMulEquiv h = { Generators := IsFreeGroup.Generators G, MulEquiv' := MulEquiv.trans (IsFreeGroup.MulEquiv G) h }