# Documentation

Mathlib.GroupTheory.IsFreeGroup

# 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
class IsFreeGroup (G : Type u) [inst : ] :
Type (u+1)
• The generators of a free group.

Generators : Type u
• 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.

MulEquiv' : FreeGroup Generators ≃* G

IsFreeGroup G means that G isomorphic to a free group.

Instances
Equations
• = { Generators := X, MulEquiv' := }
def IsFreeGroup.MulEquiv (G : Type u_1) [inst : ] [inst : ] :

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

Equations
• = IsFreeGroup.MulEquiv'
@[simp]
theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [inst : ] [inst : ] :
∀ (a : G), ↑() a = ↑() a
@[simp]
theorem IsFreeGroup.toFreeGroup_symm_apply (G : Type u_1) [inst : ] [inst : ] :
∀ (a : ), ↑() a = ↑() a
def IsFreeGroup.toFreeGroup (G : Type u_1) [inst : ] [inst : ] :

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

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

The canonical injection of G's generators into G

Equations
• IsFreeGroup.of = ().toEquiv.toFun FreeGroup.of
@[simp]
theorem IsFreeGroup.of_eq_freeGroup_of {A : Type u} :
IsFreeGroup.of = FreeGroup.of
def IsFreeGroup.lift {G : Type u_1} [inst : ] [inst : ] {H : Type u_2} [inst : ] :
() (G →* H)

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.
@[simp]
theorem IsFreeGroup.lift'_eq_freeGroup_lift {H : Type u_1} [inst : ] {A : Type u} :
IsFreeGroup.lift = FreeGroup.lift
@[simp]
theorem IsFreeGroup.lift_of {G : Type u_1} [inst : ] [inst : ] {H : Type u_2} [inst : ] (f : ) (a : ) :
↑(IsFreeGroup.lift f) () = f a
@[simp]
theorem IsFreeGroup.lift_symm_apply {G : Type u_1} [inst : ] [inst : ] {H : Type u_2} [inst : ] (f : G →* H) (a : ) :
↑(Equiv.symm IsFreeGroup.lift) f a = f ()
theorem IsFreeGroup.ext_hom {G : Type u_1} [inst : ] [inst : ] {H : Type u_2} [inst : ] ⦃f : G →* H ⦃g : G →* H (h : ∀ (a : ), f () = g ()) :
f = g
theorem IsFreeGroup.unique_lift {G : Type u_1} [inst : ] [inst : ] {H : Type u_2} [inst : ] (f : ) :
∃! F, ∀ (a : ), F () = f a

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.

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

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.
noncomputable def IsFreeGroup.ofUniqueLift {G : Type u} [inst : ] (X : Type u) (of : XG) (h : ∀ {H : Type u} [inst : ] (f : XH), ∃! F, ∀ (a : X), F (of a) = f a) :

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.
def IsFreeGroup.ofMulEquiv {G : Type u_1} [inst : ] [inst : ] {H : Type u_1} [inst : ] (h : G ≃* H) :

Being a free group transports across group isomorphisms.

Equations
• = { Generators := , MulEquiv' := }