TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

The exterior derivative commutes with pullback

Statement

For every smooth map $F : M \to N$ and every form $ω$ on $N$ , $d (F^{*} ω) = F^{*} (d ω) .$

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that On a chart, if $ω = \sum_{I} ω_{I} d x^{I}$ , then $d ω = \sum_{I} d ω_{I} \land d x^{I} .$ (The local coordinate formula for the exterior derivative).

Proof

technique · direct

1.1

Fix $p \in M$ , choose target coordinates $(y^{1}, \dots, y^{n})$ near $F (p)$ , and write $ω = \sum_{I} ω_{I} d y^{I}$ there. Pullback sends $ω_{I}$ to $ω_{I} \circ F$ and $d y^{a}$ to $d (y^{a} \circ F)$ .

given

2.1

On a neighbourhood of $p$ , the coordinate formula and the pullback wedge law give $\begin{aligned} d (F^{*} ω) & = \sum_{I} d (ω_{I} \circ F) \land d (y^{i_{1}} \circ F) \land \dots \land d (y^{i_{k}} \circ F) \\ = F^{*} ⁣ (\sum_{I} d ω_{I} \land d y^{I}) = F^{*} (d ω) . \end{aligned}$ Since $p$ was arbitrary, the identity holds on $M$ .

F1step 1.1∎

Depends on

Used by

Pullback carries closed forms to closed forms and exact forms to exact forms Corollary
Lie derivatives are natural for related vector fields Proposition

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

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)