Alphabeta Math
TheoremStatement: 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.

Pullback connection is well defined and functorial

Statement

The pullback prescription defines a unique connection f, independent of frames. Under the canonical bundle isomorphisms it satisfies id= and g(f)=(fg). For a local section s of E, (f)X(fs)(q)=(s)f(q)(dfqXq). The right side is interpreted in the fibre of the pullback bundle at q.

Facts & Assumptions

Given: Smooth maps g:PN, f:NM and a connection on EM.

[F1]

The pullback prescription uses matrix fω in frame fe (Pullback connection).

[F2]

Matrices transform by ω=A1ωA+A1dA (Connection one form transformation law).

[F3]

The matrix overlap condition is necessary and sufficient for unique gluing (Local connection forms glue exactly when they obey the transformation law).

[F4]

The canonical composite pullback isomorphisms preserve fibre coordinates in pulled-back charts (Pullback is functorial up to canonical bundle isomorphism).

Proof

1.1

Pull back the identity in [F2]. Composition preserves matrix products and inverses, and the chain rule gives d(Af)=f(dA). Thus fω=(Af)1(fω)(Af)+(Af)1d(Af). These are exactly the transition matrices of the pulled-back frames, so the prescription glues uniquely and is frame independent.

F1F2F3
2.1

For a one-form entry η and vTxP, (gfη)x(v)=ηf(g(x))(dfg(x)dgxv)=((fg)η)x(v) by the chain rule. Hence the connection matrices coincide in the frames identified by the canonical bundle isomorphism. Gluing uniqueness gives composite functoriality; the identity case is the same evaluation with did=id.

F1F3F4step 1.1
3.1

If s=eu, then fs=(fe)(uf). Its coefficient derivative is X(uf)=du(dfX), giving the displayed section identity. Constant f has df=0, so pulled-back sections from E are parallel, whereas general coefficients on N still differentiate as prescribed. Empty bases and rank-zero bundles give unique zero operators; no rank condition on df was used and rank one follows entrywise. All local values are specified uniquely without AC.

F1step 1.1

Depends on

Used by

Cited to discharge well-definedness by Pullback connection.

Dependency tree · two levels

12 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