Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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 restriction

Statement

Let M be a smooth manifold, U⊆M open, k≥0, ω∈Ωk(M), and j:U↪M the inclusion. Then j∗(dMω)=dU(j∗ω), where the subscripts specify the manifold.

Facts & Assumptions

Given: The smooth manifold M, open subset U, and smooth k-form ω in the statement.

[F2]

The invariant vector-field formula defines d locally from the values of a form, vector fields, and their brackets (The exterior derivative by the invariant vector-field formula).

[F3]

A smooth bump equal to one near a point and supported inside a chosen chart exists (A manifold bump for a compact set inside an open set).

Proof

technique · direct
1.1F3givenconstruct

Fix p∈U and tangent vectors v0,…,vk∈TpM=TpU. Choose a chart around p contained in U, extend each vector using constant coordinate coefficients there, multiply by a bump equal to one near p, and extend by zero. This gives smooth fields Y0,…,Yk on M with Yi(p)=vi.

2.1F2step 1.1algebra

Evaluate the invariant formula for dMω on Yi and the formula for dU(ω∣U) on Yi∣U. Each scalar evaluation of the form restricts to the same smooth function on U, so its directional derivatives agree there. Brackets restrict as well: their commutators on smooth functions have identical local expressions. Thus every term in the two formulas has the same value at p.

3.1step 1.1step 2.1given∎

The arbitrary tangent vectors in step 1.1 show equality of the two (k+1)-covectors at p, and arbitrary p gives dU(ω∣U)=(dMω)∣U. Pullback by the open inclusion is restriction because its tangent map is the identity under TpU=TpM, proving the claim. The assertion is vacuous if U is empty.

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