circle in nLab
Context
Topology
topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
-
fiber space, space attachment
Extra stuff, structure, properties
-
Kolmogorov space, Hausdorff space, regular space, normal space
-
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
-
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
-
open subspaces of compact Hausdorff spaces are locally compact
-
compact spaces equivalently have converging subnet of every net
-
continuous metric space valued function on compact metric space is uniformly continuous
-
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
-
injective proper maps to locally compact spaces are equivalently the closed embeddings
-
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
Manifolds and cobordisms
manifolds and cobordisms
cobordism theory, Introduction
Definitions
Genera and invariants
Classification
Theorems
Contents
Idea
The circle (the 1-dimension sphere) is a fantastic thing with lots and lots of properties and extra structures. It is a:
-
Lie group (the circle group)
-
co-H-group?
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:
-
It is the topological subspace of ℂ\mathbb{C} consisting of those numbers of norm/absolute value 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}))
-
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}, t↦e 2πitt \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≃Bℤʃ S^1 \simeq \mathbf{B}\mathbb{Z} of the cohesive circle S 1S^1 is equivalent to 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 circle type for more.
Properties
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.
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(ℤ,1)K({\mathbb{Z}},1). Explicitly, the first homotopy group π 1(S 1)\pi_1(S^1) is the integers ℤ\mathbb{Z}. 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). This can be deduced from the result that the loop space ΩS 1\Omega S^1 of the circle is the group ℤ{\mathbb{Z}} of integers and that S 1S^1 is path-connected. Proofs of this in homotopy type theory are in the references.
The result that S 1≃K(ℤ,1)S^1\simeq K({\mathbb{Z}},1) holds in a general Grothendieck (∞,1)-topos. In fact, more generally, for XX a pointed object of a Grothendieck (∞,1)-topos ℋ{\mathcal{H}}, there is a natural equivalence between the suspension object ΣX\Sigma X and the classifying space Bℤ∧X B{\mathbb{Z}}\wedge X. In particular, when XX is specifically the 0-truncated two-point space S 0S^0, we get S 1≃K(ℤ,1)S^1\simeq K({\mathbb{Z}},1).
The product of the circle with itself is the (22)-torus
T=S 1×S 1. T = S^1 \times S^1 \,.
Generally, the nn-torus T nT^n is (S 1) n(S^1)^n.
References
A formalization of the shape homotopy type ʃS 1≃Bℤʃ S^1 \simeq \mathbf{B}\mathbb{Z} of the circle as a higher inductive type in homotopy type theory, along with a proof that ΩʃS 1≃ℤ\Omega ʃS^1\simeq {\mathbb{Z}} (and hence π 1(ʃS 1)≃ℤ\pi_1(ʃS^1) \simeq \mathbb{Z}):
-
Dan Licata, Mike Shulman, Calculating the Fundamental Group of the Circle in Homotopy Type Theory, LICS ‘13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science June 2013 (arXiv:1301.3443, doi:10.1109/LICS.2013.28)
blog announcement: A formal proof that π 1(S 1)=ℤ\pi_1(S^1) = \mathbb{Z}
-
Marc Bezem, Ulrik Buchholtz, Daniel Grayson, Michael Shulman, Construction of the Circle in UniMath, Journal of Pure and Applied Algebra Volume 225, Issue 10, October 2021, 106687 (arXiv:1910.01856)
The proof is formalized therein using the Agda proof assistant. See also
-
The HoTT Book, section 8.1
-
The HoTT Coq library: theories/Spaces/Circle.v, theories/Homotopy/Pi1S1.v
-
The HoTT Agda library: homotopy/LoopSpaceCircle.agda
Last revised on January 31, 2025 at 08:52:28. See the history of this page for a list of all contributions to it.