Free groups structures on arbitrary types

This file defines the notion of free basis of a group, which induces an isomorphism between the group and the free group generated by the basis.

It also introduced a type class for groups which are free groups, i.e., for which some free basis exists.

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

Main definitions

• FreeGroupBasis ι G : a function from ι to G such that G is free over its image. Equivalently, an isomorphism between G and FreeGroup ι.

• IsFreeGroup G : a typeclass to indicate that G is free over some generators

• Generators G : given a group satisfying IsFreeGroup G, some indexing type over which G is free.

• IsFreeGroup.of : the canonical injection of G's generators into G

• IsFreeGroup.lift : the universal property of the free group

Main results

• FreeGroupBasis.isFreeGroup: a group admitting a free group basis is free.
• IsFreeGroup.toFreeGroup: any free group with generators A is equivalent to FreeGroup A.
• IsFreeGroup.unique_lift: the universal property of a free group.
• FreeGroupBasis.ofUniqueLift: a group satisfying the universal property of a free group admits a free group basis.

structure FreeGroupBasis (ι : Type u_1) (G : Type u_2) [Group G] : Type (max u_1 u_2)

A free group basis FreeGroupBasis ι G is a structure recording the isomorphism between a group G and the free group over ι. One may think of such a basis as a function from ι to G (which is registered through a FunLike instance) together with the fact that the morphism induced by this function from FreeGroup ι to G is an isomorphism.

• ofRepr :: (
• repr : G ≃* FreeGroup ι

  repr is the isomorphism between the group G and the free group generated by ι.

• )

class IsFreeGroup (G : Type u) [Group G] : Prop

A group is free if it admits a free group basis. In the definition, we require the basis to be in the same universe as G, although this property follows from the existence of a basis in any universe, see FreeGroupBasis.isFreeGroup.

• nonempty_basis : ∃ (ι : Type u), Nonempty (FreeGroupBasis ι G)

instance FreeGroupBasis.instFunLike {ι : Type u_1} {G : Type u_3} [Group G] : FunLike (FreeGroupBasis ι G) ι G

A free group basis for G over ι is associated to a map ι → G recording the images of the generators.

Equations

• FreeGroupBasis.instFunLike = { coe := fun (b : FreeGroupBasis ι G) (i : ι) => (MulEquiv.symm b.repr) (FreeGroup.of i), coe_injective' := ⋯ }

@[simp]

theorem FreeGroupBasis.repr_apply_coe {ι : Type u_1} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) (i : ι) : b.repr (b i) = FreeGroup.of i

def FreeGroupBasis.ofFreeGroup (X : Type u_5) : FreeGroupBasis X (FreeGroup X)

The canonical basis of the free group over X.

Equations

• FreeGroupBasis.ofFreeGroup X = { repr := MulEquiv.refl (FreeGroup X) }

@[simp]

theorem FreeGroupBasis.ofFreeGroup_apply {X : Type u_5} (x : X) : (FreeGroupBasis.ofFreeGroup X) x = FreeGroup.of x

def FreeGroupBasis.reindex {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) (e : ι ≃ ι') : FreeGroupBasis ι' G

Reindex a free group basis through a bijection of the indexing sets.

Equations

• FreeGroupBasis.reindex b e = { repr := MulEquiv.trans b.repr (FreeGroup.freeGroupCongr e) }

@[simp]

theorem FreeGroupBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) (e : ι ≃ ι') (x : ι') : (FreeGroupBasis.reindex b e) x = b (e.symm x)

def FreeGroupBasis.map {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (e : G ≃* H) : FreeGroupBasis ι H

Pushing a free group basis through a group isomorphism.

Equations

• FreeGroupBasis.map b e = { repr := MulEquiv.trans (MulEquiv.symm e) b.repr }

@[simp]

theorem FreeGroupBasis.map_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (e : G ≃* H) (x : ι) : (FreeGroupBasis.map b e) x = e (b x)

theorem FreeGroupBasis.injective {ι : Type u_1} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) : Function.Injective ⇑b

theorem FreeGroupBasis.isFreeGroup {ι : Type u_1} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) : IsFreeGroup G

