Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck pass
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 n≥1. Let f:Sn→Sn be continuous of degree d (Degree of a self map of an oriented sphere). Then L(f)=1+(−1)nd. In particular, for n=1 a circle map of degree d has L=1−d, and for n=2 every self-map of the sphere has L=1+d, so a degree-d map with d≠−1 has a fixed point by the Lefschetz fixed point theorem; for n=2 and d=−1 the antipodal map is fixed-point-free, with L=1−1=0.

Verification

Given: A continuous map f:Sn→Sn of degree d.

[F1] Hi(Sn;Q) is Q for i=0,n and vanishes otherwise (Homology of spheres); f∗ is the identity on H0 and multiplication by d on Hn (Degree of a self map of an oriented sphere).

[L1] L is the alternating trace sum over rational homology (Algebraic Lefschetz number via rational homology traces), and when f is smooth with isolated fixed points the index sum equals L on the scope of Lefschetz-Hopf index formula.

1.1givenF1L1

The trace computation. By [F1] the only nonzero rational homology groups are H0 and Hn, with f∗=id on H0 and f∗=d on Hn; the defining alternating sum therefore has exactly the two terms (−1)0tr⁡(id)=1 and (−1)nd, so L(f)=1+(−1)nd.

2.1step 1.1L1∎

Consequences. For n=1 this is 1−d, vanishing exactly for the degree-one circle maps such as rotations; for n=2 it is 1+d, and this is nonzero exactly when d≠−1, so the fixed-point theorem forces a fixed point in that case; the degree-−1 antipodal map has no fixed points and Lefschetz number 1−1=0, the standard sharpness example. When f is smooth with nondegenerate fixed points the same number is the index sum by [L1], for instance for an integer d≥2 the map z↦zd extends smoothly to S2, with the coordinate expression w↦wd at infinity. Its fixed points are 0, ∞, and the d−1 solutions of zd−1=1. The derivative is zero at 0 and infinity, and is complex multiplication by d at those roots; hence I−Df has positive real determinant at all d+1 points and every local index is +1 by The index of a nondegenerate fixed point is the sign of det(I-Df). A nonzero finite target value has d regular preimages of positive orientation, proving the asserted degree d by Regular-value formula for degree.

Depends on

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