PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-14

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 based loop space of BG recovers G weakly

Statement

Assume AC. For a well-pointed topological group $G$ of CW type, path lifting in Milnor's bundle gives a continuous based endpoint-label map

$ε : Ω B G ⟶ G .$

Put $δ = inv \circ ε$ . Under the canonical identification $π_{k} (Ω B G) ≅ π_{k + 1} (B G)$ , the maps induced by $δ$ are the connecting homomorphisms of Milnor's bundle; on components they give its connecting pointed-set map. Both $ε$ and $δ$ are weak homotopy equivalences. If $G$ and $Ω B G$ have CW type, they are based homotopy equivalences. Thus a chosen homotopy inverse $G \to Ω B G$ exists under those stronger hypotheses. No point-set connecting map independent of the chosen lifting function is asserted.

Facts & Assumptions

[F1]

Milnor's $E G \to B G$ is a numerable principal bundle and $E G$ is contractible (Milnor's join model is a contractible free G-space).

[F2]

Assuming AC, a numerable bundle is a Hurewicz fibration, so its lifting function gives a continuous endpoint map on based loops (Numerable fiber bundles are hurewicz fibrations).

[F3]

The fibration long exact sequence includes $π_{k + 1} (B G) \to π_{k} (G) \to π_{k} (E G)$ for $k \geq 1$ and the exact component segment $π_{1} (E G) \to π_{1} (B G) \to π_{0} (G) \to π_{0} (E G)$ . Its boundary is computed by choosing a lift ending at the basepoint and restricting to the opposite face; the resulting class is independent of the lift. Under the library convention its component boundary is the inverse of the forward endpoint label (Long exact sequence of homotopy groups of a fibration).

[F4]

Assuming AC, Whitehead promotes a weak equivalence between CW models to a homotopy equivalence (Whitehead theorem).

[F5]

Inversion $g \mapsto g^{- 1}$ is a based homeomorphism of a topological group.

[A1]

AC is used by the lifting-function and Whitehead suppliers, and nowhere else in this argument (The Axiom of Choice).

Proof

Given: The Milnor bundle, based by $e_{0} \mapsto b_{0}$ and with its fiber identified by $g \mapsto e_{0} g$ , and [A1].

1.1A1F1F2F5

By [A1, F1, F2], lift a loop $γ$ from $e_{0}$ . Its endpoint lies in $p^{- 1} (b_{0})$ and is uniquely $e_{0} g$ ; define $ε (γ) = g$ and $δ (γ) = g^{- 1}$ . The lifting function is continuous and sends the constant loop to $e_{0}$ , so both maps are continuous and based. The exact AC expenditure is the well-ordering used by [F2] to construct the lifting function for a numerable bundle.

2.1F1F2F3step 1.1

We compare the chosen map $δ$ with the class-level boundary in [F3]. Let a based $S^{k}$ -family of loops be given. The lifting function produces a continuous family ${\tilde{γ}}_{s}$ starting at $e_{0}$ and ending at $e_{0} ε (γ_{s})$ . Right-translate the whole $s$ -th lift by $ε (γ_{s})^{- 1}$ . The translated family still covers $γ_{s}$ , now ends at $e_{0}$ , and its initial face is $e_{0} δ (γ_{s})$ . This is precisely the lift-and-restrict representative used to define the connecting homomorphism in [F3]. Hence, for every $k \geq 1$ , $δ_{*}$ agrees with the connecting homomorphism after $π_{k} (Ω B G) ≅ π_{k + 1} (B G)$ ; the same argument for a single loop gives the asserted map on components. Notice that this compares induced classes, not two point-set maps obtained from unrelated lifting choices.

3.1F1F3step 2.1

Contractibility gives $π_{j} (E G) = 0$ for every $j \geq 1$ and one component. Exactness in [F3] therefore makes

$δ_{*} : π_{k} (Ω B G) ≅ π_{k + 1} (B G) ⟶ π_{k} (G)$

an isomorphism for every $k \geq 1$ , while the component segment makes $δ_{*} : π_{0} (Ω B G) \to π_{0} (G)$ a bijection. Repeating the translated-lift comparison of Step 2.1 after rebasing at a representative loop gives the same isomorphisms at every basepoint. Thus $δ$ is a weak homotopy equivalence. By [F5], $ε = inv \circ δ$ is one as well. [F1, F3, F5, step 2.1]

4.1A1F4F5step 3.1

If both spaces have CW type, choose based CW models under [A1]. The induced comparison of models is weak by Step 3.1, so [F4] supplies a based homotopy inverse; transporting it through the model equivalences makes $δ$ a based homotopy equivalence. Composing with inversion gives the same conclusion for $ε$ . Besides the lifting-function use in Step 1.1, AC is spent here exactly through [F4]. Without those CW-type hypotheses, only the proved weak equivalences are asserted. $□$

Depends on

Used by

The classifying space of a discrete group is a K(G,1) Corollary
Path-loop Serre computation of CP infinity Example

Dependency tree · two levels

28 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

James Davis and Paul Kirk, Lecture Notes in Algebraic Topology (standard reference, not scraped)
Haynes Miller, MIT 18.906 Algebraic Topology II lecture notes (standard reference, not scraped)