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.
There is no retraction of the closed disk onto the unit circle
Statement
Write and (Euclidean spheres and closed balls as subspaces of ). There is no continuous retraction from the closed unit disk onto the unit circle .
Facts & Assumptions
Given: The closed unit disk , the unit circle , the common basepoint , and the inclusion .
If is a retract of , then the inclusion induces an injective homomorphism on fundamental groups at every basepoint of (A retract induces an injection on fundamental groups, and a deformation retract induces an isomorphism).
The closed unit disk and unit circle are respectively the Euclidean closed ball and Euclidean sphere (Euclidean spheres and closed balls as subspaces of ).
Every nonempty convex subset of is simply connected (Every nonempty convex subset of is simply connected).
For the geometric unit circle based at , (The trigonometric loops give ).
The Euclidean norm is a norm on , so it is absolutely homogeneous and satisfies the triangle inequality (Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation).
Proof
The disk is nonempty and convex: if and , then . Hence has one element.
The unit circle has isomorphic to the nontrivial group .
Suppose a retraction existed.
By [L1], would be injective, but steps 1.1 and 1.2 make this a homomorphism from a nontrivial group to a one-element group, which cannot be injective. Thus no such retraction exists.
Depends on
- A retract induces an injection on fundamental groups, and a deformation retract induces an isomorphism
- Euclidean spheres and closed balls as subspaces of $\mathbb{R}^n$
- Every nonempty convex subset of $\mathbb R^n$ is simply connected
- The trigonometric loops give $\pi_1(\{(x,y):x^2+y^2=1\},(1,0))\cong\mathbb Z$
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
Used by
Dependency tree · two levels
31 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, proof of Theorem 1.9 (standard reference, not scraped)
- J. Peter May, A Concise Course in Algebraic Topology, Chapter 1, §6 (standard reference, not scraped)