Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated
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.

A bundle connection is local and restricts to open sets

Statement

For a connection on EM, if two sections agree near p, their covariant derivatives at p agree in every tangent direction. The derivative in direction X depends only on X(p). For every open UM, there is a unique connection on EU agreeing with the original on restricted global sections; restrictions to nested open sets compose. Boundary points are included.

Facts & Assumptions

Given: A smooth bundle EM, a connection , a point p where relevant, and an open set U.

[F1]

Directional connection laws hold; the converse proof also constructs plateau cutoffs in interior and boundary charts (Connection laws in directional form).

[F2]

The connection value is a smooth fibrewise linear map TpMEp (Connection on a smooth vector bundle).

Proof

1.1

Suppose s vanishes on a neighbourhood W of p. Take a smooth cutoff χ supported in W with χ(p)=1, using the construction in the proof of [F1]. Since χs=0, the Leibniz rule at any vTpM gives 0=v(χs)=dχp(v)s(p)+χ(p)vs=vs. Apply this to the difference of two sections. The direction depends only on its value by [F2]; no assertion that dχp=0 was needed in this vanishing argument.

F1F2
2.1

For a local section s on U, take a cutoff supported in U and equal to one on a neighbourhood V of pU. Extend χs by zero outside U to a global smooth section s~: outside its closed support it is identically zero, so the definitions paste smoothly. Define (Us)p=(s~)p. Different extensions agree near p, so step 1.1 proves independence. On V, one fixed extension works at every point, making Us smooth. Local functions can be extended by the same cutoff; the global real-linearity and Leibniz laws then imply those laws on U. Thus this is a connection.

F1step 1.1construct
3.1

Any other restriction connection is local by step 1.1 applied on U, and agrees on the global extension in step 2.1; hence its value on s at p is forced. This proves uniqueness and, by applying uniqueness twice, composition of restrictions. The empty open set has a unique zero operator. Zero sections and rank-zero bundles give zero derivatives in steps 1.1 and 2.1; rank one and a zero-dimensional base require no modification. A single point is handled with a single cutoff, and the uniquely specified values assemble without a choice of cutoffs for all points.

step 1.1step 2.1

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