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 isomorphism to the canonical free group, or by proving that the universal property holds.

For the explicit construction of free groups, see GroupTheory/FreeGroup.

Main definitions

• IsFreeGroup G - a typeclass to indicate that G is free over some generators
• IsFreeGroup.of - the canonical injection of G's generators into G
• IsFreeGroup.lift - the universal property of the free group

Main results

• IsFreeGroup.toFreeGroup - any free group with generators A is equivalent to FreeGroup A.
• IsFreeGroup.unique_lift - the universal property of a free group
• IsFreeGroup.ofUniqueLift - constructing IsFreeGroup from the universal property

class IsFreeGroup (G : Type u) [Group G] : Type (u + 1)

• Generators : Type u

  The generators of a free group.

• MulEquiv' : FreeGroup (IsFreeGroup.Generators G) ≃* G

  The multiplicative equivalence between "the" free group on the generators, and the given group G. Note: IsFreeGroup.MulEquiv' should not be used directly. IsFreeGroup.MulEquiv should be used instead because it makes G an explicit variable.

IsFreeGroup G means that G isomorphic to a free group.

instance instIsFreeGroupFreeGroupInstGroupFreeGroup (X : Type u_1) : IsFreeGroup (FreeGroup X)

def IsFreeGroup.MulEquiv (G : Type u_1) [Group G] [IsFreeGroup G] : FreeGroup (IsFreeGroup.Generators G) ≃* G

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

@[simp]

theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [Group G] [IsFreeGroup G] : ∀ (a : G), ↑(IsFreeGroup.toFreeGroup G) a = ↑(MulEquiv.symm (IsFreeGroup.MulEquiv G)) a

@[simp]

theorem IsFreeGroup.toFreeGroup_symm_apply (G : Type u_1) [Group G] [IsFreeGroup G] : ∀ (a : FreeGroup (IsFreeGroup.Generators G)), ↑(MulEquiv.symm (IsFreeGroup.toFreeGroup G)) a = ↑(IsFreeGroup.MulEquiv G) a

def IsFreeGroup.toFreeGroup (G : Type u_1) [Group G] [IsFreeGroup G] : G ≃* FreeGroup (IsFreeGroup.Generators G)

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

def IsFreeGroup.of {G : Type u_1} [Group G] [IsFreeGroup G] : IsFreeGroup.Generators G → G

The canonical injection of G's generators into G

@[simp]

theorem IsFreeGroup.of_eq_freeGroup_of {A : Type u} : IsFreeGroup.of = FreeGroup.of

def IsFreeGroup.lift {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] : (IsFreeGroup.Generators G → H) ≃ (G →* H)

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

@[simp]

theorem IsFreeGroup.lift'_eq_freeGroup_lift {H : Type u_2} [Group H] {A : Type u} : IsFreeGroup.lift = FreeGroup.lift

@[simp]

theorem IsFreeGroup.lift_of {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : IsFreeGroup.Generators G → H) (a : IsFreeGroup.Generators G) : ↑(↑IsFreeGroup.lift f) (IsFreeGroup.of a) = f a

@[simp]

theorem IsFreeGroup.lift_symm_apply {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : G →* H) (a : IsFreeGroup.Generators G) : ↑IsFreeGroup.lift.symm f a = ↑f (IsFreeGroup.of a)

theorem IsFreeGroup.ext_hom {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] ⦃f : G →* H⦄ ⦃g : G →* H⦄ (h : ∀ (a : IsFreeGroup.Generators G), ↑f (IsFreeGroup.of a) = ↑g (IsFreeGroup.of a)) : f = g

theorem IsFreeGroup.unique_lift {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : IsFreeGroup.Generators G → H) : ∃! F, ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f a

The universal property of a free group: A function from the generators of G to another group extends in a unique way to a homomorphism from G.

Note that since IsFreeGroup.lift is expressed as a bijection, it already expresses the universal property.

def IsFreeGroup.ofLift {G : Type u} [Group G] (X : Type u) (of : X → G) (lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)) (lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑(lift H inst) f) (of a) = f a) : IsFreeGroup 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 IsFreeGroup.lift and its properties.

noncomputable def IsFreeGroup.ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [inst : Group H] (f : X → H), ∃! F, ∀ (a : X), ↑F (of a) = f a) : IsFreeGroup 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 IsFreeGroup.unique_lift.

def IsFreeGroup.ofMulEquiv {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_1} [Group H] (h : G ≃* H) : IsFreeGroup H

Being a free group transports across group isomorphisms.