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.1A1

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.2F1F2F3F4

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$ .

1.3F1

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.1A1F1step 1.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}$ .

3.1F1step 2.1

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

$Φ (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.1F4step 3.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.

5.1A1step 1.2step 1.3step 4.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. $□$

Numerable principal bundles are classified by maps to BG

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources