# mathlibdocumentation

group_theory.is_free_group

# 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 that G is free over some generators
• is_free_group.of - the canonical injection of G's generators into G
• is_free_group.lift - the universal property of the free group

## Main results #

• is_free_group.to_free_group - any free group with generators A is equivalent to free_group A.
• is_free_group.unique_lift - the universal property of a free group
• is_free_group.of_unique_lift - constructing is_free_group from the universal property
@[class]
structure is_free_group (G : Type u) [group G] :
Type (u+1)
• generators : Type ?
• mul_equiv :

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
@[protected, instance]
def free_group.is_free_group (X : Type u_1) :
Equations
def is_free_group.to_free_group (G : Type u_1) [group G]  :

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

Equations
@[simp]
theorem is_free_group.to_free_group_symm_apply (G : Type u_1) [group G] (ᾰ : free_group ) :
=
@[simp]
theorem is_free_group.to_free_group_apply (G : Type u_1) [group G] (ᾰ : G) :
=
def is_free_group.of {G : Type u_1} [group G]  :

The canonical injection of G's generators into G

Equations
@[simp]
theorem is_free_group.of_eq_free_group_of {A : Type u} :
def is_free_group.lift {G : Type u_1} [group G] {H : Type u_2} [group H] :
→ H) (G →* H)

The equivalence between functions on the generators and group homomorphisms from a free group given by those generators.

Equations
@[simp]
theorem is_free_group.lift'_eq_free_group_lift {H : Type u_2} [group H] {A : Type u} :
@[simp]
theorem is_free_group.lift_of {G : Type u_1} [group G] {H : Type u_2} [group H] (f : → H) (a : is_free_group.generators G) :
= f a
@[simp]
theorem is_free_group.lift_symm_apply {G : Type u_1} [group G] {H : Type u_2} [group H] (f : G →* H) (a : is_free_group.generators G) :
a = f
@[ext]
theorem is_free_group.ext_hom {G : Type u_1} [group G] {H : Type u_2} [group H] ⦃f g : G →* H⦄ (h : ∀ (a : , f = g ) :
f = g
theorem is_free_group.unique_lift {G : Type u_1} [group G] {H : Type u_2} [group H] (f : → H) :
∃! (F : G →* H), ∀ (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 is_free_group.lift is expressed as a bijection, it already expresses the universal property.

def is_free_group.of_lift {G : Type u} [group G] (X : Type u) (of : X → G) (lift : Π {H : Type u} [_inst_5 : group H], (X → H) (G →* H)) (lift_of : ∀ {H : Type u} [_inst_6 : group H] (f : X → H) (a : X), (lift 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 is_free_group.lift and its properties.

Equations
noncomputable def is_free_group.of_unique_lift {G : Type u} [group G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [_inst_5 : group H] (f : X → H), ∃! (F : G →* H), ∀ (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 is_free_group.unique_lift.

Equations
def is_free_group.of_mul_equiv {G : Type u_1} [group G] {H : Type u_1} [group H] (h : G ≃* H) :

Being a free group transports across group isomorphisms.

Equations