TheoremStatement: Literature-sourcedProof: 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.

The oriented intersection number is homotopy invariant

Statement

Assume ${A C}_{ω}$ . Let $X$ be a compact oriented smooth manifold without boundary, $M$ an oriented smooth $n$ -manifold without boundary, and $Z \subseteq M$ a closed oriented embedded submanifold with $\dim X + \dim Z = n$ . Let $F : [0, 1] \times X \to M$ be a smooth family transverse to $Z$ , including on the boundary faces. Then the endpoint slice maps $F_{0}, F_{1}$ are transverse to $Z$ and $I (F_{0}, Z) = I (F_{1}, Z),$ with the oriented intersection number of The oriented intersection number. Consequently $I (\cdot, Z)$ is well defined on homotopy classes of smooth maps $X \to M$ : any two transverse maps in the same homotopy class give the same number, and the definition extends to all smooth maps. Compactness of the source and closedness of $Z$ ensure a compact trace; compactness of $M$ is unnecessary; the safe proper extension is recorded in the remark on properness later on this page.

Facts & Assumptions

Given: Oriented $X, M, Z$ with $\dim X + \dim Z = \dim M$ , a smooth family $F : [0, 1] \times X \to M$ transverse to $Z$ including on the faces, and ${A C}_{ω}$ for the extension clause.

[F1]

$W : = F^{- 1} (Z)$ is a compact oriented $1$ -manifold with boundary $F_{0}^{- 1} (Z) ⊔ F_{1}^{- 1} (Z)$ , neat in $[0, 1] \times X$ , and the slices $F_{0}, F_{1}$ are transverse to $Z$ (Transverse preimages for maps from manifolds with boundary, Smooth families of maps and their evaluation maps).

[F2]

With the preimage orientation, the boundary signs of $W$ satisfy $\sum_{p \in \partial W} ε_{W} (p) = I (F_{1}, Z) - I (F_{0}, Z)$ (Oriented boundary of an intersection trace has opposite end signs, Preimage orientation agrees with the local intersection sign).

[F3]

The signed boundary sum of a compact oriented $1$ -manifold vanishes (Oriented boundary counts of a compact oriented 1-manifold cancel); its boundary also has even cardinality (Boundary of a compact 1-manifold has even cardinality).

[F4]

$I (f, Z)$ is the finite sum of the local signs over a transverse representative, and the definition on arbitrary smooth maps uses a transverse homotopic representative (The oriented intersection number).

[F5]

Under ${A C}_{ω}$ , a smooth map is homotopic to a transverse one (The transversality homotopy theorem). A homotopy between transverse endpoints can be smoothed and made transverse with its endpoints fixed by the end-collar construction in step 3.1 of The mod 2 intersection number is homotopy invariant, and its explicit parameter-cutoff argument (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct; the trace's signed boundary count is computed twice

1.1F1F4given

By [F1] the trace $W$ is a compact oriented $1$ -manifold with boundary the disjoint union of the finite sets $F_{0}^{- 1} (Z)$ and $F_{1}^{- 1} (Z)$ , and the endpoint slice maps $F_{0}, F_{1}$ are transverse to $Z$ , so $I (F_{0}, Z)$ and $I (F_{1}, Z)$ are defined by [F4].

2.1F2F3step 1.1algebra

By [F2] the sum of the outward-normal-first boundary signs of $W$ equals $I (F_{1}, Z) - I (F_{0}, Z)$ ; by [F3] that sum vanishes, because $W$ is a compact oriented $1$ -manifold. Hence $I (F_{1}, Z) = I (F_{0}, Z)$ .

3.1F2F3F4F5step 2.1choose∎

For the extension to arbitrary smooth maps, let $g_{0}, g_{1} : X \to M$ be transverse and homotopic; use the end-collar construction of [F5] to obtain a transverse homotopy fixed at those endpoints. Applying 2.1 to that trace gives $I (g_{0}, Z) = I (g_{1}, Z)$ whenever both are transverse; for an arbitrary smooth map one chooses a transverse representative by [F5], and the value is independent of the choice by the previous sentence, so the definition of [F4] is well posed on homotopy classes. Countable Choice is inherited through the classification and used for the approximation suppliers; the finite determinant and sum computations add no choice.

Depends on

Used by

The oriented intersection number reduces to the mod 2 number Corollary
Geometric cardinality is not homotopy invariant Counterexample
Noncompact intersections can escape during a homotopy Counterexample
Properness can replace compactness only when the intersection trace is compact Remark
Intersection number under factor interchange Theorem

Cited to discharge well-definedness by The oriented intersection number.

Dependency tree · two levels

52 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)
John Milnor, Topology from the Differentiable Viewpoint (Princeton University Press; complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)