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

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`

is the isomorphism between the group`G`

and the free group generated by`ι`

.- )

## Instances For

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`

.

- nonempty_basis : ∃ (ι : Type u), Nonempty (FreeGroupBasis ι G)

## Instances

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 : FreeGroupBasis ι G) (i : ι) => b.repr.symm (FreeGroup.of i), coe_injective' := ⋯ }

The canonical basis of the free group over `X`

.

## Equations

- FreeGroupBasis.ofFreeGroup X = { repr := MulEquiv.refl (FreeGroup X) }

## Instances For

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

## Equations

- b.reindex e = { repr := b.repr.trans (FreeGroup.freeGroupCongr e) }

## Instances For

Pushing a free group basis through a group isomorphism.

## Equations

- b.map e = { repr := e.symm.trans b.repr }

## Instances For

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

## Equations

- ⋯ = ⋯

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

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

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

A set of generators of a free group, chosen arbitrarily

## Equations

- IsFreeGroup.Generators G = ⋯.choose

## Instances For

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

## Equations

## Instances For

A free group basis of a free group `G`

, over the set `Generators G`

.

## Equations

- IsFreeGroup.basis G = { repr := (IsFreeGroup.mulEquiv G).symm }

## Instances For

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

## Equations

- IsFreeGroup.toFreeGroup G = (IsFreeGroup.mulEquiv G).symm

## Instances For

The canonical injection of G's generators into G

## Equations

- IsFreeGroup.of = (IsFreeGroup.mulEquiv G).toFun ∘ FreeGroup.of

## Instances For

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

## Equations

- IsFreeGroup.lift = (IsFreeGroup.basis G).lift

## 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 with respect to a given type, then
it is free. Here, the universal property is expressed as in `IsFreeGroup.lift`

and its
properties.

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`

.