nLab circle

Context

Topology

topology

algebraic topology

Examples

Manifolds and cobordisms

manifolds and cobordisms

Contents

Idea

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:

Definition

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

As a topological space

Definition

The two most common definitions of the circle are:

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

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

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

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

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

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

As a homotopy type

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

$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.

Properties

The topological circle is a compact, connected topological space. It is a $1$-dimensional smooth manifold (indeed, it is the only $1$-dimensional compact, connected smooth manifold). It is not simply connected. Its first homotopy group is the integers

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

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

But the higher homotopy groups $\pi_n(S^1) \simeq *$, $n \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 \times S^1 \,.$

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

References

A formalization in homotopy type theory, along with a proof that $\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 (89.204.137.111)