Alphabeta Math
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≥2, let m,n≥1, and let π:Fm+n(M)⟶Fm(M),π(x1,…,xm+n):=(x1,…,xm) forget the last n points (Ordered configuration spaces Fn(X)). Write Qq′:={q1′,…,qm′} for the underlying set of a configuration q′∈Fm(M). Then:

  1. Local triviality, with the fibre of the configuration. For every base configuration q′ there are an open neighbourhood U⊆Fm(M) of q′ and a homeomorphism U×Fn(M∖Qq′)→π−1(U) over U, and the fibre π−1(q′) is homeomorphic to Fn(M∖Qq′) (Forgetting the last n points is locally trivial with fibre Fn of the punctured manifold).
  2. The fibre type is constant. For all q′,q′′∈Fm(M) the spaces Fn(M∖Qq′) and Fn(M∖Qq′′) are homeomorphic; this uses the connectedness of Fm(M) and no choice principle.
  3. Fixed fibre and numerability for configurations in the disk. Fix q∈Fm(M) and F:=Fn(M∖Qq). Assume the Axiom of Choice. Then there are an open cover of Fm(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 Fn(M∖Qq′) of part 1 onto the fixed F. If moreover M=int⁡D2, 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≥2, integers m,n≥1, the forgetful map π:Fm+n(M)→Fm(M), and configurations q,q′,q′′∈Fm(M).

[F1]

For a topological space X, Fk(X) is the space of k-tuples of pairwise distinct points of X with the subspace topology of Xk, so that Fm(M)⊆Mm carries the subspace topology (Ordered configuration spaces Fn(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 Fm+n(M), and for x∈Fm(M) its fibre is π−1(x)={x}×Fn(M∖{x1,…,xm}), since the last n coordinates of a point of Fm+n(M) must be distinct from each other and from x1,…,xm.

[L2]

Local triviality. For every base configuration q′∈Fm(M) there are an open neighbourhood U⊆Fm(M) of q′ and a homeomorphism Φ:U×Fn(M∖Qq′)→π−1(U) with π∘Φ=pr⁡1; the restriction of Φ to {x}×Fn(M∖Qq′) is a homeomorphism onto π−1(x) for each x∈U, and no choice principle is used (Forgetting the last n points is locally trivial with fibre Fn of the punctured manifold, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, The product set ∏i∈IXi 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≥2, implies Fm(M) path-connected, hence connected (Ordered configuration spaces cover the unordered ones regularly with deck group Sn, 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→B together with an open cover (Ui) of B and homeomorphisms p−1(Ui)→Ui×F over Ui; it is numerable when there is additionally a locally finite partition of unity (ρi) with closed support contained in Ui (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).

[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⁡D2={z∈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.1F1L2

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×Fn(M∖Qq′)→π−1(U) over U; for x∈U the restriction of Φ maps {x}×Fn(M∖Qq′) 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.

1.2F1L2

The set of configurations with fibre homeomorphic to a fixed one is open and closed. Fix q∈Fm(M), put F:=Fn(M∖Qq) and S:={q′∈Fm(M):Fn(M∖Qq′) is homeomorphic to F}. Let q′∈Fm(M) and let U be a neighbourhood of q′ as in [L2]; for every x∈U the fibre π−1(x) is homeomorphic to Fn(M∖Qq′) by [L2] and also, by applying [L2] at the configuration x, homeomorphic to Fn(M∖Qx); so Fn(M∖Qx) is homeomorphic to Fn(M∖Qq′) for every x∈U. Consequently q′∈S implies U⊆S, and q′∉S implies U∩S=∅; that is, S and its complement are open in Fm(M).

1.3F1L5L7

The disk base is a metric space. Suppose M=int⁡D2. By [L7] this is a boundaryless surface, and Fm(int⁡D2) is a subspace of (int⁡D2)m, hence of Cm with the product topology; by [L5] the max-metric on Cm induces that product topology and its restriction to the subspace Fm(int⁡D2) is a metric inducing the subspace topology. So in the disk case the base of π is a metric space.

2.1step 1.2L3

Claim 2. The configuration q lies in S, so S≠∅. By step 1.2 the set S⊆Fm(M) is open and closed, and by [L3] the space Fm(M) is connected; a nonempty open and closed subset of a connected space is the whole space by [L3], so S=Fm(M). Hence Fn(M∖Qq′)≅Fn(M∖Qq′′) for all q′,q′′, which is claim 2; no choice was used, since the argument only used the local trivializing neighbourhoods and connectedness.

3.1step 2.1L2L4L6

Fixed fibre and the numerable data, under AC. Assume AC, fix q∈Fm(M) and put F:=Fn(M∖Qq). For every base point q′, step 2.1 provides a homeomorphism αq′:F→Fn(M∖Qq′), and [L2] provides a trivialization Φq′:Uq′×Fn(M∖Qq′)→π−1(Uq′) over an open neighbourhood Uq′ of q′; composing with id⁡Uq′×αq′ gives trivializations of π over the open cover {Uq′}q′∈Fm(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 {Uq′}, 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.

4.1step 1.3step 3.1L4L6

The configuration bundle in the disk is numerable, hence a Hurewicz fibration. Assume AC and DC and M=int⁡D2. 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 Uq′. 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.

5.1step 1.1step 2.1step 3.1step 4.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⁡D2 under AC and DC. No structure on M beyond the boundaryless manifold structure and no choice principle beyond those declared was used.

Depends on

Used by

Dependency tree · two levels

116 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