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 FreeAddGroupBasis (ι : Type u_1) (G : Type u_2) [AddGroup G] : Type (max u_1 u_2)

A free group basis FreeAddGroupBasis ι G is a structure recording the isomorphism between an additive group G and the additive 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 FreeAddGroup ι to G is an isomorphism.

• ofRepr :: (
• repr : G ≃+ FreeAddGroup ι

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

• )

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 IsFreeAddGroup (G : Type u) [AddGroup G] : Prop

An additive group is free if it admits an additive 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 FreeAddGroupBasis.isFreeAddGroup.

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

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_reducible]

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 : ι) => b.repr.symm (FreeGroup.of i), coe_injective := ⋯ }

@[instance_reducible]

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

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

Equations

• FreeAddGroupBasis.instFunLike = { coe := fun (b : FreeAddGroupBasis ι G) (i : ι) => b.repr.symm (FreeAddGroup.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

@[simp]

theorem FreeAddGroupBasis.repr_apply_coe {ι : Type u_1} {G : Type u_3} [AddGroup G] (b : FreeAddGroupBasis ι G) (i : ι) : b.repr (b i) = FreeAddGroup.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) }

def FreeAddGroupBasis.ofFreeAddGroup (X : Type u_5) : FreeAddGroupBasis X (FreeAddGroup X)

The canonical basis of the additive free group over X.

Equations

• FreeAddGroupBasis.ofFreeAddGroup X = { repr := AddEquiv.refl (FreeAddGroup X) }

@[simp]

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

@[simp]

theorem FreeAddGroupBasis.ofFreeAddGroup_apply {X : Type u_5} (x : X) : (ofFreeAddGroup X) x = FreeAddGroup.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

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

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

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

Equations

• b.reindex e = { repr := b.repr.trans (FreeAddGroup.freeAddGroupCongr e) }

@[simp]

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

@[simp]

