CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Unordered planar configuration spaces are aspherical

Statement

Assume the Axiom of Choice. For every $n \geq 1$ , every $k \geq 2$ and every basepoint $b \in C_{n} (int D^{2})$ one has $π_{k} (C_{n} (int D^{2}), b) = 0.$ The same conclusion holds for the unordered configuration spaces $C_{n} (C)$ and $C_{n} (D^{2})$ under the coordinatewise radial homeomorphism and the published unordered inclusion homotopy equivalence. Consequently the open-disc and plane unordered configuration spaces are $K (B_{n}^{c o n f}, 1)$ in the higher-homotopy sense: their fundamental group is $B_{n}^{c o n f}$ in the convention of The configuration braid group $B_{n}^{c o n f}$ as the fundamental group of an unordered configuration space and all higher homotopy groups vanish.

Facts & Assumptions

Given: the Axiom of Choice, an integer $n \geq 1$ , a basepoint $b \in C_{n} (int D^{2})$ with a chosen preimage $x \in F_{n} (int D^{2})$ , and a degree $k \geq 2$ .

[A1]

The Axiom of Choice holds (The Axiom of Choice).

[F1]

For every $m \geq 1$ , every $j \geq 2$ and every base configuration $c \in F_{m} (int D^{2})$ one has $π_{j} (F_{m} (int D^{2}), c) = 0$ (Ordered planar configuration spaces are aspherical).

[F2]

For the surface $M = int D^{2}$ the quotient map $p : F_{n} (M) \to C_{n} (M)$ is an $n!$ -sheeted covering map, both $F_{n} (M)$ and $C_{n} (M)$ are path-connected, and $p$ is regular; no choice principle is used (Ordered configuration spaces cover the unordered ones regularly with deck group $S_{n}$ ).

[F3]

Let $Y$ be path-connected and locally path-connected and let $f : (Y, y_{0}) \to (B, b_{0})$ be based, with $p : (E, e_{0}) \to (B, b_{0})$ a covering; a based lift of $f$ exists if and only if $f_{*} π_{1} (Y, y_{0}) \subseteq p_{*} π_{1} (E, e_{0})$ (Lifting criterion for maps from path-connected locally path-connected spaces).

[F4]

Let $p : E \to B$ be a covering, $H : Y \times I \to B$ a homotopy and ${\tilde{H}}_{0} : Y \to E$ a lift of $H (-, 0)$ ; there is a unique lift $\tilde{H} : Y \times I \to E$ extending ${\tilde{H}}_{0}$ (Existence and uniqueness of homotopy lifts through a covering map).

[F5]

For every $k \geq 2$ the sphere $S^{k}$ is simply connected, hence path-connected and locally path-connected ( $S^{n}$ is simply connected for every $n \geq 2$ , Cubical and spherical models of higher homotopy agree).

[F6]

The unordered inclusion $ι^{C} : C_{n} (int D^{2}) \to C_{n} (D^{2})$ is a homotopy equivalence, the coordinatewise radial map restricts to a homeomorphism $C_{n} (C) \to C_{n} (int D^{2})$ , and homotopy equivalences induce isomorphisms on all homotopy groups in degrees $\geq 1$ (The interior-disc and closed-disc configuration spaces are homotopy equivalent, Higher homotopy groups are functorial and based homotopy invariant).

[F7]

$B_{n}^{c o n f} = π_{1} (C_{n} (D^{2}), [q])$ for the orbit of a base configuration of interior points, and the inclusion of the open-disc model induces an isomorphism $π_{1} (C_{n} (int D^{2}), [q]) \to B_{n}^{c o n f}$ (The configuration braid group $B_{n}^{c o n f}$ as the fundamental group of an unordered configuration space).

Proof

technique · direct

1.1A1F1

Ordered vanishing. Under the standing assumption [A1], which discharges the Axiom-of-Choice hypothesis of [F1], the ordered result applies: for the chosen preimage $x \in F_{n} (int D^{2})$ of $b$ one has $π_{k} (F_{n} (int D^{2}), x) = 0$ for the degree $k \geq 2$ ; that is, every based map $S^{k} \to F_{n} (int D^{2})$ at $x$ is based-homotopic to the constant map.

