Wc
plain-language theorem explainer
The doubly punctured circle is the unit circle with north and south poles removed, packaged as a topological space. It is the ambient space for the two-arc cover used in the singular-sphere homology calculation. The definition is the intersection of the two standard open charts on S¹, promoted to TopCat.
Claim. Let $S^1$ be the unit circle in $\mathbb{R}^2$. Write $U = S^1 \setminus \{\text{south pole}\}$ and $V = S^1 \setminus \{\text{north pole}\}$. The doubly punctured circle is the topological space $W_c := U \cap V = S^1 \setminus \{\text{north},\text{south}\}$.
background
In this module the $n$-sphere Sph n is the unit sphere in Euclidean space of dimension $n+1$, viewed as an object of TopCat. The two standard charts are the sphere minus the south pole and the sphere minus the north pole; their union recovers the whole sphere.
For $n=1$ those charts are open arcs covering $S^1$. Their intersection is $S^1$ with both poles deleted: a circle with two punctures, homeomorphic to two open intervals (the east and west semicircles). That intersection is the space named here.
The construction sits in the singular-sphere geometry layer that feeds Čech/singular $H_0$ computations distinguishing the two arcs.
proof idea
Definitional abbreviation only: form the set-theoretic intersection of the two charts on the 1-sphere, cast as a subtype of the sphere, and wrap it with TopCat.of to obtain a topological space object. No proof obligations.
why it matters
This space is the carrier for the two-point difference class in $H_0$ and for the east-arc augmentation that pairs to $1$ against it. Downstream definitions place the east and west points in the intersection, the real coordinate along the ambient $x$-axis, the right arc ${w : x(w)>0}$, and the difference class ptH(a)-ptH(b). The pairing lemma then shows that class is nonzero in $H_0(W_c)$ while dying in the direct sum of the chart homologies, which is the local algebraic content of the singular-sphere argument.
In the broader Recognition stack this is pure topological scaffolding for the foundation geometry, not a forcing-chain step (T0–T8) or a physical constant identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.