topology (point-set topology, point-free topology)



Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory

Manifolds and cobordisms



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:


We consider the circle first as a topological space, then as the homotopy type represented by that space.

As a topological space


The two most common definitions of the circle are:

  1. It is the subspace of \mathbb{C} consisting of those numbers of length 11:

    U(1){z:|z|=1} U(1) \coloneqq \{z \in \mathbb{C} : {|z|} = 1\}

    (of course, \mathbb{C} can be identified with 2\mathbb{R}^2 and an equivalent formulation of this definition given; also, to emphasise the reason for the notation U(1)U(1), \mathbb{C} can be replaced by *=GL 1()\mathbb{C}^* = GL_1(\mathbb{C}))

  2. It is the quotient of \mathbb{R} by the integers:

    S 1/ S^1 \coloneqq \mathbb{R}/\mathbb{Z}

The standard equivalence of the two definitions is given by the map \mathbb{R} \to \mathbb{C}, te 2πitt \mapsto e^{2 \pi i t}.

As a homotopy type

As a homotopy type the circle is for instance the homotopy pushout

S 1* ***. S^1 \simeq * \coprod_{* \coprod * } * \,.

In homotopy type theory, this can be formalized as a higher inductive type generated by a point base and a path from base to itself; see the references.


The topological circle is a compact, connected topological space. It is a 11-dimensional smooth manifold (indeed, it is the only 11-dimensional compact, connected smooth manifold). It is not simply connected.

The circle is a model for the classifying space for the abelian group \mathbb{Z}, the integers. Equivalently, the circle is the Eilenberg-Mac Lane space K(,1)K({\mathbb{Z}},1). Explicitly, the first homotopy group π 1(S 1)\pi_1(S^1) is the integers \mathbb{Z}. But the higher homotopy groups π n(S 1)*\pi_n(S^1) \simeq *, n>1n \gt 1 all vanish (and so is a homotopy 1-type). This can be deduced from the result that the loop space ΩS 1\Omega S^1 of the circle is the group {\mathbb{Z}} of integers and that S 1S^1 is path-connected. A proof of this in homotopy type theory is in Shulman P1S1.

The result that S 1K(,1)S^1\simeq K({\mathbb{Z}},1) holds in a general Grothendieck (∞,1)-topos. In fact, more generally, for XX a pointed object of a Grothendieck (∞,1)-topos {\mathcal{H}}, there is a natural equivalence between the suspension object ΣX\Sigma X and the classifying space BX B{\mathbb{Z}}\wedge X. In particular, when XX is specifically the 0-truncated two-point space S 0S^0, we get S 1K(,1)S^1\simeq K({\mathbb{Z}},1).

The product of the circle with itself is the (22)-torus

T=S 1×S 1. T = S^1 \times S^1 \,.

Generally, the nn-torus T nT^n is (S 1) n(S^1)^n.


A formalization in homotopy type theory, along with a proof that ΩS 1\Omega S^1\simeq {\mathbb{Z}} (and hence π 1(S 1)\pi_1(S^1) \simeq \mathbb{Z}), can be found in

The proof is formalized therein using the Agda proof assistant. See also

Last revised on May 12, 2017 at 05:57:17. See the history of this page for a list of all contributions to it.