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

In constructive mathematics, the notions of real numbers and complex numbers split into multiple notions. In general, if the metric space of the real numbers is not sequentially Cauchy complete, such as in the modulated Cantor real numbers, then the two definitions cannot be proven to be equivalent, since the exponential function is not well defined on $\mathbb{C}$. Only if the real numbers are sequentially Cauchy complete are the two definitions the same.

### 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. Proofs of this in homotopy type theory are in the references.

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

## References

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

Last revised on November 22, 2023 at 20:04:47. See the history of this page for a list of all contributions to it.