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 be a numerable locally trivial fiber bundle with compact Hausdorff fiber over a paracompact Hausdorff base . Then is paracompact and Hausdorff. If in addition is compactly generated, then is compactly generated (and hence CGWH). If and have the homotopy type of CW complexes, then 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 .
Facts & Assumptions
Given: AC, a numerable locally trivial fiber bundle with compact Hausdorff fiber over a paracompact Hausdorff base .
A locally trivial bundle has fiber homeomorphisms 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 is with each a homeomorphism of (Locally trivial fiber bundle).
Let be compact, , and open with . Then there is an open with and (Tube lemma: if is compact and an open contains , then contains for some open ).
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).
Products of Hausdorff spaces are Hausdorff (Arbitrary products preserve , , and Hausdorffness).
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).
Every numerable fiber bundle is a Hurewicz fibration (Numerable fiber bundles are hurewicz fibrations).
An open subset of a compactly generated space is compactly generated when each point of has an open neighborhood in the ambient space whose closure lies in ; 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).
AC is the Axiom of Choice in the form fixed by The Axiom of Choice.
Proof
is Hausdorff. Let be points of . If , choose disjoint open containing them, possible because is Hausdorff; then and are disjoint open subsets of containing and . If , choose a chart domain containing and apply the homeomorphism : the images lie in , which is Hausdorff by [F4] because and are Hausdorff; separating them there and applying separates and in .
is paracompact. Let be an open cover of . For the fiber is compact, so has a finite subfamily covering ; fix such a finite list for every (this is the only choice made, and it is a choice of one set for every element of ). In a chart about the union of the listed open sets contains in ; the tube lemma [F2] applied with compact factor gives an open with contained in that union, that is, is covered by the finitely many listed members of . The family is an open cover of the paracompact space , so by [F3] it has a locally finite open refinement . Choose for each an index with ; then the family consisting of the open sets , for all and all in the finite list attached to , covers and refines , since is covered by that finite list. It is locally finite: given with , local finiteness of at supplies an open meeting only finitely many , and then the neighborhood of meets only for those finitely many . Hence every open cover of has a locally finite open refinement, so is paracompact by [F3].
The compact-generation and CW-type clauses. Suppose first that is compactly generated. Since a paracompact Hausdorff space is regular, every point of a chart domain has an open neighborhood in whose closure lies in ; [F7] therefore makes compactly generated. The compact Hausdorff fiber is locally compact, so [F7] makes each ordinary product , and hence each open chart , compactly generated. Compact generation is local on this open cover: if meets every compact subspace of in a closed set, then has the same property in the compactly generated chart and is closed there; the chart cover then makes closed in . Thus is compactly generated. It is weak Hausdorff because it is Hausdorff by step 1.1, so it is CGWH. Independently, if and have the homotopy type of CW complexes, then [F6] makes a Hurewicz fibration, and [F5] gives the homotopy type of a CW complex for .
Consequences and boundary cases. The projective bundle of a numerable rank- bundle with is a numerable fiber bundle with fiber , and the flag bundle is a composite of such bundles, each with the compact CW complex 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 of finitely many such total spaces is a numerable bundle over with compact fiber, so the same clauses apply. If then ; if is a point then over ; if then . In each case paracompactness, Hausdorffness, compact generation and the CW-type conclusion hold under their stated hypotheses because the empty space and itself have the corresponding properties. For projective fibers, the one-point case is and the empty convention is ; both are compact and have CW type.
Depends on
- Locally trivial fiber bundle
- Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word
- Tube lemma: if $K$ is compact and an open $N \subseteq X \times Z$ contains $K \times \{z_0\}$, then $N$ contains $K \times W$ for some open $W \ni z_0$
- Arbitrary products preserve $T_0$, $T_1$, and Hausdorffness
- Numerable fiber bundles are hurewicz fibrations
- The Axiom of Choice
Used by
- Characteristic class as a universal natural bundle class Definition
- Complex flag bundle and Chern roots Definition
- Complex projective bundle and tautological complex line Definition
- Real flag bundle and Stiefel–Whitney roots Definition
- Real projective bundle and tautological line Definition
- Euler class of the universal oriented two-plane Example
- The universal oriented sphere-bundle total space has the homotopy type of BSO(n-1) Lemma
- Complex splitting principle with integral injective pullback Theorem
- Integral complex projective bundle theorem Theorem
- Mod-two real projective bundle theorem Theorem
- Real splitting principle with mod-two injective pullback Theorem
- Uniqueness of Chern classes from the splitting principle Theorem
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
- Allen Hatcher, Vector Bundles & K-Theory (standard reference, not scraped)
- Rolf Schon, Fibrations Over a CWh-Base (standard reference, not scraped)
- Haynes Miller, MIT 18.906 Algebraic Topology II lecture notes (standard reference, not scraped)
- J. P. May, A Concise Course in Algebraic Topology (standard reference, not scraped)