1.2F2F3F4F5

Covering and lifting tools. By [F2] the quotient $p : F_{n} (int D^{2}) \to C_{n} (int D^{2})$ is a covering with both spaces path-connected; by [F5] the sphere $S^{k}$ is path-connected, locally path-connected and simply connected with $π_{1} (S^{k}, s_{0}) = 1$ for $k \geq 2$ ; the based lifting criterion [F3] and the homotopy lifting theorem [F4] are therefore available for based maps out of $(S^{k}, s_{0})$ .

1.3F6

Transferring along the disc models. The coordinatewise radial map gives homeomorphisms $C_{n} (C) ≅ C_{n} (int D^{2})$ , and the unordered inclusion $ι^{C} : C_{n} (int D^{2}) \to C_{n} (D^{2})$ is a homotopy equivalence; by [F6] both induce isomorphisms on $π_{j}$ for every $j \geq 1$ , so vanishing of $π_{k}$ transfers between the three models at corresponding basepoints.

2.1step 1.2F3

Lifting a based sphere. Let $u : (S^{k}, s_{0}) \to (C_{n} (int D^{2}), b)$ be a based map. Its induced map on $π_{1}$ is trivial because $π_{1} (S^{k}, s_{0}) = 1$ by step 1.2, so $u_{*} π_{1} (S^{k}, s_{0}) = {1} \subseteq p_{*} π_{1} (F_{n} (int D^{2}), x)$ and the lifting criterion [F3] provides a based lift $\tilde{u} : (S^{k}, s_{0}) \to (F_{n} (int D^{2}), x)$ with $p \circ \tilde{u} = u$ .

3.1step 1.1step 2.1F4

Nullhomotoping the lift and projecting. By step 1.1 the based class $[\tilde{u}] \in π_{k} (F_{n} (int D^{2}), x)$ is trivial, so there is a based homotopy $\tilde{H} : S^{k} \times I \to F_{n} (int D^{2})$ from $\tilde{u}$ to the constant map at $x$ with $\tilde{H} (s_{0}, t) = x$ for all $t$ . Then $p \circ \tilde{H} : S^{k} \times I \to C_{n} (int D^{2})$ is a based homotopy from $u = p \circ \tilde{u}$ to the constant map at $b$ , because $p (x) = b$ ; hence $u$ is nullhomotopic as a based map, and $[u] = 0$ in $π_{k} (C_{n} (int D^{2}), b)$ .

4.1step 3.1

Vanishing for the unordered open-disc model. Since $u$ was an arbitrary based map out of $(S^{k}, s_{0})$ with arbitrary basepoint $b$ and arbitrary $k \geq 2$ , step 3.1 shows that every based class in $π_{k} (C_{n} (int D^{2}), b)$ is trivial, so $π_{k} (C_{n} (int D^{2}), b) = 0$ .

5.1step 1.3step 4.1F7

The other models and the $K (B_{n}^{c o n f}, 1)$ reading. By step 1.3 the vanishing of step 4.1 transfers to $π_{k} (C_{n} (C), b^{'})$ and $π_{k} (C_{n} (D^{2}), b^{''})$ for arbitrary basepoints, and [F7] identifies the fundamental groups of the open-disc and plane models with $B_{n}^{c o n f}$ ; hence these spaces have fundamental group $B_{n}^{c o n f}$ and vanishing higher homotopy groups, that is, they are $K (B_{n}^{c o n f}, 1)$ in the higher-homotopy sense.

The proof lifts sphere classes to the ordered configuration space, where they vanish by ordered asphericity, and projects the nullhomotopy; the covering is used through its lifting properties only, and the case $k = 2$ of the ordered input was proved without point pushing. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Juan Gonzalez-Meneses, Basic results on braid groups, section 2.1, printed pp. 11-14 (Theorem 2.2: the unordered configuration space is a K(pi,1)) (standard reference, not scraped)
Edward Fadell and Lee Neuwirth, Configuration Spaces, section III, printed pp. 114-115 (standard reference, not scraped)