nLab free group




The free group on a given set SS is the free object on SS in the category of groups. The elements of SS are called the generators of this group.


In type theory

In dependent type theory, the free group on a type AA is the 0-truncation of the underlying type of free infinity-group of AA, FreeGroup(A)[UTFIG(A)] 0\mathrm{FreeGroup}(A) \coloneqq [\mathrm{UTFIG}(A)]_0. This is because in any dependent type theory with uniqueness of identity proofs, where every type is 0-truncated, the underlying type of the free infinity-group of AA is the free group of AA.

In addition, one could construct the free group directly from the traditional axioms of a group, as detailed below:

The inference rules for free group types:

ΓAtypeΓFreeGroup(A)type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{FreeGroup}(A) \; \mathrm{type}}

Introduction rules for free groups:

ΓAtypeΓη:AFreeGroup(A)typeΓAtypeΓμ:FreeGroup(A)×FreeGroup(A)FreeGroup(A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \eta:A \to \mathrm{FreeGroup}(A) \; \mathrm{type}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mu:\mathrm{FreeGroup}(A) \times \mathrm{FreeGroup}(A) \to \mathrm{FreeGroup}(A)}
ΓAtypeΓϵ:FreeGroup(A)ΓAtypeΓι:FreeGroup(A)FreeGroup(A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \epsilon:\mathrm{FreeGroup}(A)} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \iota:\mathrm{FreeGroup}(A) \to \mathrm{FreeGroup}(A)}
ΓAtypeΓx:FreeGroup(A)Γy:FreeGroup(A)Γz:FreeGroup(A)Γα(x,y,z):Id FreeGroup(A)(μ(x,μ(y,z)),μ(μ(x,y),z))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:\mathrm{FreeGroup}(A) \quad \Gamma \vdash y:\mathrm{FreeGroup}(A) \quad \Gamma \vdash z:\mathrm{FreeGroup}(A)}{\Gamma \vdash \alpha(x, y, z):\mathrm{Id}_{\mathrm{FreeGroup}(A)}(\mu(x, \mu(y, z)),\mu(\mu(x, y), z))}
ΓAtypeΓx:FreeGroup(A)Γλ ϵ(x):Id FreeGroup(A)(μ(ϵ,x),x)ΓAtypeΓx:FreeGroup(A)Γρ ϵ(x):Id FreeGroup(A)(μ(x,ϵ),x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:\mathrm{FreeGroup}(A)}{\Gamma \vdash \lambda_\epsilon(x):\mathrm{Id}_{\mathrm{FreeGroup}(A)}(\mu(\epsilon, x), x)} \quad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:\mathrm{FreeGroup}(A)}{\Gamma \vdash \rho_\epsilon(x):\mathrm{Id}_{\mathrm{FreeGroup}(A)}(\mu(x, \epsilon), x)}
ΓAtypeΓx:FreeGroup(A)Γλ ι(x):Id FreeGroup(A)μ(ι(x),x),ϵ)ΓAtypeΓx:FreeGroup(A)Γρ ι(x):Id FreeGroup(A)(μ(x,ι(x)),ϵ)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:\mathrm{FreeGroup}(A)}{\Gamma \vdash \lambda_\iota(x):\mathrm{Id}_{\mathrm{FreeGroup}(A)}\mu(\iota(x), x), \epsilon)} \quad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:\mathrm{FreeGroup}(A)}{\Gamma\vdash \rho_\iota(x):\mathrm{Id}_{\mathrm{FreeGroup}(A)}(\mu(x, \iota(x)), \epsilon)}
ΓAtypeΓτ:isSet(FreeGroup(A))\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \tau:\mathrm{isSet}(\mathrm{FreeGroup}(A))}



Early discussion of (subgroups of) free groups (proof of the Nielsen-Schreier theorem) and generalization to the amalgamated free product of groups:

Expository review:

  • Abhay Chandel, Free groups and amalgamated product, BSc thesis (2013) [pdf, pdf]

Discussion of free groups in homotopy type theory:

Last revised on May 6, 2023 at 12:34:14. See the history of this page for a list of all contributions to it.