LemmaStatement: 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.

An immersion into R^n gives a rank-(n-m) representative of the stable normal bundle

Statement

Assume ${A C}_{ω}$ . Let $f : M^{m} ↬ R^{n}$ be a smooth immersion of a closed smooth $m$ -manifold with $n > m$ , so that $(f, d f)$ is a formal immersion and $ν_{f} = f^{*} T R^{n} / d f (T M)$ is its normal bundle of rank $n - m$ (Formal immersion between smooth manifolds, Normal bundle of a formal immersion). Then the splitting of the tangent-normal sequence of Formal immersion gives the tangent normal-bundle identity gives a smooth bundle isomorphism $T M \oplus ν_{f} \to f^{*} T R^{n}$ , which under the canonical trivialization $f^{*} T R^{n} ≅ ε^{n}$ becomes a smooth isomorphism $φ : T M \oplus ν_{f} \to ε^{n}$ . Hence $(ν_{f}, φ)$ is a rank- $(n - m)$ stable normal inverse of $M$ in the sense of Stable normal inverse of the tangent bundle: an immersion of codimension $n - m$ supplies an actual rank- $(n - m)$ representative of the inverse normal class, not merely a stable one. The choice hypothesis is inherited from the bundle-metric splitting in the normal-bundle construction.

Facts & Assumptions

Given: A smooth immersion $f : M^{m} ↬ R^{n}$ of a closed smooth $m$ -manifold with $n > m$ , and countable choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

A smooth map $f$ is an immersion exactly when $(f, d f)$ is a formal immersion; a formal immersion from $M^{m}$ to $N^{n}$ is a smooth map together with a fibrewise injective smooth bundle map over it, and, when $M$ is nonempty, necessarily $m \leq n$ (Immersions, submersions, and constant-rank maps, Formal immersion between smooth manifolds).

[F2]

For a formal immersion $(f, F)$ from $M^{m}$ to $N^{n}$ , the normal bundle $ν_{F} = f^{*} T N / F (T M)$ is a smooth quotient bundle of rank $n - m$ over $M$ when $m \leq n$ ; if $M = \emptyset$ and $m > n$ , it is the empty rank-zero bundle; it is intrinsic up to canonical isomorphism, and for $(f, F) = (f, d f)$ with $f$ a genuine immersion it is the normal bundle of the immersion (Normal bundle of a formal immersion).

[F3]

For every formal immersion $(f, F)$ the quotient map fits into the short exact sequence of smooth bundles $0 \to T M \overset{F}{\to} f^{*} T N \to ν_{F} \to 0$ over $M$ , which splits: a smooth complement of $F (T M)$ restricts to an isomorphism onto $ν_{F}$ and yields a smooth bundle isomorphism $T M \oplus ν_{F} \to f^{*} T N$ restricting to $F$ on the tangent summand. If a smooth bundle metric on $f^{*} T N$ is chosen, the orthogonal complement $F (T M)^{⊥}$ is a canonical complement for that metric (Formal immersion gives the tangent normal-bundle identity). The splitting in the general case uses the metric and inherits ${A C}_{ω}$ .

[F4]

Under ${A C}_{ω}$ the identity chart of $R^{n}$ is a global smooth chart, so its induced tangent-bundle chart trivializes the Euclidean tangent bundle, $T R^{n} ≅ ε_{R^{n}}^{n}$ ; pulling this trivialization back along $f$ and applying the choice-free product-pullback lemma gives the canonical trivialization $f^{*} T R^{n} ≅ f^{*} ε_{R^{n}}^{n} ≅ ε^{n}$ (Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure, The induced tangent bundle chart, The pullback of a trivial smooth vector bundle is canonically trivial).

[F5]

A stable normal inverse of $M$ is a pair $(ν, φ)$ with $ν \to M$ a smooth real vector bundle of finite rank $k$ and $φ : T M \oplus ν \to ε^{m + k}$ a smooth bundle isomorphism; a rank- $k$ stable normal inverse is one with $rank ν = k$ (Stable normal inverse of the tangent bundle).

Proof

1.1F1F2

Since $f$ is an immersion, $(f, d f)$ is a formal immersion from $M^{m}$ to $R^{n}$ by [F1]; in particular $d f : T M \to f^{*} T R^{n}$ is fibrewise injective. By [F2] its normal bundle $ν_{f} = f^{*} T R^{n} / d f (T M)$ is a smooth real vector bundle over $M$ of rank $n - m$ .

1.2F2F3

By [F3] the quotient sequence $0 \to T M \overset{d f}{\to} f^{*} T R^{n} \to ν_{f} \to 0$ splits: the tangent-normal sequence admits a smooth bundle isomorphism $s : T M \oplus ν_{f} ⟶ f^{*} T R^{n}$ restricting to $d f$ on the tangent summand. The splitting uses a smooth bundle metric on the pullback bundle (whose existence is the countable-choice input of that lemma), so this step uses exactly the hypothesis ${A C}_{ω}$ and no more.

2.1F3F4step 1.2

Compose the splitting $s$ with the canonical trivialization $t : f^{*} T R^{n} \to ε^{n}$ supplied by [F4], which exists because the identity chart of $R^{n}$ trivializes $T R^{n}$ and the product-pullback lemma trivializes its pullback along $f$ : $φ : = t \circ s : T M \oplus ν_{f} ⟶ ε^{n}$ is a smooth bundle isomorphism, the composite of two smooth bundle isomorphisms.

3.1F3F4F5step 1.1step 1.2step 2.1∎

By step 1.1 the bundle $ν_{f}$ has rank $n - m$ and by step 2.1 the isomorphism $φ$ maps $T M \oplus ν_{f}$ onto $ε^{n} = ε^{m + (n - m)}$ ; so $(ν_{f}, φ)$ is a rank- $(n - m)$ stable normal inverse of $M$ in the sense of [F5]. Thus an immersion of codimension $n - m$ provides an actual rank- $(n - m)$ inverse bundle, not merely a stable one; nothing beyond this rank and the isomorphism is asserted about $ν_{f}$ . The countable-choice hypothesis is the one inherited from the metric splitting of [F3] and from the canonical trivialization [F4]; no bundle metric, complement or frame is chosen in addition to those data.

Depends on

Used by

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

Ralph L. Cohen, Immersions of Manifolds and Homotopy Theory (lecture notes, 30 June 2022; complete 46-page text) (standard reference, not scraped)
Ralph L. Cohen, Bundles, Manifolds, and Homotopy (author draft, complete 568-page text) (standard reference, not scraped)
John W. Milnor and James D. Stasheff, Characteristic Classes (Annals of Mathematics Studies 74, Princeton University Press; complete text) (standard reference, not scraped)