mathlib documentation

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 #

Main results #

@[class]
structure is_free_group (G : Type u) [group G] :
Type (u+1)

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

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

Equations
def is_free_group.of {G : Type u_1} [group G] [is_free_group G] :

The canonical injection of G's generators into G

Equations
def is_free_group.lift {G : Type u_1} [group G] [is_free_group G] {H : Type u_2} [group H] :

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

Equations
@[simp]
@[simp]
theorem is_free_group.lift_of {G : Type u_1} [group G] [is_free_group G] {H : Type u_2} [group H] (f : is_free_group.generators G → H) (a : is_free_group.generators G) :
@[simp]
theorem is_free_group.lift_symm_apply {G : Type u_1} [group G] [is_free_group G] {H : Type u_2} [group H] (f : G →* H) (a : is_free_group.generators G) :
@[ext]
theorem is_free_group.ext_hom {G : Type u_1} [group G] [is_free_group G] {H : Type u_2} [group H] ⦃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
theorem is_free_group.unique_lift {G : Type u_1} [group G] [is_free_group G] {H : Type u_2} [group H] (f : is_free_group.generators G → H) :
∃! (F : G →* H), ∀ (a : is_free_group.generators G), F (is_free_group.of a) = 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] [is_free_group G] {H : Type u_1} [group H] (h : G ≃* H) :

Being a free group transports across group isomorphisms.

Equations