LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 boundary stable tangent bundle splits off a trivial line

Statement

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used exactly through the global inward vector field of A global inward-pointing boundary vector field exists. Let $W$ be a smooth manifold with boundary $M = \partial W$ (Smooth maps between manifolds with boundary), let $i : M \to W$ be the inclusion, which is a closed embedding of a smooth $n$ -manifold (The boundary of a positive-dimensional manifold is a closed embedded smooth (n-1)-manifold), and let $X$ be a smooth vector field on a neighbourhood of $M$ in $W$ that is inward at every point of $M$ (Inward, outward, and boundary-tangent vectors).

Then the map $Φ : T M \oplus ε^{1} ⟶ T W ∣_{M}, Φ (v, t) = d i (v) + t X ∣_{M},$ is an isomorphism of smooth real vector bundles over $M$ (Whitney sum, tensor, dual, Hom, and exterior-power bundles, Pullback vector bundles and sections). Consequently $T W ∣_{M} ≅ T M \oplus ε^{1}$ and the normal line $T W ∣_{M} / T M$ is trivial. Since ${A C}_{ω}$ supplies such an $X$ for every smooth manifold with boundary, the splitting holds for every smooth manifold with boundary. In particular the stabilization of $T M$ by one trivial line is identified with the restriction $T W ∣_{M}$ ; this is the identification used by the characteristic number propositions of this page.

Facts & Assumptions

Given: A smooth manifold $W$ with boundary $M = \partial W$ , the inclusion $i : M \to W$ , a neighbourhood of $M$ carrying a smooth vector field $X$ inward along $M$ , and the map $Φ : T M \oplus ε^{1} \to T W ∣_{M}$ , $Φ (v, t) = d i (v) + t X$ . Countable choice ${A C}_{ω}$ is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

A vector at $p \in \partial W$ is inward when its last coordinate in a boundary chart is positive, outward when negative, and boundary-tangent when zero; the alternatives are chart independent (Inward, outward, and boundary-tangent vectors).

[F2]

For $p \in M$ the differential $d i_{p}$ identifies $T_{p} M$ with the boundary-tangent hyperplane of $T_{p} W$ (The boundary tangent space is the boundary-tangent hyperplane).

[F3]

Here $T W ∣_{M}$ denotes the pullback $i^{*} T W$ , not restriction to an open subset (Pullback vector bundles and sections). In a boundary chart, the tangent-bundle trivialization restricts to its face and the bundle transitions are the ambient tangent transitions restricted to that face; they are smooth, so this gives a smooth bundle over $M$ (Tangent and cotangent bundles extend over a boundary). The inclusion differential and restricted section are smooth in these charts. With the Whitney sum and trivial line bundle, $Φ$ is therefore a smooth fibrewise-linear bundle map (Whitney sum, tensor, dual, Hom, and exterior-power bundles, Smooth vector bundles, rank, fibres, and trivial bundles).

[F4]

A smooth vector bundle map over a diffeomorphism whose fibre maps are bijective is a vector bundle isomorphism (A fibrewise bijective smooth bundle map over a diffeomorphism is a bundle isomorphism).

[F5]

Assuming ${A C}_{ω}$ , every smooth manifold with boundary admits a smooth vector field on a neighbourhood of its boundary that is inward at every boundary point (A global inward-pointing boundary vector field exists).

Proof

1.1F3

( $Φ$ is a smooth bundle map.) The differential $d i : T M \to i^{*} T W$ is a smooth bundle map and $X ∣_{M}$ is a smooth section by [F3], and the trivial line bundle is smooth; forming sums and scalar multiples fibrewise, $Φ (v, t) = d i (v) + t X ∣_{M}$ is a smooth map of total spaces whose restriction to each fibre is linear and whose base map is the identity.

1.2F1F2

(Fibrewise bijectivity.) Fix $p \in M$ . By [F2], $d i_{p}$ is injective with image the boundary-tangent hyperplane $H_{p} \subseteq T_{p} W$ , a linear subspace of dimension $n = \dim M$ . By [F1], $X (p)$ is inward at $p$ , so its last boundary-chart coordinate is positive and $X (p) \neq 0$ ; in particular $X (p) \notin H_{p}$ , since elements of $H_{p}$ have last coordinate zero. Hence $H_{p} \cap R X (p) = {0}$ , and $\dim H_{p} + 1 = n + 1 = \dim T_{p} W$ gives $T_{p} W = H_{p} \oplus R X (p)$ . Therefore $Φ_{p} : H_{p} \oplus R \to T_{p} W$ , $(v, t) \mapsto v + t X (p)$ , is a linear isomorphism.

2.1F4step 1.1step 1.2

( $Φ$ is a bundle isomorphism.) The base map of $Φ$ is the identity, a diffeomorphism, and by step 1.2 every fibre map $Φ_{p}$ is bijective; step 1.1 makes $Φ$ a smooth bundle map. By [F4], $Φ$ is an isomorphism of smooth vector bundles. Hence $T W ∣_{M} ≅ T M \oplus ε^{1}$ . Moreover $Φ$ carries the subbundle $0 \oplus ε^{1}$ isomorphically onto a line subbundle complementary to $d i (T M)$ ; composing with the quotient projection identifies $ε^{1}$ with $T W ∣_{M} / d i (T M)$ , so the normal line $T W ∣_{M} / T M$ is trivial and is spanned by $X ∣_{M}$ .

3.1F5step 2.1∎

(Every manifold with boundary; assembly.) Let $N$ be an arbitrary smooth manifold with boundary. By [F5] there is, under ${A C}_{ω}$ , a smooth vector field on a neighbourhood of $\partial N$ inward at every boundary point, and steps 1.1–2.1 apply to it; hence $T (\partial N) \oplus ε^{1} ≅ T N ∣_{\partial N}$ for every smooth manifold with boundary $N$ . Applied to $N = W$ this is the asserted splitting, and it identifies the stabilization of $T M$ by one trivial line with $T W ∣_{M}$ . The argument used ${A C}_{ω}$ only in the selection of the inward field in [F5]; no other choice is made.

Depends on

Used by

Boundaries have zero Stiefel-Whitney numbers Proposition
Oriented boundaries have zero Pontryagin numbers Proposition

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

John Milnor and James Stasheff, Characteristic Classes (original pagination) (standard reference, not scraped)
C. T. C. Wall, Differential Topology (Cambridge Studies in Advanced Mathematics 156, 2016) (standard reference, not scraped)