ExampleConstruction: Literature-sourcedVerification: 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 standard sphere immersion and its normal line

Example

Let $j : S^{2} ↪ R^{3}$ be the standard unit sphere inclusion. Then $(j, d j)$ is a formal immersion, and the normal bundle of the formal immersion is $ν_{d j} = d j (T S^{2})^{⊥}$ , the fibrewise orthogonal complement of the tangent planes of $S^{2}$ in $j^{*} T R^{3}$ . The outward unit normal $N (x) = x$ is a global nonvanishing section, so $ν_{d j} ≅ ε^{1}$ is trivial, and the tangent-normal identity gives $T S^{2} \oplus ε^{1} ≅ j^{*} T R^{3} = ε^{3},$ the standard trivialization of the tangent bundle of $S^{2}$ stabilised by one trivial line. The bundle isomorphism $(v, a) \mapsto v + a x$ therefore trivializes $T S^{2} \oplus ε^{1}$ ; the inverse images of the standard basis vectors $e_{i}$ give the global frame $x \mapsto (e_{i} - ⟨ e_{i}, x ⟩ x, ⟨ e_{i}, x ⟩)$ , $i = 1, 2, 3$ , while $T S^{2}$ alone admits no nowhere-zero global section by A positive even sphere has no nowhere-zero tangent field; hence the extra normal line is essential and the splitting is not a triviality of $T S^{2}$ . This verifies the tangent-normal identity in the first nontrivial even-dimensional case and provides the normal line used in the sphere-eversion computation on the next page.

Facts & Assumptions

Given: The standard unit sphere inclusion $j : S^{2} ↪ R^{3}$ and the standard structures on $T R^{3} ≅ R^{3} \times R^{3}$ (The tangent bundle as a disjoint union).

[F1]

$(j, d j)$ is a formal immersion whose fibres are injective, and the normal bundle of the formal immersion is $ν_{d j} = d j (T S^{2})^{⊥}$ , the orthogonal complement with respect to the standard metric (Formal immersion between smooth manifolds, Normal bundle of a formal immersion).

[L1]

The tangent-normal identity gives a smooth bundle isomorphism $T S^{2} \oplus ν_{d j} ≅ j^{*} T R^{3}$ (Formal immersion gives the tangent normal-bundle identity), and $j^{*} T R^{3} ≅ ε^{3}$ is the trivial rank-three bundle (Smooth vector bundles, rank, fibres, and trivial bundles).

Verification

technique · direct

1.1F1givenalgebra

For $x \in S^{2}$ the tangent space $T_{x} S^{2}$ is the orthogonal complement of the radial line $R x$ in $R^{3}$ , and $d j_{x}$ is the inclusion $T_{x} S^{2} ↪ R^{3}$ . Hence the normal line of $d j$ at $x$ is spanned by $x$ , and the outward unit normal $N (x) : = x$ is a global smooth nonvanishing section of $ν_{d j}$ .

2.1L1step 1.1∎

A line bundle with a global nonvanishing section is trivial, so $ν_{d j} ≅ ε^{1}$ ; the tangent-normal identity of [L1] then gives $T S^{2} \oplus ε^{1} ≅ j^{*} T R^{3} = ε^{3}$ , and the isomorphism $(v, a) \mapsto v + a x$ pulls back the standard basis to the three smooth sections $(e_{i} - ⟨ e_{i}, x ⟩ x, ⟨ e_{i}, x ⟩)$ , which are a global frame because their images are a basis in every fibre.

Remarks

The failure of a nowhere-zero section of $T S^{2}$ is proved by the identity-to-antipodal homotopy obstruction in A positive even sphere has no nowhere-zero tangent field. The explicit normal-line verification above and that obstruction together distinguish stable triviality from triviality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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, Bundles, Manifolds, and Homotopy, Ch. 7 §2 “Obstructions to the existence of embeddings and immersions, the Hirsch–Smale theorem”, printed pp. 226–232 (Theorem 7.5, Corollary 7.6) (standard reference, not scraped)
Andrew Ranicki, Algebraic and Geometric Surgery, Ch. 7 §7.4 “The Smale–Hirsch classification of immersions”, printed pp. 142–146 (Theorem 7.35, Proposition 7.39) (standard reference, not scraped)