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 mod-two degree is well defined and homotopy invariant

Statement

Assume ${A C}_{ω}$ . Let $M$ be a closed smooth $m$ -manifold, $m \geq 1$ , and let $f, g : M \to S^{m}$ be smooth. (i) Any two regular values $y, y^{'}$ of $f$ give the same parity $∣ f^{- 1} (y) ∣ \equiv ∣ f^{- 1} (y^{'}) ∣ (m o d 2)$ , so $\deg_{2} (f)$ is well defined. (ii) If $f$ and $g$ are homotopic, equivalently smoothly homotopic, then $\deg_{2} (f) = \deg_{2} (g)$ ; hence $\deg_{2}$ is defined on free homotopy classes of continuous maps $[M, S^{m}]$ . (iii) If $M$ is nonempty, connected and oriented then $\deg_{2} (f) \equiv \deg (f) (m o d 2)$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , a closed smooth $m$ -manifold $M$ , $m \geq 1$ , and smooth maps $f, g : M \to S^{m}$ . The source may be empty or disconnected.

[F1]

At regular values $y, y^{'}$ of a fixed map, the framed preimages using positive bases are framed cobordant (Framed regular preimages of a map to a sphere, The framed preimage class is independent of regular value and positive basis, clause (ii)).

[F2]

A framed cobordism of finite configurations is a compact $1$ -manifold with their disjoint union as its boundary, and this boundary has even cardinality (Framed cobordism of framed submanifolds, Boundary of a compact 1-manifold has even cardinality).

[F3]

Smoothly homotopic maps with a common regular value and positive basis have framed-cobordant preimages (Homotopic maps with a common regular value have framed-cobordant preimages).

[F4]

Under ${A C}_{ω}$ , critical value sets are null; finite unions of manifold-null sets are null, and their complement in a positive-dimensional manifold is dense (Morse-Sard for smooth manifolds, Countable unions and subsets of manifold null sets are null, A null set has dense complement in a positive-dimensional manifold).

[F5]

Under ${A C}_{ω}$ , every continuous map has a homotopic smooth representative, and continuously homotopic smooth maps are smoothly homotopic (Every continuous map between smooth manifolds is homotopic to a smooth map, Continuously homotopic smooth maps are smoothly homotopic, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F6]

For a nonempty connected oriented $M$ , the integer degree is the signed count of a finite regular fibre (Regular-value formula for degree, Degree of a proper smooth map by compact-support cohomology). The candidate mod-two degree is its cardinality modulo two (The mod-two degree of a map to a sphere).

Proof

1.1F1F2F4given

For any framed cobordism from $N_{0}$ to $N_{1}$ , [F2] gives $∣ N_{0} ∣ + ∣ N_{1} ∣$ even, hence equal parities. This uses no orientability or connectedness of the ambient $M$ . Applying it to the cobordism of [F1] proves independence of the supplied regular value and positive basis. Existence of a regular value follows from [F4], since $S^{m}$ is nonempty and positive-dimensional. For empty $M$ every fibre is empty and the degree is $0$ .

2.1F2F3F4step 1.1

If $f$ and $g$ are smoothly homotopic, use [F4] to choose $y$ outside the union of their two critical value sets. Then $y$ is regular for both endpoint maps; no regularity assertion about an arbitrary homotopy at its boundary is required. Fix a positive basis at $y$ and apply [F3]. By [F2] the two fibres have equal parity, and step 1.1 identifies these parities with $\deg_{2} (f)$ and $\deg_{2} (g)$ .

3.1F5step 2.1

For a continuous map define $\deg_{2}$ using any smooth representative supplied by [F5]. Two choices are continuously homotopic and hence smoothly homotopic by [F5], so step 2.1 proves independence. The same argument proves invariance under a continuous homotopy. Thus the degree is defined on $[M, S^{m}]$ , including empty and disconnected sources.

4.1F6step 1.1algebra∎

If $M$ is nonempty, connected and oriented, [F6] expresses $\deg (f)$ as a sum of local signs $\pm 1$ . Each sign is $1$ modulo two, so reducing that sum gives $∣ f^{- 1} (y) ∣ m o d 2 = \deg_{2} (f)$ . This proves (iii) within the domain of the cited integer-degree definition.

Depends on

Used by

Cited to discharge well-definedness by The mod-two degree of a map to a sphere.

Dependency tree · two levels

77 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)
Victor Guillemin and Alan Pollack, Differential Topology (standard reference, not scraped)