TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-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.

Dual and Hom transition functions define smooth bundles

Statement

If $E \to M$ and $F \to M$ are smooth vector bundles, then $E^{*} \to M$ and $Hom (E, F) \to M$ are smooth vector bundles. In local bundle charts, the dual transition matrices are $(g_{β α}^{- 1})^{T}$ and the Hom transition matrices are $A \mapsto h_{β α} A g_{β α}^{- 1}$ .

Facts & Assumptions

Given: Smooth vector bundles $E \to M$ and $F \to M$ with local transition matrices $g_{β α}$ and $h_{β α}$ .

[L1]

Vector bundle chart changes are fibrewise linear and smooth (Vector bundle charts and transition functions).

[L2]

The matrix of the transpose linear map is the transpose matrix (In dual bases, the matrix of $T^{*}$ is the transpose of the matrix of $T$ ).

[L3]

Finite products of second-countable spaces are second countable, and subspaces inherit second countability (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A product of two at most countable sets is at most countable, Second countability is hereditary).

[L4]

An open surjection has the quotient topology on its target (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps).

[L5]

Inversion is smooth on the open set of invertible matrices (Matrix inversion preserves $C^{k}$ regularity where the determinant is nonzero).

Proof

technique · direct

1.1givenL3construct

Put $A = E$ and $B = F$ , of ranks $r, s$ . For $r, s > 0$ , let $D \subseteq A^{r} \times B^{r}$ consist of tuples $(a_{1}, \dots, a_{r}, b_{1}, \dots, b_{r})$ over a common base point $p$ , with $(a_{i})$ a basis of $A_{p}$ . Give $D$ the finite-product subspace topology. It is second countable: choose one countable base of each supplied total space, take finite product boxes, and restrict them to $D$ . Only finitely many bases are chosen, and [L3] makes the resulting family countable.

2.1step 1.1L4L5construct

Let $H = ∐_{p \in M} Hom (A_{p}, B_{p})$ as a set. Send a tuple in $D$ to the unique fibre map taking $a_{i}$ to $b_{i}$ . This map $q : D \to H$ is onto: a basis can be chosen for each one fibre without selecting bases for all fibres simultaneously. Give $H$ the quotient topology. On a common local trivialization over $U$ , the open saturated set $D_{U}$ has coordinates $(p, C, V) \in U \times G L (r, R) \times M_{s \times r} (R)$ , and the composite of $q$ with the proposed Hom matrix chart is $(p, C, V) \mapsto (p, V C^{- 1})$ . This is a continuous open surjection: $(p, C, V) \mapsto (p, C, V C^{- 1})$ is a homeomorphism by [L5], followed by the open product projection. By [L4], the induced chart $H_{U} \to U \times M_{s \times r} (R)$ is a homeomorphism and $H_{U}$ is open.

3.1step 1.1step 2.1L3

The map $q$ is globally open because its restriction over every such open $H_{U}$ is open. Images of a countable base of $D$ then form a countable base of $H$ : for each $h \in W$ open, choose one $d \in q^{- 1} (h)$ and a basic neighbourhood $C$ with $d \in C \subseteq q^{- 1} (W)$ , so $h \in q (C) \subseteq W$ . Distinct maps over distinct base points separate by base neighbourhoods; distinct maps over one point separate in one Hausdorff matrix chart. Thus $H$ is Hausdorff and second countable.

4.1step 2.1step 3.1L1L5algebra

If the original bundle frames change by $g_{β α}$ and $h_{β α}$ , a Hom matrix $T$ changes to $h_{β α} T g_{β α}^{- 1}$ . These maps and their inverses are smooth by [L1] and [L5], so the charts in step 2.1 give $H$ a smooth vector-bundle atlas; a boundary base chart yields the corresponding half-space product chart. Fibre addition and scalar multiplication are linear in these coordinates. If $r = 0$ or $s = 0$ , $H$ is the zero bundle $M$ ; if $M$ is empty, it is empty.

5.1step 4.1L2algebra∎

Take $B = M \times R$ in steps 1.1–4.1 to obtain $E^{*} = Hom (E, M \times R)$ as a smooth bundle. A functional with row coordinates $ℓ$ changes to $ℓ g_{β α}^{- 1}$ ; by [L2], its column transition matrix is $(g_{β α}^{- 1})^{T}$ . Step 4.1 gives the stated Hom transition matrix.

Depends on

Used by

Sections of Hom are the same as smooth fibrewise linear maps Proposition
Vector-bundle curvature is an endomorphism-valued two-form Proposition

Dependency tree · two levels

54 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 M. Lee, Introduction to Smooth Manifolds (standard reference, not scraped)
Will J. Merry, Differential Geometry (standard reference, not scraped)