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 continuous self-map of the circle is nullhomotopic
Statement
False claim: every continuous map is nullhomotopic.
The identity map is a counterexample.
Facts & Assumptions
Given: The identity map of .
A map is nullhomotopic if it is homotopic to a constant map for some (Nullhomotopic maps and contractible spaces).
is a covering map ( is a covering map with translated interval sheets).
A homotopy through a covering has a unique lift extending any prescribed lift of (Existence and uniqueness of homotopy lifts through a covering map).
A path through a covering has a unique lift once its initial point is prescribed (Existence and uniqueness of path lifts through a covering map).
The standard loop is (The standard circle loops for ).
For the quotient projection, exactly when , and for every integer (The circle as with basepoint ).
Constant functions, the identity, finite sums, and scalar multiples are continuous on real intervals (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).
Refutation
Suppose, for contradiction, that the identity is nullhomotopic. By [A1], there are and a homotopy with and . Reverse its time coordinate to obtain , so and .
Since is surjective, choose with . The constant map lifts , so [L1] and [L2] give a lift . Define . Then is continuous and , so is the identity: is a section of .
The path is a lift of because is the identity, and it is closed because . Put by [L5]. The path is another lift of starting at , since [L4] and [L5] give ; it is continuous by [L6]. Uniqueness in [L3] forces , whose endpoint is , contradicting that is closed.
The contradiction discharges the assumption of step 1.1. Hence the identity is not nullhomotopic, and the universal claim is false.
Depends on
- Nullhomotopic maps and contractible spaces
- The circle as $S^1=\mathbb R/\mathbb Z$ with basepoint $[0]$
- $p:\mathbb R\to\mathbb R/\mathbb Z$ is a covering map with translated interval sheets
- Existence and uniqueness of homotopy lifts through a covering map
- Existence and uniqueness of path lifts through a covering map
- The standard circle loops $\omega_n(t)=[nt]$ for $n\in\mathbb Z$
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
37 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, Ch. 1, Section 1.1 (standard reference, not scraped)
- J. Peter May, A Concise Course in Algebraic Topology, Ch. 1, Section 5 (standard reference, not scraped)