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ι
toG
such thatG
is free over its image. Equivalently, an isomorphism betweenG
andFreeGroup ι
. 
IsFreeGroup G
: a typeclass to indicate thatG
is free over some generators 
Generators G
: given a group satisfyingIsFreeGroup G
, some indexing type over whichG
is free. 
IsFreeGroup.of
: the canonical injection ofG
's generators intoG

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 generatorsA
is equivalent toFreeGroup 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 groupG
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
.