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.

The pullback of a trivial smooth vector bundle is canonically trivial

Statement

Let $f : N \to M$ be a smooth map and let $ε_{M}^{r} = M \times R^{r}$ be the trivial smooth real rank- $r$ bundle over $M$ . Then the pullback $f^{*} ε_{M}^{r}$ is canonically isomorphic to the trivial bundle $ε_{N}^{r} = N \times R^{r}$ : the constant frame $e_{1}, \dots, e_{r}$ of $ε_{M}^{r}$ pulls back to the nowhere-zero global frame $x \mapsto (x, e_{j})$ of $f^{*} ε_{M}^{r}$ , and the isomorphism is the one determined by that frame (Local and global frames of a vector bundle, A vector bundle is trivial if and only if it has a global frame). This product-bundle assertion is choice-free.

Facts & Assumptions

Given: A smooth map $f : N \to M$ and the trivial smooth rank- $r$ real bundle $ε_{M}^{r} = M \times R^{r} \to M$ .

[F1]

The pullback set is $f^{*} ε_{M}^{r} = {(q, e) \in N \times (M \times R^{r}) : f (q) = {pr}_{1} (e)} = {(q, (f (q), v)) : q \in N, v \in R^{r}}$ , with projection $(q, (f (q), v)) \mapsto q$ and fibrewise vector-space operations inherited from $ε_{M}^{r}$ (Pullback vector bundles as fibre products, Smooth vector bundles, rank, fibres, and trivial bundles).

[F2]

The pullback carries the smooth rank- $r$ vector-bundle structure constructed in The pullback fibre product is a smooth vector bundle: for a bundle chart $Φ_{α} : E ∣_{U_{α}} \to U_{α} \times R^{r}$ of a bundle $E$ , the map $(q, e) \mapsto (q, v)$ with $Φ_{α} (e) = (f (q), v)$ is a bundle chart over $f^{- 1} (U_{α})$ ; the trivial bundle $ε_{M}^{r}$ has the single global bundle chart $Φ (p, v) = (p, v)$ over $M$ .

[F3]

A smooth rank- $r$ vector bundle is trivial if and only if it has a global frame (Local and global frames of a vector bundle, A vector bundle is trivial if and only if it has a global frame); a global frame $(s_{1}, \dots, s_{r})$ determines the bundle isomorphism $N \times R^{r} \to E$ , $(q, (λ_{1}, \dots, λ_{r})) \mapsto \sum_{j} λ_{j} s_{j} (q)$ .

[F4]

Maps into a product of smooth manifolds are smooth exactly when their components are, and smooth maps are continuous ( $C^{r}$ and smooth maps between smooth manifolds).

Proof

1.1F1F4

Define $Φ : f^{*} ε_{M}^{r} \to N \times R^{r}$ by $Φ (q, (f (q), v)) = (q, v)$ , using the description [F1]. Then $Φ$ is well defined, and its inverse is $(q, v) \mapsto (q, (f (q), v))$ . On each fibre it is the linear isomorphism onto ${q} \times R^{r}$ inverse to $v \mapsto (f (q), v)$ , and $Φ$ lies over ${id}_{N}$ . So $Φ$ is a fibrewise-linear bijection over the base.

2.1F2F4step 1.1

$Φ$ is smooth with smooth inverse. Indeed, in the global pullback chart of [F2] coming from the global chart $Φ (p, v) = (p, v)$ of $ε_{M}^{r}$ , the chart map is exactly $Φ$ , i.e. the identity identification of $N \times R^{r}$ ; and the inverse $(q, v) \mapsto (q, (f (q), v))$ has components $q \mapsto q$ , $q \mapsto f (q)$ and $v \mapsto v$ , which are smooth by [F4] since $f$ is smooth. Hence $Φ$ is a diffeomorphism, and consequently a smooth bundle isomorphism over $N$ .

3.1F2F3step 1.1step 2.1∎

Therefore $f^{*} ε_{M}^{r} ≅ ε_{N}^{r}$ as smooth vector bundles over $N$ , by the isomorphism $Φ$ , which was defined by an explicit formula using only $f$ and hence is canonical. Equivalently, the constant sections $s_{j} (p) = (p, e_{j})$ of $ε_{M}^{r}$ pull back to the sections $f^{*} s_{j} (q) = (q, (f (q), e_{j}))$ of $f^{*} ε_{M}^{r}$ , none of whose values is the zero vector; these pullbacks are smooth because in the global pullback chart of step 2.1 the section $f^{*} s_{j}$ reads as the constant map $q \mapsto e_{j}$ , and they form a global frame of $f^{*} ε_{M}^{r}$ that $Φ$ converts into the standard frame of $N \times R^{r}$ . No selection of local trivializations, complements or representatives has been made: the chart of [F2] used above is the single global chart of the product bundle, so the argument uses no choice principle. The case $r = 0$ gives the zero bundle over $N$ , and the empty or disconnected base is covered verbatim.

Depends on

Used by

Dependency tree · two levels

21 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 (author draft, complete 568-page text) (standard reference, not scraped)
Ralph L. Cohen, Immersions of Manifolds and Homotopy Theory (lecture notes, 30 June 2022; complete 46-page text) (standard reference, not scraped)