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. Its first homotopy group is the integers

π 1(S 1). \pi_1(S^1) \simeq \mathbb{Z} \,.

(A proof of this in homotopy type theory is in Shulman P1S1.)

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). The circle is a model for the classifying space for the abelian group \mathbb{Z}, the integers.

The product of the circle with itself is the torus

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

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


A formalization in homotopy type theory, along with a proof that π 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 January 6, 2014 13:07:28 by Urs Schreiber (