TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Global sphere degree is the sum of local degrees

Statement

Let $f : S^{n} \to S^{n}$ be continuous, $n \geq 1$ , with source and target orientations fixed. If $f^{- 1} (y)$ is finite, then $\deg (f) = \sum_{x \in f^{- 1} (y)} \deg_{x} f .$ The sum over an empty fibre is $0$ .

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

For $n \geq 1$ , $H_{n} (S^{n}, S^{n} ∖ {x}; Z) ≅ Z$ , with generator the restriction of the global sphere orientation. The local degree in def-local-degree-at-an-isolated-preimage is independent of shrinking its neighborhood. For every finite nonempty $F \subset S^{n}$ , $H_{n} (S^{n}, S^{n} ∖ F; Z) ≅ ⨁_{x \in F} H_{n} (S^{n}, S^{n} ∖ {x}; Z),$ and the global orientation maps to the tuple of local orientation generators. (Local sphere orientations and finite puncture excision)

[F2]

A continuous map between oriented $n$ -spheres, $n \geq 1$ , whose degree is nonzero must be surjective. (A map of nonzero degree between spheres is surjective)

Proof

1.1F2

If the fibre is empty, $f$ omits a point, so its degree is zero by F2. This equals the empty sum.

1.2F1

For a nonempty finite fibre $F$ , use the global-to-relative maps for $(S^{n}, S^{n} ∖ F)$ and $(S^{n}, S^{n} ∖ {y})$ . Functoriality makes the square with $f$ commute. By F1, the source global generator maps to $(1)_{x \in F}$ and the target global generator maps to $1$ .

2.1F1step 1.2algebra∎

On the summand indexed by $x$ , the lower map in this square is multiplication by $\deg_{x} f$ , by the local definition and excision. Its value on the diagonal is the sum of these integers. The other route through the square gives $\deg (f)$ , proving the formula, also for a singleton fibre.

Depends on

Used by

Degree zero does not imply a sphere map is constant Counterexample
Degree of the circle power map Example
Local degrees of a polynomial map on the riemann sphere Example
Mapping cone of a degree d circle map Example
Handle boundary coefficients are attaching-belt intersection numbers Lemma
Handle slides act by elementary basis change on handle chains Lemma
Real projective space cellular homology and the pinch map Lemma
Elementary matrix operations are realized by handle slides Proposition
Every integer occurs as the degree of a sphere map Proposition
Based sphere maps are classified by degree Theorem
Compactness of the normalized K-quasiconformal self-maps of the sphere Theorem

Dependency tree · two levels

11 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

Hatcher, Algebraic Topology, Proposition 2.30, p.136 (standard reference, not scraped)