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.
Adding an endomorphism valued one form to a connection gives a connection
Statement
If is a connection and , then defines a connection. If the set of connections is nonempty, it is an affine space modeled on the real vector space of endomorphism-valued one-forms: that vector space acts freely and transitively by this addition.
Facts & Assumptions
Given: A connection and a smooth endomorphism-valued one-form on .
The connection definition is real linearity and the one-form Leibniz rule (Connection on a smooth vector bundle).
Two connections have a unique endomorphism-valued one-form as their difference (The difference of two connections is an endomorphism valued one form).
Proof
Define . In local matrices this is a finite sum of products of smooth coefficients, hence a smooth Hom section. It is real-linear in and satisfies . Therefore . This proves the connection axioms.
Adding the zero form fixes , and adding then equals adding by pointwise evaluation. The difference theorem shows any other connection equals for exactly one , proving transitivity and freeness. For a rank-zero bundle the modeling vector space is zero and the connection space a singleton; an empty base has the same interpretation. In rank one the action is addition of scalar one-forms. No claim of nonemptiness without a given connection, or choice of a preferred origin, enters this affine-space assertion.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
13 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)