theorem FreeAddGroupBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [AddGroup G] (b : FreeAddGroupBasis ι G) (e : ι ≃ ι') (x : ι') : (b.reindex 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

• b.map e = { repr := e.symm.trans b.repr }

def FreeAddGroupBasis.map {ι : Type u_1} {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (b : FreeAddGroupBasis ι G) (e : G ≃+ H) : FreeAddGroupBasis ι H

Pushing an additive free group basis through a group isomorphism.

Equations

• b.map e = { repr := e.symm.trans 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 : ι) : (b.map e) x = e (b x)

@[simp]

theorem FreeAddGroupBasis.map_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (b : FreeAddGroupBasis ι G) (e : G ≃+ H) (x : ι) : (b.map e) x = e (b x)

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

theorem FreeAddGroupBasis.injective {ι : Type u_1} {G : Type u_3} [AddGroup G] (b : FreeAddGroupBasis ι 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.

theorem FreeAddGroupBasis.isFreeAddGroup {ι : Type u_1} {G : Type u_3} [AddGroup G] (b : FreeAddGroupBasis ι G) : IsFreeAddGroup G

An additive group admitting an additive free group basis is an additive free group.

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

instance FreeAddGroupBasis.instIsFreeAddGroupFreeAddGroup (X : Type u_5) : IsFreeAddGroup (FreeAddGroup X)

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.

def FreeAddGroupBasis.lift {ι : Type u_1} {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (b : FreeAddGroupBasis ι G) : (ι → H) ≃ (G →+ H)

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

Equations

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

@[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) (x : G) : (b.lift a✝) x = (FreeGroup.lift a✝) (b.repr x)

@[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✝¹ : ι) : b.lift.symm a✝ a✝¹ = a✝ (b.repr.symm (FreeGroup.of a✝¹))

@[simp]

theorem FreeAddGroupBasis.lift_apply_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (b : FreeAddGroupBasis ι G) (a✝ : ι → H) (x : G) : (b.lift a✝) x = (FreeAddGroup.lift a✝) (b.repr x)

@[simp]

theorem FreeAddGroupBasis.lift_symm_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (b : FreeAddGroupBasis ι G) (a✝ : G →+ H) (a✝¹ : ι) : b.lift.symm a✝ a✝¹ = a✝ (b.repr.symm (FreeAddGroup.of a✝¹))

theorem FreeGroupBasis.ext_hom {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (f 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.

theorem FreeAddGroupBasis.ext_hom {ι : Type u_1} {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (b : FreeAddGroupBasis ι G) (f 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 := ((FreeGroup.lift of).toMulEquiv (lift FreeGroup.of) ⋯ ⋯).symm }

def FreeAddGroupBasis.ofLift {G : Type u} [AddGroup G] (X : Type u) (of : X → G) (lift : {H : Type u} → [inst : AddGroup H] → (X → H) ≃ (G →+ H)) (lift_of : ∀ {H : Type u} [inst : AddGroup H] (f : X → H) (a : X), (lift f) (of a) = f a) : FreeAddGroupBasis X G

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

Equations

• FreeAddGroupBasis.ofLift X of lift lift_of = { repr := ((FreeAddGroup.lift of).toAddEquiv (lift FreeAddGroup.of) ⋯ ⋯).symm }

noncomputable 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.

noncomputable def FreeAddGroupBasis.ofUniqueLift {G : Type u} [AddGroup G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [inst : AddGroup H] (f : X → H), ∃! F : G →+ H, ∀ (a : X), F (of a) = f a) : FreeAddGroupBasis X G

If an additive group satisfies the universal property of an additive free group with respect to a given type, then it admits an additive free group basis based on this type. Here the universal property is expressed as in IsFreeAddGroup.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 = ⋯.choose

def IsFreeAddGroup.Generators (G : Type u_1) [AddGroup G] [IsFreeAddGroup G] : Type u_1

A set of generators of an additive free group, chosen arbitrarily

Equations

• IsFreeAddGroup.Generators G = ⋯.choose

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

@[irreducible]

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

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

Equations

• IsFreeGroup.mulEquiv G = ⋯.some.repr.symm

noncomputable def IsFreeAddGroup.addEquiv (G : Type u_2) [AddGroup G] [IsFreeAddGroup G] : FreeAddGroup (Generators G) ≃+ G

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

Equations

• IsFreeAddGroup.addEquiv G = ⋯.some.repr.symm

theorem IsFreeAddGroup.addEquiv_def (G : Type u_2) [AddGroup G] [IsFreeAddGroup G] : addEquiv G = ⋯.some.repr.symm

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

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

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

Equations

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

noncomputable def IsFreeAddGroup.basis (G : Type u_1) [AddGroup G] [IsFreeAddGroup G] : FreeAddGroupBasis (Generators G) G

An additive free group basis of an additive free group G, over the set Generators G.

Equations

• IsFreeAddGroup.basis G = { repr := (IsFreeAddGroup.addEquiv G).symm }

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

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

Equations

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

noncomputable def IsFreeAddGroup.toFreeAddGroup (G : Type u_1) [AddGroup G] [IsFreeAddGroup G] : G ≃+ FreeAddGroup (Generators G)

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

Equations

• IsFreeAddGroup.toFreeAddGroup G = (IsFreeAddGroup.addEquiv G).symm

@[simp]

theorem IsFreeAddGroup.toFreeAddGroup_symm_apply (G : Type u_1) [AddGroup G] [IsFreeAddGroup G] (a✝ : FreeAddGroup (Generators G)) : (toFreeAddGroup G).symm a✝ = (addEquiv G) a✝

@[simp]

theorem IsFreeAddGroup.toFreeAddGroup_apply (G : Type u_1) [AddGroup G] [IsFreeAddGroup G] (a✝ : G) : (toFreeAddGroup G) a✝ = (addEquiv G).symm a✝

@[simp]

theorem IsFreeGroup.toFreeGroup_symm_apply (G : Type u_1) [Group G] [IsFreeGroup G] (a✝ : FreeGroup (Generators G)) : (toFreeGroup G).symm a✝ = (mulEquiv G) a✝

@[simp]

theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [Group G] [IsFreeGroup G] (a✝ : G) : (toFreeGroup G) a✝ = (mulEquiv G).symm a✝

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

The canonical injection of G's generators into G

Equations

• IsFreeGroup.of = (IsFreeGroup.mulEquiv G).toFun ∘ FreeGroup.of

noncomputable def IsFreeAddGroup.of {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] : Generators G → G

The canonical injection of G's generators into G

Equations

• IsFreeAddGroup.of = (IsFreeAddGroup.addEquiv G).toFun ∘ FreeAddGroup.of

noncomputable def IsFreeGroup.lift {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] : (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 = (IsFreeGroup.basis G).lift

noncomputable def IsFreeAddGroup.lift {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [AddGroup H] : (Generators G → H) ≃ (G →+ H)

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

Equations

• IsFreeAddGroup.lift = (IsFreeAddGroup.basis G).lift

@[simp]

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

@[simp]

theorem IsFreeAddGroup.lift_of {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [AddGroup H] (f : Generators G → H) (a : Generators G) : (lift f) (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 : Generators G) : lift.symm f a = f (of a)

@[simp]

theorem IsFreeAddGroup.lift_symm_apply {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (a : Generators G) : lift.symm f a = f (of a)

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

theorem IsFreeAddGroup.ext_hom {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [AddGroup H] ⦃f g : G →+ H⦄ (h : ∀ (a : Generators G), f (of a) = g (of a)) : f = g

theorem IsFreeGroup.unique_lift {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : Generators G → H) : ∃! F : G →* H, ∀ (a : Generators G), F (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 IsFreeAddGroup.unique_lift {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [AddGroup H] (f : Generators G → H) : ∃! F : G →+ H, ∀ (a : Generators G), F (of a) = f a

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

Note that since IsFreeAddGroup.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 IsFreeAddGroup.ofLift {G : Type u} [AddGroup G] (X : Type u) (of : X → G) (lift : {H : Type u} → [inst : AddGroup H] → (X → H) ≃ (G →+ H)) (lift_of : ∀ {H : Type u} [inst : AddGroup H] (f : X → H) (a : X), (lift f) (of a) = f a) : IsFreeAddGroup G

If an additive group satisfies the universal property of an additive free group with respect to a given type, then it is free. Here, the universal property is expressed as in IsFreeAddGroup.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 IsFreeAddGroup.ofUniqueLift {G : Type u} [AddGroup G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [inst : AddGroup H] (f : X → H), ∃! F : G →+ H, ∀ (a : X), F (of a) = f a) : IsFreeAddGroup G

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

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

theorem IsFreeAddGroup.ofAddEquiv {G : Type u_1} [AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [AddGroup H] (e : G ≃+ H) : IsFreeAddGroup H