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 #

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 : is_free_group.generators G → G
unique_lift' : ∀ {X : Type ?} [_inst_1_1 : 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

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

@[protected, instance]

def free_group_is_free_group {A : Type u_1} :

is_free_group (free_group A)

Equations

free_group_is_free_group = {generators := A, of := free_group.of A, unique_lift' := _}

@[simp]

theorem is_free_group.lift'_symm_apply {G H : Type u} [group G] [group H] [is_free_group G] (F : G →* H) (ᾰ : is_free_group.generators G) :

⇑(is_free_group.lift'.symm) F ᾰ = (⇑F ∘ is_free_group.of) ᾰ

noncomputable def is_free_group.lift' {G H : Type u} [group G] [group H] [is_free_group G] :

(is_free_group.generators G → H) ≃ (G →* H)

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

Equations

is_free_group.lift' = {to_fun := λ (f : is_free_group.generators G → H), classical.some _, inv_fun := λ (F : G →* H), ⇑F ∘ is_free_group.of, left_inv := _, right_inv := _}

@[simp]

theorem is_free_group.lift'_of {G H : Type u} [group G] [group H] [is_free_group G] (f : is_free_group.generators G → H) (a : is_free_group.generators G) :

⇑(⇑is_free_group.lift' f) (is_free_group.of a) = f a

@[simp]

theorem is_free_group.lift'_eq_free_group_lift {H : Type u} [group H] {A : Type u} :

is_free_group.lift' = free_group.lift

@[simp]

theorem is_free_group.of_eq_free_group_of {A : Type u} :

is_free_group.of = free_group.of

@[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) :

is_free_group H

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

Equations

is_free_group.of_mul_equiv h = {generators := is_free_group.generators G _inst_4, of := ⇑h ∘ is_free_group.of, unique_lift' := _}

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

noncomputable def is_free_group.to_free_group (G : Type u) [group G] [is_free_group G] :

G ≃* free_group (is_free_group.generators G)

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

Equations

is_free_group.to_free_group G = {to_fun := ⇑(⇑is_free_group.lift' free_group.of), inv_fun := ⇑(⇑free_group.lift is_free_group.of), left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem is_free_group.to_free_group_symm_apply (G : Type u) [group G] [is_free_group G] (ᾰ : free_group (is_free_group.generators G)) :

⇑((is_free_group.to_free_group G).symm) ᾰ = ⇑(⇑free_group.lift is_free_group.of) ᾰ

@[simp]

theorem is_free_group.to_free_group_apply (G : Type u) [group G] [is_free_group G] (ᾰ : G) :

⇑(is_free_group.to_free_group G) ᾰ = ⇑(⇑is_free_group.lift' free_group.of) ᾰ

noncomputable def is_free_group.lift {G : Type u} {X : Type w} [group G] [group X] [is_free_group G] :

(is_free_group.generators G → X) ≃ (G →* X)

A universe-polymorphic version of is_free_group.lift'.

Equations

is_free_group.lift = {to_fun := λ (f : is_free_group.generators G → X), (⇑free_group.lift f).comp (is_free_group.to_free_group G).to_monoid_hom, inv_fun := λ (F : G →* X), ⇑F ∘ is_free_group.of, left_inv := _, right_inv := _}

@[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) :

⇑(is_free_group.lift.symm) F ᾰ = (⇑F ∘ is_free_group.of) ᾰ

@[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) :

⇑(⇑is_free_group.lift f) (is_free_group.of a) = f a

@[simp]

theorem is_free_group.lift_eq_free_group_lift {H : Type u} [group H] {A : Type u} :

is_free_group.lift = free_group.lift

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.