A group admitting a free group basis is a free group.

instance FreeGroupBasis.instIsFreeGroupFreeGroupInstGroupFreeGroup (X : Type u_5) : IsFreeGroup (FreeGroup X)

Equations

• ⋯ = ⋯

@[simp]

theorem FreeGroupBasis.lift_symm_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) : ∀ (a : G →* H) (a_1 : ι), (FreeGroupBasis.lift b).symm a a_1 = a ((MulEquiv.symm b.repr) (FreeGroup.of a_1))

@[simp]

theorem FreeGroupBasis.lift_apply_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) : ∀ (a : ι → H) (a_1 : G), ((FreeGroupBasis.lift b) a) a_1 = (FreeGroup.lift a) (b.repr a_1)

def FreeGroupBasis.lift {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) : (ι → H) ≃ (G →* H)

Given a free group basis of G over ι, there is a canonical bijection between maps from ι to a group H and morphisms from G to H.

Equations

• One or more equations did not get rendered due to their size.

theorem FreeGroupBasis.ext_hom {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (f : G →* H) (g : G →* H) (h : ∀ (i : ι), f (b i) = g (b i)) : f = g

If two morphisms on G coincide on the elements of a basis, then they coincide.

def FreeGroupBasis.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 f) (of a) = f a) : FreeGroupBasis X G

If a group satisfies the universal property of a free group with respect to a given type, then it admits a free group basis based on this type. Here, the universal property is expressed as in IsFreeGroup.lift and its properties.

Equations

• FreeGroupBasis.ofLift X of lift lift_of = { repr := MulEquiv.symm (MonoidHom.toMulEquiv (FreeGroup.lift of) (lift FreeGroup.of) ⋯ ⋯) }

def FreeGroupBasis.ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [inst : Group H] (f : X → H), ∃! F : G →* H, ∀ (a : X), F (of a) = f a) : FreeGroupBasis X G

If a group satisfies the universal property of a free group with respect to a given type, then it admits a free group basis based on this type. Here the universal property is expressed as in IsFreeGroup.unique_lift.

Equations

• One or more equations did not get rendered due to their size.

def IsFreeGroup.Generators (G : Type u_1) [Group G] [IsFreeGroup G] : Type u_1

A set of generators of a free group, chosen arbitrarily

Equations

• IsFreeGroup.Generators G = Exists.choose ⋯

@[irreducible]

def IsFreeGroup.mulEquiv (G : Type u_2) [Group G] [IsFreeGroup G] : FreeGroup (IsFreeGroup.Generators G) ≃* G

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

Equations

• IsFreeGroup.mulEquiv = IsFreeGroup.wrapped✝.1

theorem IsFreeGroup.mulEquiv_def (G : Type u_2) [Group G] [IsFreeGroup G] : IsFreeGroup.mulEquiv G = MulEquiv.symm (Nonempty.some ⋯).repr

def IsFreeGroup.basis (G : Type u_1) [Group G] [IsFreeGroup G] : FreeGroupBasis (IsFreeGroup.Generators G) G

A free group basis of a free group G, over the set Generators G.

Equations

• IsFreeGroup.basis G = { repr := MulEquiv.symm (IsFreeGroup.mulEquiv G) }

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

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

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.

Equations

• IsFreeGroup.toFreeGroup G = MulEquiv.symm (IsFreeGroup.mulEquiv G)

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

The canonical injection of G's generators into G

Equations

• IsFreeGroup.of = (IsFreeGroup.mulEquiv G).toFun ∘ 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.

Equations

• IsFreeGroup.lift = FreeGroupBasis.lift (IsFreeGroup.basis G)

@[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 : G →* H, ∀ (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.

theorem 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 f) (of a) = f a) : IsFreeGroup G

If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here, the universal property is expressed as in IsFreeGroup.lift and its properties.

theorem IsFreeGroup.ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [inst : Group H] (f : X → H), ∃! F : G →* H, ∀ (a : X), F (of a) = f a) : IsFreeGroup G

If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here the universal property is expressed as in IsFreeGroup.unique_lift.

theorem IsFreeGroup.ofMulEquiv {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (e : G ≃* H) : IsFreeGroup H