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.
The Hawaiian earring is locally path-connected but has no universal cover
Example
The Hawaiian earring is locally path-connected but is not semilocally simply connected at its wedge point. Consequently it has no universal cover.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
The loop in is not nullhomotopic. (The projected unit interval is not nullhomotopic in ).
If a space admits a universal covering, then it is semilocally simply connected. No local path-connectedness hypothesis is required. (A space admitting a universal covering is semilocally simply connected).
A space is semilocally simply connected at when there is a neighbourhood of and a basepoint-preserving inclusion whose induced map on fundamental groups is trivial (def-neighbourhood-top, def-induced-homomorphism-on-fundamental-groups, def-based-loops-and-fundamental-group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected. (Semilocally simply connected spaces with explicit basepoint convention).
The quotient topology. Let be a topological space (def-topological-space), let be a set and let be a surjection (def-injection-surjection-bijection). The quotient topology on induced by is the final topology of the one-element family (def-initial-and-final-topology): That this is a topology is discharged in def-initial-and-final-topology, where every final topology is verified to satisfy (T1), (T2) and (T3). Dually, is closed in exactly when is closed in , because . (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).
Verification
Model the earring as countably many copies of with diameters tending to zero and all zero classes identified, using the standard shrinking-wedge metric.
Away from the wedge point, sufficiently short open arcs are path-connected neighbourhoods.
At the wedge point, every open neighbourhood contains a smaller metric ball whose intersection with each circle is an arc through the wedge point and which contains every sufficiently small circle, so that ball is path-connected.
Retraction to one such small circle and the essential unit loop show its inclusion carries a nontrivial loop, so semilocal simple connectedness fails at the wedge point.
The necessity theorem then rules out a universal cover.
The preceding construction and implications establish the assertion.
Depends on
- The projected unit interval is not nullhomotopic in $\mathbb R/\mathbb Z$
- A space admitting a universal covering is semilocally simply connected
- Semilocally simply connected spaces with explicit basepoint convention
- The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 44 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Allen Hatcher, Algebraic Topology, §1.3 (standard reference, not scraped)
- Marco Gualtieri, MAT1300 Week 4 Term 2, §1.6 (standard reference, not scraped)
- Omar Antolín Camarena, Proper local homeomorphisms and covering maps (standard reference, not scraped)