Pith. sign in
def

arcMinus

definition
show as:
module
IndisputableMonolith.Foundation.LinkingVanishingHighDim
domain
Foundation
line
179 · github
papers citing
none yet

plain-language theorem explainer

The lower semicircle on $S^1$, as a continuous path from the unit interval into the circle. Anyone running Mayer–Vietoris on circle complements in high-dimensional spheres cites it as one of the two arc pieces. It is a one-line specialization of the general semicircle map at the sign $-1$.

Claim. Let $\gamma_- : [0,1] \to S^1$ be the continuous map obtained by specializing the semicircle arc construction at the sign $s=-1$ (so $s^2=1$). Its image is the closed lower semicircle $\{z\in S^1 : z_1 \le 0\}$.

background

The ambient space is the topological $n$-sphere $\mathrm{Sph},n$, the unit sphere in Euclidean space of dimension $n+1$. Here one works on $\mathrm{Sph},1$, the ordinary circle.

The module builds the high-dimensional half of the linking-vanishing argument: embedded circles in $S^D$ for $D\ge 1$, $D\ne 3$, should have $H_1$-acyclic complements once arc complements are acyclic. The circle is split into two closed semicircles that meet only at a pair of antipodal endpoints, so Mayer–Vietoris can be applied to the complements of those images.

Upstream, the general continuous semicircle map $\mathrm{arcMap}(s)$ (for any $s$ with $s^2=1$) packages the coordinate formula into a map of topological spaces $C([0,1],S^1)$. The lower arc is the instance at $s=-1$.

proof idea

One-line definitional wrapper: instantiate the general semicircle continuous map at $s=-1$, using the elementary fact $(-1)^2=1$ to discharge the side condition. Continuity is inherited from the general construction; no separate continuity argument is written here.

why it matters

This arc is one of the two pieces in the circle-complement reduction (Hatcher 2B.1, circle case). Downstream, the embedding lemma for the lower arc, the identification of its range as ${z_1\le 0}$, the intersection of upper and lower ranges (exactly the east and west points), and their union (the whole circle) all name it directly. Those range and embedding facts feed the Mayer–Vietoris argument in the theorem that, for $D\ge 1$ and $D\ne 3$, every embedded circle in $S^D$ has $H_1$-acyclic complement whenever arc complements are acyclic. In the Recognition foundation stack this is geometric scaffolding for dimension-sensitive linking vanishing, complementary to the low-dimensional linking module and ultimately tied to the $D=3$ exceptional case in the forcing chain.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.