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 group_theory/free_group
.
Main definitions #
is_free_group G
- a typeclass to indicate thatG
is free over some generatorsis_free_group.of
- the canonical injection ofG
's generators intoG
is_free_group.lift
- the universal property of the free group
Main results #
is_free_group.to_free_group
- any free group with generatorsA
is equivalent tofree_group A
.is_free_group.unique_lift
- the universal property of a free groupis_free_group.of_unique_lift
- constructingis_free_group
from the universal property
- generators : Type ?
- mul_equiv : free_group (is_free_group.generators G) ≃* G
is_free_group G
means that G
isomorphic to a free group.
Instances of this typeclass
Instances of other typeclasses for is_free_group
- is_free_group.has_sizeof_inst
Equations
- free_group.is_free_group X = {generators := X, mul_equiv := mul_equiv.refl (free_group X) free_group.has_mul}
Any free group is isomorphic to "the" free group.
Equations
The canonical injection of G's generators into G
Equations
The equivalence between functions on the generators and group homomorphisms from a free group given by those generators.
Equations
- is_free_group.lift = free_group.lift.trans {to_fun := λ (f : free_group (is_free_group.generators G) →* H), f.comp (is_free_group.mul_equiv G).symm.to_monoid_hom, inv_fun := λ (f : G →* H), f.comp (is_free_group.mul_equiv G).to_monoid_hom, left_inv := _, right_inv := _}
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 is_free_group.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 is_free_group.lift
and its properties.
Equations
- is_free_group.of_lift X of lift lift_of = {generators := X, mul_equiv := (⇑free_group.lift of).to_mul_equiv (⇑lift free_group.of) _ _}
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 is_free_group.unique_lift
.
Equations
- is_free_group.of_unique_lift X of h = let lift : Π {H : Type u} [_inst_6 : group H], (X → H) ≃ (G →* H) := λ {H : Type u} [_inst_6 : group H], {to_fun := λ (f : X → H), classical.some _, inv_fun := λ (F : G →* H), ⇑F ∘ of, left_inv := _, right_inv := _}, lift_of : ∀ {H : Type u} [_inst_6 : group H] (f : X → H) (a : X), ⇑(⇑lift f) (of a) = f a := _ in is_free_group.of_lift X of lift lift_of
Being a free group transports across group isomorphisms.
Equations
- is_free_group.of_mul_equiv h = {generators := is_free_group.generators G _inst_2, mul_equiv := (is_free_group.mul_equiv G).trans h}