The circle is a fantastic thing with lots and lots of properties and extra structures. It is a:
and it is one of the basic building blocks for lots of areas of mathematics, including:
The two most common definitions of the circle are:
It is the subspace of consisting of those numbers of length :
(of course, can be identified with and an equivalent formulation of this definition given; also, to emphasise the reason for the notation , can be replaced by )
It is the quotient of by the integers:
The standard equivalence of the two definitions is given by the map , .
The topological circle is a compact, connected topological space. It is a -dimensional smooth manifold (indeed, it is the only -dimensional compact, connected smooth manifold). It is not simply connected.
The circle is a model for the classifying space for the abelian group , the integers. Equivalently, the circle is the Eilenberg-Mac Lane space . Explicitly, the first homotopy group is the integers . But the higher homotopy groups , all vanish (and so is a homotopy 1-type). This can be deduced from the result that the loop space of the circle is the group of integers and that is path-connected. A proof of this in homotopy type theory is in Shulman P1S1.
The result that holds in a general Grothendieck (∞,1)-topos. In fact, more generally, for a pointed object of a Grothendieck (∞,1)-topos , there is a natural equivalence between the suspension object and the classifying space . In particular, when is specifically the 0-truncated two-point space , we get .
Generally, the -torus is .
A formalization in homotopy type theory, along with a proof that (and hence ), can be found in
The HoTT Book, section 8.1
The HoTT Coq library: theories/hit/Circle.v
The HoTT Agda library: homotopy/LoopSpaceCircle.agda