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.

Stable splitting of the tangent bundle of the Milnor disk bundle

Statement

Assume the Axiom of Choice as inherited from the connection and Pontryagin-class suppliers. Let $ξ = ξ_{h, j} \to S^{4}$ be the quaternionic clutching bundle, $W = D (ξ_{h, j})$ its disk bundle and $π : W \to S^{4}$ the projection. Then $T W \oplus ε^{1} ≅ π^{*} (ξ_{h, j} \oplus ε^{5}), p_{1} (T W) = 2 (h - j) π^{*} u \in H^{4} (W; Z) .$

Facts & Assumptions

Given: The clutchings $ξ = ξ_{h, j}$ , the disk bundle $W = D (ξ)$ with projection $π$ , and the generator $u \in H^{4} (S^{4}; Z)$ .

[A1]

The Axiom of Choice is assumed (The Axiom of Choice).

[L1]

The vertical tangent bundle of a smooth vector bundle total space is the pullback of the bundle along the projection; restricting to the disk bundle and splitting the tangent sequence by a connection gives $T W ≅ π^{*} (T S^{4} \oplus ξ)$ (Every smooth vector bundle admits a connection, The Milnor sphere and disk bundles $M_{h, j}$ and $W_{h, j}$ ).

[L2]

The explicit map $(v, t) \mapsto v + t b$ at a base point of the unit sphere identifies $T S^{4} \oplus ε^{1}$ with the trivial rank-five bundle $ε^{5}$ (the unit sphere lies in $R^{5}$ with outward normal $b$ ).

[L3]

Assume AC. Pontryagin classes are natural and stable on CW bases (Naturality, stability, and mod-two reduction of Pontryagin classes). On a CW-type base they are defined by transport along a homotopy equivalence (Pontryagin classes by complexification); homotopic pullbacks of numerable bundles are isomorphic (Homotopy invariance of vector-bundle pullback). Here the zero section $s : S^{4} \to W$ and projection $π$ are explicit homotopy inverses, using the fibre contraction. Thus $p_{1} (E) = π^{*} p_{1} (s^{*} E)$ for a bundle $E$ on $W$ , and stability can be checked on $S^{4}$ .

[L4]

$p_{1} (ξ_{h, j}) = 2 (h - j) u$ under the calibrated clutching conventions (Euler and first Pontryagin classes of $ξ_{h, j}$ ).

Proof

technique · direct

1.1L1A1given

The tangent sequence $0 \to π^{*} ξ \to T W \to π^{*} T S^{4} \to 0$ is split by the horizontal lifts of a smooth connection on $ξ$ , so $T W ≅ π^{*} (T S^{4} \oplus ξ)$ .

2.1step 1.1L2

The map $(v, t) \mapsto v + t b$ identifies $T S^{4} \oplus ε^{1}$ with $ε^{5}$ , so adding a trivial line to both sides of step 1.1 gives $T W \oplus ε^{1} ≅ π^{*} (T S^{4} \oplus ξ) \oplus ε^{1} ≅ π^{*} ((T S^{4} \oplus ε^{1}) \oplus ξ) ≅ π^{*} (ξ \oplus ε^{5})$ , the first assertion.

3.1step 2.1L3L4∎

Pulling the stable splitting of step 2.1 back along the zero section gives $s^{*} T W \oplus ε^{1} ≅ ξ \oplus ε^{5}$ on the actual CW sphere. By [L3] and [L4], $p_{1} (s^{*} T W) = p_{1} (ξ) = 2 (h - j) u$ . Transporting back through the explicit homotopy equivalence gives $p_{1} (T W) = π^{*} p_{1} (s^{*} T W) = 2 (h - j) π^{*} u$ .

Depends on

Used by

Relative Pontryagin square of the Milnor disk bundle Lemma

Dependency tree · two levels

34 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, On Manifolds Homeomorphic to the 7-Sphere, Annals of Mathematics 64 (1956), 399-405 (standard reference, not scraped)
Allen Hatcher, Vector Bundles & K-Theory, section 3.2 (the tangent bundle of a vector bundle and stability) (standard reference, not scraped)