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
 One or more equations did not get rendered due to their size.
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
 FreeGroupBasis.reindex b e = { repr := MulEquiv.trans b.repr (FreeGroup.freeGroupCongr e) }
Instances For
Pushing a free group basis through a group isomorphism.
Equations
 FreeGroupBasis.map b e = { repr := MulEquiv.trans (MulEquiv.symm e) b.repr }
Instances For
A group admitting a free group basis is a free group.
Equations
 (_ : IsFreeGroup (FreeGroup X)) = (_ : IsFreeGroup (FreeGroup X))
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
 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.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 = Exists.choose (_ : ∃ (ι : Type u_1), Nonempty (FreeGroupBasis ι G))
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 := MulEquiv.symm (IsFreeGroup.MulEquiv G) }
Instances For
Any free group is isomorphic to "the" free group.
Equations
Instances For
The canonical injection of G's generators into G
Equations
 IsFreeGroup.of = (IsFreeGroup.MulEquiv G).toEquiv.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 = FreeGroupBasis.lift (IsFreeGroup.basis G)
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
.