mathlib documentation

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 #

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)

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
@[simp]
def is_free_group.lift' {G H : Type u} [group G] [group H] [is_free_group G] :

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

Equations
@[simp]
@[ext]
theorem is_free_group.ext_hom' {G H : Type u} [group G] [group H] [is_free_group G] ⦃f g : G →* H⦄ (h : ∀ (a : is_free_group.generators G), f (is_free_group.of a) = g (is_free_group.of a)) :
f = g
def is_free_group.of_mul_equiv {G H : Type u} [group G] [group H] [is_free_group G] (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.lift {G : Type u} {X : Type w} [group G] [group X] [is_free_group G] :

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] [is_free_group G] (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] [is_free_group G] ⦃f g : G →* X⦄ (h : ∀ (a : is_free_group.generators G), f (is_free_group.of a) = g (is_free_group.of a)) :
f = g
@[simp]
theorem is_free_group.lift_of {G : Type u} {X : Type w} [group G] [group X] [is_free_group G] (f : is_free_group.generators G → X) (a : is_free_group.generators G) :
@[simp]
theorem is_free_group.unique_lift {G : Type u} [group G] [is_free_group G] {X : Type w} [group X] (f : is_free_group.generators G → X) :
∃! (F : G →* X), ∀ (a : is_free_group.generators G), F (is_free_group.of a) = f a

A universe-polymorphic version of unique_lift.