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 difference of two connections is an endomorphism valued one form
Statement
For two connections on the same bundle , there is a unique smooth section of such that This is called an endomorphism-valued one-form. In a frame it has matrix .
Facts & Assumptions
Given: Two connections on a finite-rank smooth real bundle.
The local coefficient rule is (Local coordinate formula for a bundle connection).
Connection matrices transform by conjugation plus (Connection one form transformation law).
The choice-free open-quotient construction gives Hom bundles with Hausdorff second-countable smooth structures and the fibrewise matrix transition rule (Connection on a smooth vector bundle).
Proof
Subtracting the local formulas cancels : for , the difference is . At a point it depends only on and , not their derivatives. Thus the matrix difference gives a smooth linear map in each chart, including zero inputs.
Under , the two terms cancel and the matrix difference becomes . This is exactly change of basis for the same fibre endomorphism. These local maps agree intrinsically and define the claimed smooth Hom section. Every fibre vector is a value of a local constant-coefficient section; the equality for these sections determines the endomorphism uniquely. Equal connections give ; rank one gives scalar one-forms, rank zero gives the unique zero map, and an empty base imposes no values. This is a comparison of supplied connections and uses no existence theorem or choice axiom.
Depends on
Used by
Dependency tree · two levels
14 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)