Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)
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

Definition

Let f:NM be smooth and let be a connection on EM. Give fE={(q,e)N×E:f(q)=π(e)} the subspace topology. If Φ:EUU×Rr is a vector-bundle chart and Φ(e)=(π(e),v), then Φ~(q,e)=(q,v),Φ~1(q,v)=(q,Φ1(f(q),v)). Both displayed maps are continuous in the subspace and product topologies, so this is a homeomorphism from (fE)f1U to f1U×Rr. On overlaps its change of coordinates is (q,v)(q,gβα(f(q))v), which is smooth and fibrewise linear. These charts therefore supply the smooth rank-r bundle structure directly. Its total space is Hausdorff and second countable: N×E is a smooth manifold by Products of smooth manifolds have a canonical product smooth structure, and both properties pass to the subspace fE by T0, T1, and Hausdorffness are hereditary and Second countability is hereditary.

In a pulled-back frame fe on f1U, the pullback connection f is specified by (f)X((fe)u)=(fe)(X(u)+(fω)(X)u), where (fω)q(v)=ωf(q)(dfqv) entrywise and u is any smooth coefficient column on N. These are local prescriptions under the gluing criterion Local connection forms glue exactly when they obey the transformation law; their compatibility and hence well-definedness are proved in the next theorem.

In particular, coefficient functions are not required to factor through f. For constant f, a constant frame of Ef(N) gives zero pulled-back matrix and ordinary differentiation of arbitrary u; it does not make every varying section parallel. Empty source and rank-zero bundles use empty coefficient data. No injectivity, immersion, submersion, or choice of an extension is part of this definition.

Depends on

Used by

Dependency tree · two levels

21 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