TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Evaluation boundary isomorphism for the disk

Statement

Assume the Axiom of Choice. Let $D^{2} \subseteq R^{2}$ be the closed unit disc with the base configuration $Q_{n} = (q_{1}, \dots, q_{n})$ of Boundary-fixed mapping class group of a punctured disk, let

$E : = {Homeo}^{+} (D^{2}, \partial D^{2}), B : = C_{n} (int D^{2}), F : = {Homeo}^{+} (D^{2}, \partial D^{2}; Q_{n}),$

and let $δ : π_{1} (B, [Q_{n}]) \to Mod (D^{2}, Q_{n}; \partial D^{2}) = π_{0} (F)$ be the inverse-endpoint boundary map of Boundary map from point motions. Then $δ$ is an isomorphism of groups for every $n \geq 0$ .

Facts & Assumptions

Given: The Axiom of Choice, the evaluation map $ev : E \to B$ of Evaluation is a numerable bundle and Hurewicz fibration, the fibre $F = {ev}^{- 1} ([Q_{n}])$ over the basepoint, and the boundary map $δ$ of Boundary map from point motions.

[L1]

$ev$ is a Hurewicz fibration with fibre $F$ over $[Q_{n}]$ (Evaluation is a numerable bundle and Hurewicz fibration).

[L2]

The boundary map $δ$ is a well-defined group homomorphism from $π_{1} (B, [Q_{n}])$ to $Mod (D^{2}, Q_{n}; \partial D^{2}) = π_{0} (F)$ , and it is the connecting map of the fibration exact sequence in the library's convention (Point-motion boundary map is a homomorphism, Boundary map from point motions).

[L3]

$E = {Homeo}^{+} (D^{2}, \partial D^{2})$ is contractible in the compact-open topology (Alexander contraction of the boundary-fixed disk homeomorphism group).

[L4]

A contractible space is path-connected (Every nonempty contractible space is path-connected) and has trivial fundamental group at every basepoint (A contractible space has trivial fundamental group).

[L5]

For the based fibration $ev : E \to B$ with fibre $F$ , the sequence $\dots \to π_{1} (E) \overset{{ev}_{*}}{\to} π_{1} (B) \overset{δ}{\to} π_{0} (F) \overset{i_{*}}{\to} π_{0} (E) \overset{}{\to} π_{0} (B)$ is exact wherever there is an incoming and outgoing arrow, with $π_{0}$ a pointed set and $π_{1}$ groups; exactness means incoming image equals the inverse image of the distinguished element (Long exact sequence of homotopy groups of a fibration).

[L6]

$π_{0} (F) = Mod (D^{2}, Q_{n}; \partial D^{2})$ is a group and $π_{1} (B, [Q_{n}])$ is a group, both with multiplication on classes (Boundary-fixed mapping class group of a punctured disk).

[L7]

A group isomorphism is a bijective group homomorphism (Group isomorphisms, automorphisms and the set $Aut (G)$ ).

Proof

technique · direct

1.1L3L4

The two low-degree terms of the total space are trivial. By [L3] the space $E$ is contractible, so by [L4] it is path-connected, that is $π_{0} (E)$ is a one-point set and the induced map $π_{0} (F) \to π_{0} (E)$ is constant; and $π_{1} (E, id) = {1}$ is the trivial group. Both statements hold for every $n \geq 0$ because neither depends on the number of marked points.

1.2L2L6

The boundary map is a group homomorphism. By [L2], $δ$ is a well-defined map $π_{1} (B, [Q_{n}]) \to π_{0} (F)$ preserving the products of [L6]; that is, $δ$ is a group homomorphism and the two displayed groups are the ones from the fibration exact sequence.

2.1L1L2L5step 1.1

Injectivity. The map $ev$ is a Hurewicz fibration with fibre $F$ over the basepoint by [L1], so the exact sequence [L5] applies to it; exactness at $π_{1} (B)$ says that the kernel of $δ$ equals the image of ${ev}_{*} : π_{1} (E, id) \to π_{1} (B, [Q_{n}])$ . By step 1.1 the group $π_{1} (E, id)$ is trivial, so its image is the trivial subgroup, and the kernel of $δ$ is trivial: distinct classes in $π_{1} (B, [Q_{n}])$ have distinct images in $π_{0} (F)$ .

2.2L1L5step 1.1

Surjectivity. The exact sequence [L5] applies to $ev$ by the fibration statement [L1]; exactness at $π_{0} (F)$ says that the image of $δ$ equals the kernel of $i_{*} : π_{0} (F) \to π_{0} (E)$ , the kernel of a map of pointed sets being the preimage of the distinguished component. By step 1.1 the set $π_{0} (E)$ is a single point, so every element of $π_{0} (F)$ is sent to the unique component of $E$ and the kernel of $i_{*}$ is all of $π_{0} (F)$ . Hence every element of $π_{0} (F) = Mod (D^{2}, Q_{n}; \partial D^{2})$ is the image under $δ$ of some class in $π_{1} (B, [Q_{n}])$ .

3.1L2L5L7step 1.1step 1.2step 2.1step 2.2∎

The isomorphism and the elementary cases. By steps 1.2 and 2.1 the homomorphism $δ$ is injective, and by step 2.2 it is surjective; a bijective group homomorphism is an isomorphism by [L7], which proves the claim for every $n \geq 0$ . The case $n = 0$ is included in this argument: $B = C_{0} (int D^{2})$ is a one-point space, $F = E$ , the evaluation fibration is the constant projection $E \to {[Q_{0}]}$ of the contractible space $E$ , and both $π_{1} (B, [Q_{0}])$ and $π_{0} (F)$ are trivial, as the steps above give; for $n = 1$ only the collision condition disappears from $B$ and the argument is unchanged.

Remarks

Both sides of $δ$ are computed at the same basepoint $[Q_{n}]$ , and no connecting path between basepoints is chosen; this is why the result needs only the stated Axiom of Choice, which enters through the numerable-bundle route to fibration lifting, not through a basepoint change.
The value of $δ$ is the inverse of the lifted endpoint; with this convention $δ$ is the connecting map $\partial_{p} [γ] = [e_{0}] \cdot [γ]^{- 1}$ of the published exact sequence, and the isomorphism of the theorem is the identification of the two.

Depends on

Used by

Dependency tree · two levels

35 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

Joan S. Birman and Tara E. Brendle, Braids: A Survey, section 1.3 and the proof of Theorem 1, author manuscript pp. 5-7 (standard reference, not scraped)
Brayton Gray, Homotopy Theory: An Introduction to Algebraic Topology, Chapter 8 on fibre spaces and exact sequences (standard reference, not scraped)