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:

Rules for free groups

Formation rules for free groups:

Γ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))}


Every subgroup of a free group is itself a free group. This is the Nielsen-Schreier theorem.


Discussion of free groups in homotopy type theory:

Last revised on January 26, 2023 at 15:40:03. See the history of this page for a list of all contributions to it.