nLab
circle

Idea

The circle is a fantastic thing with lots and lots of properties and extra structures. It is a:

• topological space
• smooth manifold
• Lie group (the circle group)
• co-H-group?

and it is one of the basic building blocks for lots of areas of mathematics, including:

• homotopy theory
• loop spaces
• knots and links

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 $ℂ$ consisting of those numbers of length $1$:

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

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

2. It is the quotient of $ℝ$ by the integers:

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

The standard equivalence of the two definitions is given by the map $ℝ\to ℂ$, $t\mapsto e^{2\pi it}$.

As a homotopy type

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

$$S^1\simeq *\coprod _{*\coprod *}*.$$S^1 \simeq * \coprod_{* \coprod * } * \,.

A formalization as a higher inductive type in homotopy type theory is given by

Axiom circle : Type.

Axiom base : circle.
Axiom loop : base ~~> base.

See (Shulman).

Properties

The 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}.$$\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>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.$$T = S^1 \times S^1 \,.

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

Related concepts

• sphere

• pseudocircle

References

A formalization in homotopy type theory is in

• Mike Shulman, Circle.v

The proof that ${\pi }_1(S^1)\simeq \mathbb{Z}$ in this context is in

• Mike Shulman, P1S1.v