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.
Connection laws in directional form
Statement
The directional operator of a connection obeys for smooth functions , real numbers , vector fields and sections . Conversely, a map with these three laws comes from a unique connection by evaluation. This includes manifolds with boundary.
Facts & Assumptions
Given: The displayed objects; for the converse a smooth-section-valued map satisfying the three displayed laws.
A connection is a real-linear Hom-bundle-section-valued operator satisfying the one-form Leibniz identity (Connection on a smooth vector bundle).
The directional derivative evaluates that Hom section on (Covariant derivative of a section in a vector field direction).
Chart bumps with support in a prescribed open neighbourhood exist (A chart bump at a point with prescribed support).
A compact subset of a Euclidean open set admits a smooth bump equal to one on that subset (A Euclidean bump for a compact set inside an open set).
Proof
Fibrewise linearity of gives the first identity by evaluating at . Real linearity of gives the second. Evaluating on gives the third because .
We will use a cutoff supported in a prescribed neighbourhood and equal to one on a smaller neighbourhood of a chosen point. On an interior chart this is precisely the construction in the proof of [F3]: apply [F4] to two nested balls about the coordinate point and extend by zero. For a boundary chart with image relatively open in a closed half-space , choose radii such that lies in the chart image. Restrict a Euclidean bump equal to one on and supported in to , then pull back and extend by zero. Its support lies in the compact chart preimage of , hence is closed in the Hausdorff manifold and contained in the chart; zero extension is smooth. In dimension zero use the indicator of the open-and-closed singleton. Each construction is at a fixed point, requiring only finitely many choices.
Fix and write . If vanishes near , take a cutoff supported there with . Then and . Thus depends only on the germ of . Local fields may now be multiplied by a cutoff equal to one near and extended by zero; applying and evaluating at is independent of that extension. On a neighbourhood where one fixed cutoff is one, the result is the restriction of a smooth global output, so these local values are smooth.
In a coordinate neighbourhood write . The extended local operator satisfies : extend all fields and coefficient functions using a common cutoff equal to one near and apply global function-linearity, then use step 2.1. Hence depends only on . Define . Germ independence shows this definition is independent of coordinates, and the smoothness in step 2.1 shows is a smooth Hom section. Every vector at has a local constant-coordinate extension and then a cutoff global extension, so its value is uniquely forced by .
Real linearity in gives real linearity of . Testing on a tangent vector using a global field with that value, the third law gives . Thus is the unique connection inducing . If is empty there are no pointwise tests and both operators are unique zero maps; if the coordinate sum is empty. Rank zero gives zero outputs, while in rank one the same finite calculation has one output component. No simultaneous family of cutoff choices was made: uniqueness defines the global section from locally proved values.
Depends on
Used by
- Metric compatible connection on a riemannian vector bundle Definition
- A connection is c infinity linear in the section being differentiated False statement
- Torsion free means curvature free False statement
- A bundle connection is local and restricts to open sets Lemma
- Torsion is c infinity bilinear and skew symmetric Lemma
- Gradient hessian and divergence connection formulas Proposition
- Local coordinate formula for a bundle connection Proposition
- Christoffel symbol transformation law Theorem
- The koszul formula defines an affine connection Theorem
Dependency tree · two levels
26 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, section 4.1 (standard reference, not scraped)