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.
Rotations of the two-sphere and their Lefschetz number
Example
Assume AC (The Axiom of Choice). Let be a rotation of the unit sphere. Then (Algebraic Lefschetz number via rational homology traces). For a rotation by an angle the fixed point set is exactly the two poles, both fixed points are nondegenerate of index , and therefore (Geometric Lefschetz number (index sum), Lefschetz-Hopf index formula). For the identity (angles in ) the fixed set is the whole sphere and the geometric index sum is not defined directly, while the Lefschetz number is still , because every rotation is homotopic to the identity.
Verification
Given: A rotation of about the axis through the poles.
[F1] is in degrees and and vanishes elsewhere (Homology of spheres); the degree of an orientation-preserving diffeomorphism of is (Degree of an orientation-preserving or reversing diffeomorphism, Degree of a self map of an oriented sphere); homotopic maps have equal Lefschetz numbers and (The Lefschetz number of the identity is the Euler characteristic).
[F2] A nondegenerate fixed point has index (The index of a nondegenerate fixed point is the sign of det(I-Df)).
The Lefschetz number is . Every rotation is homotopic to the identity through rotations. Since and the other groups vanish by [F1], the trace formula gives , and homotopy invariance gives . Equivalently, is the identity on and multiplication by on , so .
The fixed points of a generic rotation. In coordinates on centred at the north pole the rotation is for ; fixed points solve , so , and near the south pole the same computation in the chart shows that only the south pole is fixed. At each pole the displacement has invertible differential , so both fixed points are nondegenerate and by [F2] each has index (the linear map is a positive multiple of a rotation). Hence , in agreement with the index formula. For the half-turn , the same two poles are the entire fixed set and on each tangent plane, so each is nondegenerate of index . For the map is the identity and fixes all of ; this fixed set is not isolated, so only the Lefschetz number is asserted directly.
Depends on
- Lefschetz-Hopf index formula
- The index of a nondegenerate fixed point is the sign of det(I-Df)
- Geometric Lefschetz number (index sum)
- Algebraic Lefschetz number via rational homology traces
- The Lefschetz number of the identity is the Euler characteristic
- Homology of spheres
- Degree of a self map of an oriented sphere
- $C^r$ and smooth maps between smooth manifolds
- The Axiom of Choice
- Degree of an orientation-preserving or reversing diffeomorphism
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
58 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
- Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall 1974; complete 236-page PDF) (standard reference, not scraped)
- Peter Wong, Lectures on Fixed Point Theory, Mini-Course XV Encontro Brasileiro de Topologia, Rio Claro 2006 (complete notes) (standard reference, not scraped)