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.
Pullback connection is well defined and functorial
Statement
The pullback prescription defines a unique connection , independent of frames. Under the canonical bundle isomorphisms it satisfies and . For a local section of , The right side is interpreted in the fibre of the pullback bundle at .
Facts & Assumptions
Given: Smooth maps , and a connection on .
The pullback prescription uses matrix in frame (Pullback connection).
Matrices transform by (Connection one form transformation law).
The matrix overlap condition is necessary and sufficient for unique gluing (Local connection forms glue exactly when they obey the transformation law).
The canonical composite pullback isomorphisms preserve fibre coordinates in pulled-back charts (Pullback is functorial up to canonical bundle isomorphism).
Proof
Pull back the identity in [F2]. Composition preserves matrix products and inverses, and the chain rule gives . Thus . These are exactly the transition matrices of the pulled-back frames, so the prescription glues uniquely and is frame independent.
For a one-form entry and , by the chain rule. Hence the connection matrices coincide in the frames identified by the canonical bundle isomorphism. Gluing uniqueness gives composite functoriality; the identity case is the same evaluation with .
If , then . Its coefficient derivative is , giving the displayed section identity. Constant has , so pulled-back sections from are parallel, whereas general coefficients on still differentiate as prescribed. Empty bases and rank-zero bundles give unique zero operators; no rank condition on was used and rank one follows entrywise. All local values are specified uniquely without AC.
Depends on
Used by
- Covariant derivative along a curve Definition
- Pullback of the flat connection Example
- Pullback connections intertwine parallel transport Proposition
- Covariant derivative along a curve is independent of frame and extension Theorem
Cited to discharge well-definedness by Pullback connection.
Dependency tree · two levels
12 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
- Ved Datar, Lectures on Riemannian Geometry (standard reference, not scraped)