TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Milnor's join model is a contractible free G-space

Statement

For a well-pointed topological group $G$ of CW type, the diagonal action on Milnor's $E G$ is free, $E G$ is contractible, and

$p : E G ⟶ B G$

is a numerable principal $G$ -bundle. The numeration satisfies the library's support-subordinate convention, not merely cozero containment.

The embeddings

$e (\sum_{i} t_{i} g_{i}) = \sum_{i} t_{i} g_{i} in slot 2 i, o (\sum_{i} t_{i} g_{i}) = \sum_{i} t_{i} g_{i} in slot 2 i + 1$

are $G$ -equivariantly homotopic to the identity. If $a, b : T \to E G$ are continuous equivariant maps, then $(1 - t) e (a (-)) + t o (b (-))$ is a continuous equivariant homotopy.

For $G = S^{1}$ or $G = Z / 2$ , the selected compact-group topology identifies $B G$ with the standard weak CW colimit of the finite projective quotients ${C P}^{N}$ or ${R P}^{N}$ , respectively.

Facts & Assumptions

[F1]

The finite quotient joins provide the set of formal sums. For compact Hausdorff $G$ , $E G$ has their ordinary weak direct-limit topology; otherwise it has the ordinary, un-kified coordinate-label strong topology. In both branches $B G$ has the ordinary orbit-quotient topology and weights and positive-locus labels are continuous. Continuity into the strong branch is equivalent to continuity of those coordinates; continuity out of the weak branch is checked on its compact finite stages (Milnor's infinite-join model of EG).

[F2]

A locally finite family of nonnegative continuous functions has continuous sum (A locally finite family of continuous nonnegative functions has a continuous pointwise sum); finite maxima, sums, and division by a positive function are continuous by elementary real arithmetic.

[F3]

In the library's numerability convention, the closed support of each partition function must lie inside an assigned trivializing open set, and the chart uses an ordinary product (Locally trivial fiber bundle).

[F4]

For $G = S^{1}$ and $G = Z / 2$ , the compact finite quotient joins are respectively spheres $S^{2 N + 1}$ and $S^{N}$ , with quotient spaces ${C P}^{N}$ and ${R P}^{N}$ , compatibly with stage inclusions (Finite join models for the circle and the two-point group).

Proof

Given: $G$ , $E G$ , $B G$ , and $p$ as in the statement.

1.1

If $x h = x$ and $t_{i} (x) > 0$ , equality of join representatives gives $g_{i} h = g_{i}$ , hence $h = 1$ . Some coordinate is positive because the coordinates sum to one, so the action is free.

1.2

We construct the promised contraction rather than infer contractibility from vanishing homotopy groups. Let $I_{n} = [1 - 2^{- n}, 1 - 2^{- n - 1}]$ and $α_{n} (s) = 2^{n + 1} s - 2^{n + 1} + 2$ . For $s \in I_{n}$ , define $R_{s} (x)$ by retaining the coordinates $0, \dots, n$ and, for every $j \geq 1$ , replacing the term $t_{n + j} g_{n + j}$ by

$α_{n} (s) t_{n + j} g_{n + j} in slot n + 2 j - 1, (1 - α_{n} (s)) t_{n + j} g_{n + j} in slot n + 2 j .$

At $s = 0$ this is the even-coordinate embedding $R_{0} (\sum t_{i} g_{i}) = \sum t_{i} g_{i}$ with the $i$ th term placed in slot $2 i$ ; at $s = 1$ put $R_{1} = id$ . At the common endpoint of $I_{n}$ and $I_{n + 1}$ , the first tail coordinate has reached slot $n + 1$ and every later coordinate occupies the same slot in the two formulas. Thus the formulas agree. First consider the noncompact, strong-topology branch. Fix an output slot $k$ . Only the finitely many intervals $I_{0}, \dots, I_{k - 1}$ can change its coordinate: for $s \geq 1 - 2^{- k}$ that output coordinate and, where positive, its label are exactly the input $k$ th coordinate and label. On each earlier interval its weight is a continuous product of $α_{n} (s)$ or $1 - α_{n} (s)$ with one input weight, or is an unchanged input weight. Wherever that output weight is positive, its label is the corresponding continuous input label. At interval endpoints the two weight formulas and their positive labels agree, so finite pasting gives continuity of the $k$ th weight and positive-label map on the ordinary product $E G \times I$ , including at $s = 1$ . The strong-coordinate criterion of [F1] proves $R : E G \times I \to E G$ continuous. It is $G$ -equivariant because it moves weights and slots without changing labels. No compact image is assumed to lie in a finite stage; Step 4.1 checks ordinary continuity separately for the compact weak branch. [F1]

1.3

In the noncompact strong branch the diagonal action is continuous for ordinary $E G \times G$ : its $i$ th weight is $t_{i} (x)$ , and on the open locus $t_{i} (x) > 0$ its $i$ th label is $g_{i} (x) h$ , continuous by ordinary group multiplication. The strong-coordinate criterion in [F1] proves continuity of the action. Put $U_{i} = {b \in B G : t_{i} (b) > 0}$ and $E_{i} = p^{- 1} (U_{i})$ . The sets $U_{i}$ cover $B G$ because some weight is positive, and each $E_{i}$ is a saturated open subset of $E G$ . The map $N_{i} : E_{i} \to E_{i}$ , $N_{i} (x) = x g_{i} (x)^{- 1}$ , is continuous by the ordinary action and inversion; $N_{i} (x h) = N_{i} (x)$ and its $i$ th label is $1$ . Restricting the ordinary quotient map $p$ to the saturated open $E_{i}$ is still a quotient map, so $N_{i}$ descends to a continuous section $s_{i} : U_{i} \to E_{i}$ . The maps

$U_{i} \times G ⟶ p^{- 1} (U_{i}), (b, h) ⟼ s_{i} (b) h, x ⟼ (p (x), g_{i} (x))$

are continuous for the ordinary product and subspace topologies: the first is the composite of $s_{i} \times {i d}_{G}$ with the ordinary action, and the second is continuous by the ordinary product universal property and the partial-label continuity in [F1]. They are inverse because $g_{i} (s_{i} (b) h) = h$ and $s_{i} (p (x)) g_{i} (x) = x$ . Thus they are precisely the ordinary principal-bundle charts required by [F3]. Step 3.1 supplies the same charts for the compact weak branch. [F1, F3]

1.4

The coordinate family need not be locally finite, so set

F1F2

$w_{i} = \max (0, t_{i} - \sum_{j < i} t_{j}) .$

At a point, its least positive coordinate has positive $w_{i}$ , so $W = \sum_{i} w_{i}$ is everywhere positive. If $N$ is the last positive coordinate at $b$ , then on a neighborhood where $\sum_{j \leq N} t_{j} > 1 / 2$ , every $i > N$ satisfies $t_{i} < 1 / 2 < \sum_{j < i} t_{j}$ and hence $w_{i} = 0$ . Thus $(w_{i})$ is locally finite, $W$ is continuous, and $v_{i} = w_{i} / W$ is a locally finite partition with ${v_{i} > 0} \subseteq U_{i}$ . [F1, F2]

2.1

The even image uses no odd coordinate. Hence

F1step 1.2

$C_{u} (\sum_{i} t_{i} g_{i} in slot 2 i) = u 1 in slot 1 + \sum_{i} (1 - u) t_{i} g_{i} in slot 2 i$

is a homotopy from the even embedding to the identity-labelled vertex in slot $1$ . In the noncompact strong branch, its slot- $1$ weight is $u$ with label $1$ where positive; its even-slot weights are $(1 - u) t_{i}$ with label $g_{i}$ where positive; every other weight is zero. These are continuous weights and positive-locus labels, so [F1] proves ordinary continuity of $C$ . Reversing $R$ and then applying $C$ contracts that $E G$ . Notice that $C$ is not asserted equivariant. Splitting each even-coordinate weight as $(1 - u) t_{i}$ in slot $2 i$ and $u t_{i}$ in slot $2 i + 1$ , both carrying $g_{i}$ , likewise gives an ordinary-continuous $G$ -equivariant homotopy from the even embedding to the odd embedding. Consequently both parity embeddings are $G$ -equivariantly homotopic to the identity in this branch. For continuous equivariant $a, b : T \to E G$ , the disjoint-support interpolation has even-slot weights $(1 - u) t_{i} (a (z))$ and odd-slot weights $u t_{i} (b (z))$ on $T \times I$ . On each positive-weight locus its label is respectively $g_{i} (a (z))$ or $g_{i} (b (z))$ , hence continuous there. The strong-coordinate criterion of [F1] proves the interpolation continuous for the ordinary product $T \times I$ ; termwise it is equivariant. No compact-stage factorization is used in this branch; Step 4.1 treats the compact weak branch. [F1, step 1.2]

2.2

Cozero containment in Step 1.4 is weaker than [F3]. Choose $ε_{i} = 2^{- i - 2}$ , so $\sum_{i} ε_{i} = 1 / 2$ , and put $a_{i} = \max (0, v_{i} - ε_{i})$ . Some $a_{i}$ is positive at every point, since otherwise $1 = \sum_{i} v_{i} \leq 1 / 2$ . The family is locally finite, $A = \sum_{i} a_{i}$ is positive and continuous, and $ρ_{i} = a_{i} / A$ is a partition of unity. Moreover

F2F3step 1.4

$supp (ρ_{i}) \subseteq {v_{i} \geq ε_{i}} \subseteq U_{i} .$

3.1

Now let $G$ be any compact Hausdorff group, so [F1] selects the ordinary weak direct limit $E G = {colim}_{N} J_{N}^{q}$ . Each $J_{N}^{q}$ is compact Hausdorff: the relation identifying labels at zero-weight slots is closed in $(Δ^{N} \times G^{N + 1})^{2}$ , and appending zero gives a closed embedding. Hence this sequential compact-stage limit is a $k_{ω}$ space. Its ordinary finite products with itself, $G$ , and $I$ have the final topology for the products of finite compact stages (Franklin--Thomas, property 4). On $J_{M}^{q} \times G$ , the diagonal action is the finite quotient of the continuous coordinate action and is continuous; the finite quotient map remains quotient after multiplying by compact $G$ , since its source is compact and its target Hausdorff. The product-stage criterion therefore proves that $E G \times G \to E G$ is ordinary-continuous. The same ordinary action, continuous positive-locus labels, and saturated-open quotient argument of Step 1.3 give the explicit sections $s_{i}$ and inverse ordinary charts $U_{i} \times G ≅ p^{- 1} (U_{i})$ in this branch as well. Since each $t_{i}$ is stagewise continuous, Steps 1.4 and 2.2 give the same support-subordinate numeration.

F1F3step 1.3step 1.4step 2.2

4.1

Every required homotopy in the compact branch is likewise ordinary-continuous by the product-stage criterion, not by a claim that every compact image lies in a finite join. On $J_{M}^{q} \times I$ , the formula for $R$ from Step 1.2 uses only the finitely many intervals before $1 - 2^{- M}$ and is then the identity; finite closed pasting into $J_{2 M}^{q}$ proves continuity, including at $s = 1$ . The cone $C$ and even-to-odd interpolation of Step 2.1 map $J_{M}^{q} \times I$ into a fixed finite join and are continuous finite quotient formulas. The disjoint-support interpolation on $J_{M}^{q} \times J_{N}^{q} \times I$ is a continuous finite quotient formula into $J_{\max (2 M, 2 N + 1)}^{q}$ . Since ordinary products of these compact-stage limits have the stated final topology, all four maps are continuous on their full ordinary product domains. Composing the last one with arbitrary continuous equivariant $a, b : T \to E G$ proves its asserted continuity on $T \times I$ ; the formulas are $G$ -equivariant where claimed. Reversing $R$ and following it by $C$ contracts $E G$ . Finally, ordinary orbit quotients commute with this final topology: a set in $B G$ is open exactly when its pullback to every $J_{N}^{q}$ is open, equivalently when its intersection with every $J_{N}^{q} / G$ is open. Thus [F4] identifies the selected $B G$ for $S^{1}$ or $Z / 2$ literally with the standard weak CW colimit ${colim}_{N} {C P}^{N}$ or ${colim}_{N} {R P}^{N}$ .

F1F4step 1.2step 2.1step 3.1

5.1

Step 1.1 proves freeness in both branches. Steps 1.2, 1.3, and 2.1 prove ordinary continuity for the noncompact strong branch; Steps 3.1--4.1 prove it for the compact weak branch. The resulting ordinary charts and $(ρ_{i})$ satisfy the exact library numerability convention, and the contractions and parity homotopies establish every remaining assertion. The trivial and disconnected groups are included. $□$

F1F2F3F4step 1.1step 1.2step 1.3step 1.4step 2.1step 2.2step 3.1step 4.1

Depends on

Used by

The classifying space of a discrete group is a K(G,1) Corollary
Infinite complex projective space is K(Z,2) Example
Real projective infinity as BZ/2 Example
The based loop space of BG recovers G weakly Proposition
Numerable principal bundles are classified by maps to BG Theorem

Dependency tree · two levels

17 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

John Milnor, Construction of Universal Bundles II (standard reference, not scraped)
Tammo tom Dieck, Algebraic Topology (standard reference, not scraped)
Dale Husemoller, Fibre Bundles, Third Edition (standard reference, not scraped)
Stanley P. Franklin and Barbara V. Smith Thomas, A Survey of k-omega Spaces (standard reference, not scraped)