LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

The signed preimage count equals the degree

Statement

Assume ${A C}_{ω}$ . Let $M$ be a nonempty closed connected oriented smooth $m$ -manifold, $m \geq 1$ , let $f : M \to S^{m}$ be smooth, $y \in S^{m}$ a regular value and $b$ a positive basis of $T_{y} S^{m}$ . Then the framed regular preimage $(f^{- 1} (y), f_{*} b)$ has signed count $\sum_{x \in f^{- 1} (y)} ε (x) = \deg (f)$ , the compact-support degree of $f$ ; equivalently $ε (x) = sgn (d f_{x})$ at every $x \in f^{- 1} (y)$ . No new definition of degree is introduced.

Facts & Assumptions

Given: A nonempty closed connected oriented smooth $m$ -manifold $M$ , a smooth map $f : M \to S^{m}$ , a regular value $y$ and a positive basis $b$ of $T_{y} S^{m}$ (Degree of a proper smooth map by compact-support cohomology, Regular and critical points and values).

[F1]

Writing $β$ for the coordinate isomorphism determined by $b$ , the framed regular preimage $(f^{- 1} (y), f_{*} b)$ is a closed framed $0$ -dimensional submanifold of $M$ whose framing at $x$ is $f_{*} b = β \circ d f_{x} : ν (x) = T_{x} M \to T_{y} S^{m} \to R^{m}$ (Framed regular preimages of a map to a sphere, The framing sign of a zero-dimensional regular preimage, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

The framing sign of $x \in f^{- 1} (y)$ equals the local orientation sign $sgn (d f_{x})$ , because its coordinate isomorphism $β$ carries the orientation of $T_{y} S^{m}$ to the standard orientation of $R^{m}$ (The framing sign of a zero-dimensional regular preimage, Local orientation sign of a regular preimage, Orientation of a finite-dimensional real vector space).

[F3]

For a proper smooth map between nonempty connected oriented boundaryless manifolds and a regular value $y$ , the fibre is finite and $\deg (f) = \sum_{x \in f^{- 1} (y)} sgn (d f_{x})$ , and $f$ is proper here because $M$ is compact (Regular-value formula for degree, Degree of a proper smooth map by compact-support cohomology).

Proof

technique · direct

1.1F1given

For $x \in f^{- 1} (y)$ the normal quotient $ν (x) = T_{x} M / T_{x} {x} = T_{x} M$ is identified with $T_{x} M$ , and the differential $d f_{x} : T_{x} M \to T_{y} S^{m}$ is an isomorphism because $y$ is a regular value of an equidimensional map; the induced framing is the composite $β \circ d f_{x}$ , by [F1], where $β : T_{y} S^{m} \to R^{m}$ sends the positive basis $b$ to the standard basis.

2.1F2F3step 1.1algebra

Since $b$ is a positive basis, [F2] gives $ε (x) = sgn (d f_{x})$ for every $x$ of the fibre, and the fibre is finite; summing and applying the regular value formula of [F3] to the proper map $f$ gives $\sum_{x \in f^{- 1} (y)} ε (x) = \sum_{x \in f^{- 1} (y)} sgn (d f_{x}) = \deg (f)$ .

3.1F3step 2.1∎

Hence the signed count of the framed regular preimage is exactly the compact-support degree of the original map, with no new definition of degree and no use of an orientation of $S^{m}$ beyond the fixed positive basis.

Depends on

Used by

The Hopf degree theorem for oriented domains Theorem

Dependency tree · two levels

41 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

Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (standard reference, not scraped)