Free groups structures on arbitrary types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

@[class]

structure is_free_group (G : Type u) [group G] :

Type (u+1)

generators : Type ?
mul_equiv : free_group (is_free_group.generators G) ≃* G

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

source

@[protected, instance]

def free_group.is_free_group (X : Type u_1) :

is_free_group (free_group X)

Equations

free_group.is_free_group X = {generators := X, mul_equiv := mul_equiv.refl (free_group X) free_group.has_mul}

source

def is_free_group.to_free_group (G : Type u_1) [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 = (is_free_group.mul_equiv G).symm

source

@[simp]

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

⇑((is_free_group.to_free_group G).symm) ᾰ = ⇑(is_free_group.mul_equiv G) ᾰ

source

@[simp]

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

⇑(is_free_group.to_free_group G) ᾰ = ⇑(↑(is_free_group.mul_equiv G).symm) ᾰ

source

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

is_free_group.generators G → G

The canonical injection of G's generators into G

Equations

is_free_group.of = (is_free_group.mul_equiv G).to_fun ∘ free_group.of

source

@[simp]

theorem is_free_group.of_eq_free_group_of {A : Type u} :

is_free_group.of = free_group.of

source

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

(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 = free_group.lift.trans {to_fun := λ (f : free_group (is_free_group.generators G) →* H), f.comp (is_free_group.mul_equiv G).symm.to_monoid_hom, inv_fun := λ (f : G →* H), f.comp (is_free_group.mul_equiv G).to_monoid_hom, left_inv := _, right_inv := _}

source

@[simp]

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

is_free_group.lift = free_group.lift

source

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

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

source

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

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

source

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

source

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.

source

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

is_free_group G

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

is_free_group.of_lift X of lift lift_of = {generators := X, mul_equiv := (⇑free_group.lift of).to_mul_equiv (⇑lift free_group.of) _ _}

source

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

is_free_group G

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

is_free_group.of_unique_lift X of h = let lift : Π {H : Type u} [_inst_6 : group H], (X → H) ≃ (G →* H) := λ {H : Type u} [_inst_6 : group H], {to_fun := λ (f : X → H), classical.some _, inv_fun := λ (F : G →* H), ⇑F ∘ of, left_inv := _, right_inv := _}, lift_of : ∀ {H : Type u} [_inst_6 : group H] (f : X → H) (a : X), ⇑(⇑lift f) (of a) = f a := _ in is_free_group.of_lift X of lift lift_of

source

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

is_free_group H

Being a free group transports across group isomorphisms.

Equations

is_free_group.of_mul_equiv h = {generators := is_free_group.generators G _inst_2, mul_equiv := (is_free_group.mul_equiv G).trans h}