Contents

# 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 as a topological space are:

1. It is the topological subspace of $\mathbb{C}$ consisting of those numbers of norm/absolute value $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 the bare homotopy type, the shape $ʃ S^1 \simeq \mathbf{B}\mathbb{Z}$ of the cohesive circle $S^1$ is equivalent to 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 circle type for more.

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

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({\mathbb{Z}},1)$. Explicitly, the first homotopy group $\pi_1(S^1)$ is the integers $\mathbb{Z}$. But the higher homotopy groups $\pi_n(S^1) \simeq *$, $n \gt 1$ all vanish (and so is a homotopy 1-type). This can be deduced from the result that the loop space $\Omega S^1$ of the circle is the group ${\mathbb{Z}}$ of integers and that $S^1$ is path-connected. A proof of this in homotopy type theory is in Shulman P1S1.

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

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

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

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

A formalization of the shape homotopy type $ʃ S^1 \simeq \mathbf{B}\mathbb{Z}$ of the circle as a higher inductive type in homotopy type theory, along with a proof that $\Omega ʃS^1\simeq {\mathbb{Z}}$ (and hence $\pi_1(ʃS^1) \simeq \mathbb{Z}$):

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