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.
Degree-d self-maps of a sphere have Lefschetz number 1+(-1)^n d
Example
Assume AC (The Axiom of Choice) and . Let be continuous of degree (Degree of a self map of an oriented sphere). Then In particular, for a circle map of degree has , and for every self-map of the sphere has , so a degree- map with has a fixed point by the Lefschetz fixed point theorem; for and the antipodal map is fixed-point-free, with .
Verification
Given: A continuous map of degree .
[F1] is for and vanishes otherwise (Homology of spheres); is the identity on and multiplication by on (Degree of a self map of an oriented sphere).
[L1] is the alternating trace sum over rational homology (Algebraic Lefschetz number via rational homology traces), and when is smooth with isolated fixed points the index sum equals on the scope of Lefschetz-Hopf index formula.
The trace computation. By [F1] the only nonzero rational homology groups are and , with on and on ; the defining alternating sum therefore has exactly the two terms and , so .
Consequences. For this is , vanishing exactly for the degree-one circle maps such as rotations; for it is , and this is nonzero exactly when , so the fixed-point theorem forces a fixed point in that case; the degree- antipodal map has no fixed points and Lefschetz number , the standard sharpness example. When is smooth with nondegenerate fixed points the same number is the index sum by [L1], for instance for an integer the map extends smoothly to , with the coordinate expression at infinity. Its fixed points are , , and the solutions of . The derivative is zero at and infinity, and is complex multiplication by at those roots; hence has positive real determinant at all points and every local index is by The index of a nondegenerate fixed point is the sign of det(I-Df). A nonzero finite target value has regular preimages of positive orientation, proving the asserted degree by Regular-value formula for degree.
Depends on
- Algebraic Lefschetz number via rational homology traces
- Degree of a self map of an oriented sphere
- Homology of spheres
- Lefschetz-Hopf index formula
- The index of a nondegenerate fixed point is the sign of det(I-Df)
- Isolated fixed point and local fixed point index
- Geometric Lefschetz number (index sum)
- Lefschetz fixed point theorem
- Path-homotopic based circle loops have the same degree
- Regular-value formula for degree
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
71 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
- Peter Wong, Lectures on Fixed Point Theory, Mini-Course XV Encontro Brasileiro de Topologia, Rio Claro 2006 (complete notes) (standard reference, not scraped)
- Eleny Ionel, notes by Andrew Lin, Stanford Math 215B Differential Topology, Winter 2023 (complete 63-page lecture notes) (standard reference, not scraped)