nLab
free group
Contents
Context
Group Theory
group theory
Classical groups
Finite groups
Group schemes
Topological groups
Lie groups
Super-Lie groups
Higher groups
Cohomology and Extensions
Contents
Idea
The free group on a given set is the free object on in the category of groups. The elements of are called the generators of this group.
Definition
In type theory
In dependent type theory, the free group on a type is the 0-truncation of the underlying type of free infinity-group of , . 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 is the free group of .
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:
Introduction rules for free groups:
Properties
Every subgroup of a free group is itself a free group. This is the Nielsen-Schreier theorem.
References
Discussion of free groups in homotopy type theory:
-
Univalent Foundations Project, §6.11 of: Homotopy Type Theory – Univalent Foundations of Mathematics, Institute for Advanced Study (2013) [web, pdf]
-
Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson: §6.2 in: Symmetry (2021) [pdf]
-
Nicolai Kraus, Thorsten Altenkirch, Free Higher Groups in Homotopy Type Theory, LICS ‘18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (2018) [arXiv;1805.02069, doi:10.1145/3209108.3209183]
Last revised on January 26, 2023 at 15:40:03.
See the history of this page for a list of all contributions to it.