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 isomorphim 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

ink

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

• The generators of a free group.

  Generators : Type u

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

  MulEquiv' : FreeGroup Generators ≃* G

IsFreeGroup G means that G isomorphic to a free group.

ink

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

Equations

• instIsFreeGroupFreeGroupInstGroupFreeGroup X = { Generators := X, MulEquiv' := MulEquiv.refl (FreeGroup X) }

ink

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

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

Equations

• IsFreeGroup.MulEquiv G = IsFreeGroup.MulEquiv'

ink

@[simp]

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

ink

@[simp]

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

ink

def IsFreeGroup.toFreeGroup (G : Type u_1) [inst : Group G] [inst : 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)

ink

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

The canonical injection of G's generators into G

Equations

• IsFreeGroup.of = (IsFreeGroup.MulEquiv G).toEquiv.toFun ∘ FreeGroup.of

ink

@[simp]

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

ink

def IsFreeGroup.lift {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : 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

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

theorem IsFreeGroup.unique_lift {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : 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 functions 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.

ink

def IsFreeGroup.ofLift {G : Type u} [inst : 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.

Equations

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

ink

noncomputable def IsFreeGroup.ofUniqueLift {G : Type u} [inst : 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.

Equations

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

ink

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

Being a free group transports across group isomorphisms.

Equations

• IsFreeGroup.ofMulEquiv h = { Generators := IsFreeGroup.Generators G, MulEquiv' := MulEquiv.trans (IsFreeGroup.MulEquiv G) h }