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

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


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

Revised on May 12, 2017 05:57:17 by Urs Schreiber (