# mathlibdocumentation

group_theory.is_free_group

# Free groups structures on arbitrary types #

This file defines the universal property of free groups, and proves some things about groups with this property. For an 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.lift - the (noncomputable) universal property of the free group
• is_free_group.to_free_group - any free group with generators A is equivalent to free_group A.

## Implementation notes #

While the typeclass only requires the universal property hold within a single universe u, our explicit construction of free_group allows this to be extended universe polymorphically. The primed definition names in this file refer to the non-polymorphic versions.

@[class]
structure is_free_group (G : Type u) [group G] :
Type (u+1)
• generators : Type ?
• of :
• unique_lift' : ∀ {X : Type ?} [_inst_1_1 : group X] (f : → X), ∃! (F : G →* X), ∀ (a : , F = f a

is_free_group G means that G has the universal property of a free group, That is, it has a family generators G of elements, such that a group homomorphism G →* X is uniquely determined by a function generators G → X.

Instances
@[instance]
def free_group_is_free_group {A : Type u_1} :
Equations
@[simp]
theorem is_free_group.lift'_symm_apply {G H : Type u} [group G] [group H] (F : G →* H) (ᾰ : is_free_group.generators G) :
=
def is_free_group.lift' {G H : Type u} [group G] [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'_of {G H : Type u} [group G] [group H] (f : → H) (a : is_free_group.generators G) :
= f a
@[simp]
theorem is_free_group.lift'_eq_free_group_lift {H : Type u} [group H] {A : Type u} :
@[simp]
theorem is_free_group.of_eq_free_group_of {A : Type u} :
@[ext]
theorem is_free_group.ext_hom' {G H : Type u} [group G] [group H] ⦃f g : G →* H⦄ (h : ∀ (a : , f = g ) :
f = g
def is_free_group.of_mul_equiv {G H : Type u} [group G] [group H] (h : G ≃* H) :

Being a free group transports across group isomorphisms within a universe.

Equations

### Universe-polymorphic definitions #

The primed definitions and lemmas above require G and H to be in the same universe u. The lemmas below use X in a different universe w

def is_free_group.to_free_group (G : Type u) [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) [group G] (ᾰ : free_group ) :
@[simp]
theorem is_free_group.to_free_group_apply (G : Type u) [group G] (ᾰ : G) :
def is_free_group.lift {G : Type u} {X : Type w} [group G] [group X]  :
→ X) (G →* X)

A universe-polymorphic version of is_free_group.lift'.

Equations
@[simp]
theorem is_free_group.lift_symm_apply {G : Type u} {X : Type w} [group G] [group X] (F : G →* X) (ᾰ : is_free_group.generators G) :
=
@[ext]
theorem is_free_group.ext_hom {G : Type u} {X : Type w} [group G] [group X] ⦃f g : G →* X⦄ (h : ∀ (a : , f = g ) :
f = g
@[simp]
theorem is_free_group.lift_of {G : Type u} {X : Type w} [group G] [group X] (f : → X) (a : is_free_group.generators G) :
= f a
@[simp]
theorem is_free_group.lift_eq_free_group_lift {H : Type u} [group H] {A : Type u} :
theorem is_free_group.unique_lift {G : Type u} [group G] {X : Type w} [group X] (f : → X) :
∃! (F : G →* X), ∀ (a : , F = f a

A universe-polymorphic version of unique_lift.