TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

The Fadell-Neuwirth forgetful map: local triviality, constant fibre, and numerability for configurations in the disk

Statement

Let $M$ be a nonempty connected Hausdorff topological $d$ -manifold without boundary (Topological manifolds without boundary: Hausdorff, second-countable, and locally Euclidean spaces) with $d \geq 2$ , let $m, n \geq 1$ , and let $π : F_{m + n} (M) ⟶ F_{m} (M), π (x_{1}, \dots, x_{m + n}) : = (x_{1}, \dots, x_{m})$ forget the last $n$ points (Ordered configuration spaces $F_{n} (X)$ ). Write $Q_{q^{'}} : = {q_{1}^{'}, \dots, q_{m}^{'}}$ for the underlying set of a configuration $q^{'} \in F_{m} (M)$ . Then:

Local triviality, with the fibre of the configuration. For every base configuration $q^{'}$ there are an open neighbourhood $U \subseteq F_{m} (M)$ of $q^{'}$ and a homeomorphism $U \times F_{n} (M ∖ Q_{q^{'}}) \to π^{- 1} (U)$ over $U$ , and the fibre $π^{- 1} (q^{'})$ is homeomorphic to $F_{n} (M ∖ Q_{q^{'}})$ (Forgetting the last $n$ points is locally trivial with fibre $F_{n}$ of the punctured manifold).
The fibre type is constant. For all $q^{'}, q^{''} \in F_{m} (M)$ the spaces $F_{n} (M ∖ Q_{q^{'}})$ and $F_{n} (M ∖ Q_{q^{''}})$ are homeomorphic; this uses the connectedness of $F_{m} (M)$ and no choice principle.
Fixed fibre and numerability for configurations in the disk. Fix $q \in F_{m} (M)$ and $F : = F_{n} (M ∖ Q_{q})$ . Assume the Axiom of Choice. Then there are an open cover of $F_{m} (M)$ and trivializations of $π$ over its members with the single fibre $F$ , so that $π$ is a locally trivial fibre bundle with fibre $F$ in the sense of Locally trivial fiber bundle; the Axiom of Choice is used here to select, for each base point, a trivialization carrying the fibre $F_{n} (M ∖ Q_{q^{'}})$ of part 1 onto the fixed $F$ . If moreover $M = int D^{2}$ , so that the base is a metric space, then under AC and the Axiom of Dependent Choice the displayed locally trivial bundle is numerable and, by the published numerable-bundle theorem, is a Hurewicz fibration (Hurewicz and serre fibrations).

No global metric, paracompactness, or second countability of $M$ beyond its manifold structure is used in parts 1 and 2, and the only choice principles used anywhere are the ones declared in part 3.

Facts & Assumptions

Given: A nonempty connected Hausdorff topological $d$ -manifold $M$ without boundary with $d \geq 2$ , integers $m, n \geq 1$ , the forgetful map $π : F_{m + n} (M) \to F_{m} (M)$ , and configurations $q, q^{'}, q^{''} \in F_{m} (M)$ .

[F1]

For a topological space $X$ , $F_{k} (X)$ is the space of $k$ -tuples of pairwise distinct points of $X$ with the subspace topology of $X^{k}$ , so that $F_{m} (M) \subseteq M^{m}$ carries the subspace topology (Ordered configuration spaces $F_{n} (X)$ , Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace); the projection $π$ drops the last $n$ coordinates. It is well defined on $F_{m + n} (M)$ , and for $x \in F_{m} (M)$ its fibre is $π^{- 1} (x) = {x} \times F_{n} (M ∖ {x_{1}, \dots, x_{m}})$ , since the last $n$ coordinates of a point of $F_{m + n} (M)$ must be distinct from each other and from $x_{1}, \dots, x_{m}$ .

[L2]

Local triviality. For every base configuration $q^{'} \in F_{m} (M)$ there are an open neighbourhood $U \subseteq F_{m} (M)$ of $q^{'}$ and a homeomorphism $Φ : U \times F_{n} (M ∖ Q_{q^{'}}) \to π^{- 1} (U)$ with $π \circ Φ = {pr}_{1}$ ; the restriction of $Φ$ to ${x} \times F_{n} (M ∖ Q_{q^{'}})$ is a homeomorphism onto $π^{- 1} (x)$ for each $x \in U$ , and no choice principle is used (Forgetting the last $n$ points is locally trivial with fibre $F_{n}$ of the punctured manifold, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[L3]

$M$ connected, nonempty, of dimension $d \geq 2$ , implies $F_{m} (M)$ path-connected, hence connected (Ordered configuration spaces cover the unordered ones regularly with deck group $S_{n}$ , Every path-connected space is connected, and every path component lies inside a component, Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets). A subset of a connected space that is nonempty, open and closed is the whole space, since otherwise it and its complement would be a separation; and the complement of a closed set is open (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L4]

A locally trivial fibre bundle with fibre $F$ is a continuous map $p : E \to B$ together with an open cover $(U_{i})$ of $B$ and homeomorphisms $p^{- 1} (U_{i}) \to U_{i} \times F$ over $U_{i}$ ; it is numerable when there is additionally a locally finite partition of unity $(ρ_{i})$ with closed support contained in $U_{i}$ (Locally trivial fiber bundle, Locally finite partitions of unity and subordination to an open cover). A Hurewicz fibration has the homotopy lifting property for all spaces (Hurewicz and serre fibrations).

[L5]

$C$ with $d_{C} (z, w) = ∣ z - w ∣$ is a metric space and $C = R^{2}$ as before; the formula $d (z, w) : = \max_{1 \leq k \leq m} ∣ z_{k} - w_{k} ∣$ makes $C^{m}$ a metric space whose metric topology is the product topology, because a ball of radius $r$ is the product of the balls of radius $r$ , and the restriction of a metric to a subset is a metric inducing the subspace topology, since balls in the subspace are traces of balls of the ambient space (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space, The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[L6]

Under AC and DC, every open cover of a metric space admits a locally finite partition of unity subordinate to it (Under choice and dependent choice, metric open covers admit locally finite subordinate partitions of unity); and under AC every numerable fibre bundle with its charts and support-subordinate partition is a Hurewicz fibration (Numerable fiber bundles are hurewicz fibrations). AC is the statement that every family of nonempty sets has a choice function, and DC is the dependent choice principle (The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[L7]

The closed and open unit discs are related by an explicit radial homotopy equivalence, and $int D^{2} = {z \in C : ∣ z ∣ < 1}$ , so the interior disc is a boundaryless surface (The interior-disc and closed-disc configuration spaces are homotopy equivalent, Topological manifolds without boundary: Hausdorff, second-countable, and locally Euclidean spaces).

Proof

technique · direct

1.1

Part 1 is the local-triviality lemma. Fix a base configuration $q^{'}$ . By [L2] there are an open neighbourhood $U$ of $q^{'}$ and a homeomorphism $Φ : U \times F_{n} (M ∖ Q_{q^{'}}) \to π^{- 1} (U)$ over $U$ ; for $x \in U$ the restriction of $Φ$ maps ${x} \times F_{n} (M ∖ Q_{q^{'}})$ homeomorphically onto $π^{- 1} (x)$ . Hence $π$ is locally trivial at $q^{'}$ with that fibre, which is claim 1 of the statement for this $q^{'}$ ; as $q^{'}$ was arbitrary, claim 1 holds.

F1L2

1.2

The set of configurations with fibre homeomorphic to a fixed one is open and closed. Fix $q \in F_{m} (M)$ , put $F : = F_{n} (M ∖ Q_{q})$ and $S : = {q^{'} \in F_{m} (M) : F_{n} (M ∖ Q_{q^{'}}) is homeomorphic to F}$ . Let $q^{'} \in F_{m} (M)$ and let $U$ be a neighbourhood of $q^{'}$ as in [L2]; for every $x \in U$ the fibre $π^{- 1} (x)$ is homeomorphic to $F_{n} (M ∖ Q_{q^{'}})$ by [L2] and also, by applying [L2] at the configuration $x$ , homeomorphic to $F_{n} (M ∖ Q_{x})$ ; so $F_{n} (M ∖ Q_{x})$ is homeomorphic to $F_{n} (M ∖ Q_{q^{'}})$ for every $x \in U$ . Consequently $q^{'} \in S$ implies $U \subseteq S$ , and $q^{'} \notin S$ implies $U \cap S = \emptyset$ ; that is, $S$ and its complement are open in $F_{m} (M)$ .

F1L2

1.3

The disk base is a metric space. Suppose $M = int D^{2}$ . By [L7] this is a boundaryless surface, and $F_{m} (int D^{2})$ is a subspace of $(int D^{2})^{m}$ , hence of $C^{m}$ with the product topology; by [L5] the max-metric on $C^{m}$ induces that product topology and its restriction to the subspace $F_{m} (int D^{2})$ is a metric inducing the subspace topology. So in the disk case the base of $π$ is a metric space.

F1L5L7

2.1

Claim 2. The configuration $q$ lies in $S$ , so $S \neq \emptyset$ . By step 1.2 the set $S \subseteq F_{m} (M)$ is open and closed, and by [L3] the space $F_{m} (M)$ is connected; a nonempty open and closed subset of a connected space is the whole space by [L3], so $S = F_{m} (M)$ . Hence $F_{n} (M ∖ Q_{q^{'}}) ≅ F_{n} (M ∖ Q_{q^{''}})$ for all $q^{'}, q^{''}$ , which is claim 2; no choice was used, since the argument only used the local trivializing neighbourhoods and connectedness.

step 1.2L3

3.1

Fixed fibre and the numerable data, under AC. Assume AC, fix $q \in F_{m} (M)$ and put $F : = F_{n} (M ∖ Q_{q})$ . For every base point $q^{'}$ , step 2.1 provides a homeomorphism $α_{q^{'}} : F \to F_{n} (M ∖ Q_{q^{'}})$ , and [L2] provides a trivialization $Φ_{q^{'}} : U_{q^{'}} \times F_{n} (M ∖ Q_{q^{'}}) \to π^{- 1} (U_{q^{'}})$ over an open neighbourhood $U_{q^{'}}$ of $q^{'}$ ; composing with ${id}_{U_{q^{'}}} \times α_{q^{'}}$ gives trivializations of $π$ over the open cover ${U_{q^{'}}}_{q^{'} \in F_{m} (M)}$ , all with the single fibre $F$ . The family of these trivializations has nonempty value set at each index $q^{'}$ , so AC supplies a choice of one for every $q^{'}$ ; with that choice and the open cover ${U_{q^{'}}}$ , the map $π$ is a locally trivial fibre bundle with fibre $F$ in the sense of [L4]. This is the only use of AC in the general case.

step 2.1L2L4L6

4.1

The configuration bundle in the disk is numerable, hence a Hurewicz fibration. Assume AC and DC and $M = int D^{2}$ . By step 1.3 the base is a metric space, so by [L6] the open cover of step 3.1 admits a locally finite partition of unity $(ρ_{q^{'}})$ with closed support contained in $U_{q^{'}}$ . Together with the trivializations of step 3.1 this is numerating data for $π$ in the sense of [L4], so the bundle is numerable; by the numerable-bundle theorem of [L6], which assumes AC, it is a Hurewicz fibration. DC was used only through the partition-of-unity corollary.

step 1.3step 3.1L4L6

5.1

Conclusion. Step 1.1 proves claim 1, step 2.1 proves claim 2, and steps 3.1 and 4.1 prove claim 3, including the numerable and Hurewicz conclusions for $M = int D^{2}$ under AC and DC. No structure on $M$ beyond the boundaryless manifold structure and no choice principle beyond those declared was used.

step 1.1step 2.1step 3.1step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

110 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

Edward Fadell and Lee Neuwirth, Configuration Spaces, section II Theorem 3, printed p. 113 (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, section 4.2, the Huebsch-Hurewicz paracompact-base strengthening, printed pp. 379-380 (standard reference, not scraped)