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.
FALSE: every compact path-connected subset of has a universal cover
Statement
Every compact path-connected subset of admits a universal covering space.
Facts & Assumptions
Given: The Hawaiian earring , based at the common point .
The Hawaiian earring is a compact and path-connected subset of (The Hawaiian earring is compact and path-connected).
For every , the Hawaiian earring admits a retraction onto its circle (The Hawaiian earring retracts onto each of its circles).
A space is semilocally simply connected at when some neighbourhood of has inclusion-induced homomorphism trivial (Semilocally simply connected spaces with explicit basepoint convention).
If a space admits a universal covering, then it is semilocally simply connected (A space admitting a universal covering is semilocally simply connected).
Under the isomorphism from the geometric unit circle's fundamental group to , the once-around loop corresponds to and is therefore nontrivial (The trigonometric loops give ).
Induced maps on fundamental groups are functorial, so a homomorphism with a left inverse is injective (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).
A neighbourhood contains an open set containing the point, and open subsets of a subspace are traces of ambient open sets (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).
In a metric topology, every open set contains a metric ball about each of its points (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).
For every real there is an integer with (For every in a complete ordered field there is a natural with ).
Refutation
By [F1], satisfies the compactness and path-connectedness hypotheses of the proposed statement.
Let be any neighbourhood of in . By [F4], there is an ambient open set with and . By [F5], choose with , so . Since , [L4] gives an with .
Let be inclusion and the retraction of [F2]. Functoriality gives , so is injective. The pointed affine homeomorphism carries the geometric unit circle based at onto based at and carries the once-around loop of [L2] to a loop in . By [L2] and [L3], in ; injectivity of therefore makes its image nontrivial in . Since , the same is a loop in .
Since every neighbourhood of contains such a loop, no inclusion-induced map is trivial. Thus is not semilocally simply connected at .
By [L1], the Hawaiian earring has no universal cover. Together with step 1.1, it is a compact path-connected planar counterexample to the proposed universal claim.
Depends on
- The Hawaiian earring is compact and path-connected
- The Hawaiian earring retracts onto each of its circles
- Semilocally simply connected spaces with explicit basepoint convention
- A space admitting a universal covering is semilocally simply connected
- The trigonometric loops give $\pi_1(\{(x,y):x^2+y^2=1\},(1,0))\cong\mathbb Z$
- Induced fundamental-group maps are well defined, functorial and invariant under based homotopy
- Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
- Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
40 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, Algebraic Topology, Example 1.25 and §1.3 (standard reference, not scraped)