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 isomorphism 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 thatG
is free over some generatorsIsFreeGroup.of
- the canonical injection ofG
's generators intoG
IsFreeGroup.lift
- the universal property of the free group
Main results #
IsFreeGroup.toFreeGroup
- any free group with generatorsA
is equivalent toFreeGroup A
.IsFreeGroup.unique_lift
- the universal property of a free groupIsFreeGroup.ofUniqueLift
- constructingIsFreeGroup
from the universal property
- Generators : Type u
The generators of a free group.
- MulEquiv' : FreeGroup (IsFreeGroup.Generators G) ≃* G
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 makesG
an explicit variable.
IsFreeGroup G
means that G
isomorphic to a free group.
Instances
Any free group is isomorphic to "the" free group.
Instances For
Any free group is isomorphic to "the" free group.
Instances For
The canonical injection of G's generators into G
Instances For
The equivalence between functions on the generators and group homomorphisms from a free group given by those generators.
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, then it is a free group, where
the universal property is expressed as in IsFreeGroup.lift
and its properties.
Instances For
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
.
Instances For
Being a free group transports across group isomorphisms.