TheoremStatement: 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.

Numerable principal bundles are classified by maps to BG

Statement

Assume AC. For a well-pointed topological group $G$ of CW type and a CGWH base $X$ , pullback of Milnor's bundle induces a bijection

$[X, B G] \overset{≅}{\to} {Bun}_{G}^{n u m} (X), [f] ⟼ [f^{*} E G],$

where the right side consists of isomorphism classes of numerable right principal $G$ -bundles. A locally trivial bundle over a paracompact base is covered only after a separate theorem supplies numerability.

Facts & Assumptions

[F1]

Milnor's $E G \to B G$ is a numerable principal bundle; $E G$ is contractible; the even and odd coordinate embeddings are equivariantly homotopic to its identity; and disjoint-support interpolation after those embeddings is a continuous equivariant homotopy (Milnor's join model is a contractible free G-space).

[F2]

Pullback preserves principal-bundle charts (Associated bundle is locally trivial and functorial under pullback), and the pullback of a support-subordinate partition is support-subordinate by inverse-image functoriality of support.

[F3]

The lifting construction for a numerable bundle is made from chart transports and therefore commutes with a right principal action (Numerable fiber bundles are hurewicz fibrations).

[F4]

A continuous equivariant map between principal $G$ -bundles over the same base is a bundle isomorphism, as follows in principal charts from the torsor condition (Principal g bundle and associated fiber bundle).

[A1]

AC chooses members and chart data for arbitrary indexed families in the countabilization below. Finite supplied numerations do not require this use (The Axiom of Choice).

Proof

Given: $X, G$ and [A1] as in the statement.

1.1

First let $π : P \to X$ be numerable with an arbitrary indexed numeration $(ρ_{i})_{i \in I}$ subordinate to principal charts $U_{i}$ . For each nonempty finite $S \subseteq I$ , define

$u_{S} (x) = \max (0, \min_{i \in S} ρ_{i} (x) - \sup_{j \notin S} ρ_{j} (x)),$

where the supremum of an empty family is $0$ . Near each point only finitely many $ρ_{i}$ can be nonzero, so the displayed supremum is locally a finite maximum and $u_{S}$ is continuous. At a point, let $S$ be the finite set of indices attaining the largest positive value; then $u_{S} > 0$ . If $S \neq S^{'}$ have the same cardinality, their cozero sets are disjoint, since indices in $S ∖ S^{'}$ and $S^{'} ∖ S$ would otherwise have to be strictly larger than one another. [A1]

1.2

The assignment depends only on the homotopy class of $f$ . If $H : X \times I \to B G$ joins $f_{0}$ to $f_{1}$ , then $H^{*} E G$ is numerable by [F1, F2]. Apply the lifting function of [F3] to the paths $t \mapsto H (x, t)$ . Holding the principal group coordinate in every chart makes endpoint transport an equivariant map from the restriction over $X \times {0}$ to that over $X \times {1}$ . It is a bundle isomorphism by [F4]. Thus $f_{0}^{*} E G ≅ f_{1}^{*} E G$ .

F1F2F3F4

1.3

Conversely, suppose $f_{0}^{*} E G ≅ f_{1}^{*} E G$ and identify both with one principal bundle $P$ . Projection to the $E G$ coordinate gives equivariant maps $q_{0}, q_{1} : P \to E G$ covering $f_{0}, f_{1}$ . By [F1], equivariantly deform $q_{0}$ to a map $q_{0}^{e v}$ supported in even coordinates and $q_{1}$ to $q_{1}^{o d d}$ supported in odd coordinates. Their disjoint supports make

$K (p, t) = (1 - t) q_{0}^{e v} (p) + t q_{1}^{o d d} (p)$

a well-defined continuous equivariant map $P \times I \to E G$ . Passing to orbits gives a homotopy between the two deformed base maps. Concatenating with the orbit homotopies furnished by [F1] proves $f_{0} ≃ f_{1}$ . [F1]

2.1

For $m \geq 1$ , set $w_{m} = \sum_{∣ S ∣ = m} u_{S}$ . These sums are locally finite, their cozero sets $V_{m}$ cover $X$ , and $V_{m}$ is the disjoint union of the cozero sets of the $u_{S}$ with $∣ S ∣ = m$ . Each such piece lies in every $U_{i}$ with $i \in S$ . Use [A1] to choose one $i (S) \in S$ ; restricting its section and patching over the disjoint pieces gives a section $s_{m} : V_{m} \to P$ . Normalize the $w_{m}$ , then apply the threshold construction of the Milnor theorem with positive numbers summing to less than one. We obtain a countable locally finite partition $(λ_{m})_{m \geq 1}$ with $supp λ_{m} \subseteq V_{m}$ .

A1F1step 1.1

3.1

For $p \in P$ over $x$ , whenever $λ_{m} (x) > 0$ write uniquely $p = s_{m} (x) a_{m} (p)$ . Define

F1step 2.1

$Φ (p) = \sum_{m \geq 1} λ_{m} (x) a_{m} (p) \in E G .$

Only finitely many terms occur locally. Support containment makes the quotient formula continuous even where a label ceases to be defined, and on such a neighborhood it factors through one finite-join quotient. Thus $Φ$ is continuous. It is equivariant because $a_{m} (p g) = a_{m} (p) g$ , and it descends to a map $f : X \to B G$ . [F1, step 2.1]

4.1

The map $p \mapsto (π (p), Φ (p))$ is an equivariant map $P \to f^{*} E G$ over $X$ . On each fiber it is a map of right $G$ -torsors and is therefore bijective. In principal charts it has the form $(x, g) \mapsto (x, c (x) g)$ , whose inverse is $(x, h) \mapsto (x, c (x)^{- 1} h)$ ; hence [F4] makes it a bundle isomorphism. Every numerable bundle is therefore pulled back from Milnor's bundle.

F4step 3.1

5.1

Steps 1.2, 1.3, and 4.1 prove well-definedness, injectivity, and surjectivity of the displayed map. If $X = \emptyset$ , both sides are singletons. If the given numeration is finite, its countabilization and all chart choices in Steps 1.1--3.1 are finite; for arbitrary index sets, [A1] is exactly the declared choice use. The theorem makes no claim that paracompactness implies numerability. $□$

A1step 1.2step 1.3step 4.1

Depends on

Used by

Principal-bundle classification can fail without numerability Counterexample
The trivial principal bundle has a nullhomotopic classifying map Example

Dependency tree · two levels

21 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

Dale Husemoller, Fibre Bundles, Third Edition (standard reference, not scraped)
Haynes Miller, MIT 18.906 Algebraic Topology II lecture notes (standard reference, not scraped)