Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses

Statement

Assume AC. Let p:SB be a numerable locally trivial fiber bundle with compact Hausdorff fiber F over a paracompact Hausdorff base B. Then S is paracompact and Hausdorff. If in addition B is compactly generated, then S is compactly generated (and hence CGWH). If B and F have the homotopy type of CW complexes, then S has the homotopy type of a CW complex.

Consequently the total spaces of the projective bundle and of the flag bundle of a numerable bundle with compact fiber over a paracompact Hausdorff CGWH base of CW type are again paracompact Hausdorff CGWH spaces of CW type, and the same holds for finitely many fiber products of such total spaces over B.

Facts & Assumptions

Given: AC, a numerable locally trivial fiber bundle p:SB with compact Hausdorff fiber F over a paracompact Hausdorff base B.

[F1]

A locally trivial bundle has fiber homeomorphisms θi:p1(Ui)Ui×F over an open cover. A numeration additionally supplies a partition of unity whose cozero sets, not necessarily the original chart cover, are locally finite and whose supports lie in the chart domains; the overlap change on UiUj is (b,x)(b,gji(b,x)) with each gji(b,) a homeomorphism of F (Locally trivial fiber bundle).

[F2]

Let KX be compact, z0Z, and NX×Z open with K×{z0}N. Then there is an open WZ with z0W and K×WN (Tube lemma: if K is compact and an open NX×Z contains K×{z0}, then N contains K×W for some open Wz0).

[F3]

A space is paracompact when every open cover has a locally finite open refinement that covers it (Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word).

[F4]

Products of Hausdorff spaces are Hausdorff (Arbitrary products preserve T0, T1, and Hausdorffness).

[F5]

Schon's Theorem 2: a Hurewicz fibration whose base and fiber have the homotopy type of CW complexes has total space of the same type (Rolf Schon, Fibrations Over a CWh-Base, Theorem 2, printed page 165).

[F6]

Every numerable fiber bundle is a Hurewicz fibration (Numerable fiber bundles are hurewicz fibrations).

[F7]

An open subset U of a compactly generated space is compactly generated when each point of U has an open neighborhood in the ambient space whose closure lies in U; also, the ordinary product of a compactly generated space with a locally compact Hausdorff space is compactly generated (May, A Concise Course in Algebraic Topology, Chapter 5, printed pp.39–40).

[A1]

AC is the Axiom of Choice in the form fixed by The Axiom of Choice.

Proof

1.1

S is Hausdorff. Let ss be points of S. If p(s)p(s), choose disjoint open U,VB containing them, possible because B is Hausdorff; then p1(U) and p1(V) are disjoint open subsets of S containing s and s. If p(s)=p(s)=b, choose a chart domain Ui containing b and apply the homeomorphism θi: the images lie in Ui×F, which is Hausdorff by [F4] because UiB and F are Hausdorff; separating them there and applying θi1 separates s and s in S.

F1F4
1.2

S is paracompact. Let W be an open cover of S. For bB the fiber SbF is compact, so W has a finite subfamily covering Sb; fix such a finite list for every b (this is the only choice made, and it is a choice of one set for every element of B). In a chart θi about b the union of the listed open sets contains {b}×F in Ui×F; the tube lemma [F2] applied with compact factor F gives an open Vbb with Vb×F contained in that union, that is, p1(Vb) is covered by the finitely many listed members of W. The family {Vb} is an open cover of the paracompact space B, so by [F3] it has a locally finite open refinement {Vβ}βJ. Choose for each β an index b(β) with VβVb(β); then the family consisting of the open sets Wp1(Vβ), for all β and all W in the finite list attached to b(β), covers S and refines W, since p1(Vβ)p1(Vb(β)) is covered by that finite list. It is locally finite: given sS with p(s)=b0, local finiteness of {Vβ} at b0 supplies an open Nb0 meeting only finitely many Vβ, and then the neighborhood p1(N) of s meets p1(Vβ) only for those finitely many β. Hence every open cover of S has a locally finite open refinement, so S is paracompact by [F3].

F1F2F3A1
1.3

The compact-generation and CW-type clauses. Suppose first that B is compactly generated. Since a paracompact Hausdorff space is regular, every point of a chart domain Ui has an open neighborhood in B whose closure lies in Ui; [F7] therefore makes Ui compactly generated. The compact Hausdorff fiber F is locally compact, so [F7] makes each ordinary product Ui×F, and hence each open chart p1(Ui), compactly generated. Compact generation is local on this open cover: if AS meets every compact subspace of S in a closed set, then Ap1(Ui) has the same property in the compactly generated chart and is closed there; the chart cover then makes A closed in S. Thus S is compactly generated. It is weak Hausdorff because it is Hausdorff by step 1.1, so it is CGWH. Independently, if B and F have the homotopy type of CW complexes, then [F6] makes p:SB a Hurewicz fibration, and [F5] gives the homotopy type of a CW complex for S.

F5F6F7step 1.1
2.1

Consequences and boundary cases. The projective bundle of a numerable rank-n bundle EB with n1 is a numerable fiber bundle with fiber RPn1, and the flag bundle is a composite of such bundles, each with the compact CW complex RPj as fiber; if the initial base is paracompact Hausdorff CGWH of CW type, the three preceding steps apply at each stage and give the same conclusion for every intermediate total space. A fiber product over B of finitely many such total spaces is a numerable bundle over B with compact fiber, so the same clauses apply. If F= then S=; if F is a point then SB over B; if B= then S=. In each case paracompactness, Hausdorffness, compact generation and the CW-type conclusion hold under their stated hypotheses because the empty space and B itself have the corresponding properties. For projective fibers, the one-point case is RP0={} and the empty convention is RP1=; both are compact and have CW type.

F5F6F7step 1.1step 1.2step 1.3

Depends on

Used by

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