Alphabeta MathHow 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 of forms is smooth functorial and preserves wedges
Statement
For a smooth map , pullback sends smooth differential forms on to smooth differential forms on , is functorial, and satisfies
Facts & Assumptions
Given: A smooth map , a smooth map , and forms on the target.
A form pullback is the covariant tensor pullback restricted to alternating tensors (The pullback of a differential form).
Covariant tensor pullback is smooth and functorial (Pullback of covariant tensors is smooth and functorial).
Fibrewise linear pullback respects tensor products and permutations, hence wedge products (Linear pullback respects tensor products and permutations).
Proof
By [F1], is obtained from the covariant tensor pullback. Because [L1] sends smooth covariant tensors to smooth covariant tensors and preserves composition, the same is true for forms.
At each point , [F1] and [L2] give which is exactly .
The identity and composition laws are inherited from [L1], and step 1.2 gives wedge preservation. Therefore pullback of forms is smooth, functorial, and wedge-preserving.
Depends on
Used by
- Closed differential forms are locally exact Corollary
- The volume coordinate expression changes sign under a reflection Counterexample
- Integral of a form over a smooth singular simplex Definition
- Pullback of the circle angular form along a parametrized curve Example
- The area form in polar coordinates Example
- Finite chart localization of compactly supported top forms, including boundary Lemma
- Integration over the signed shuffle equals the product of simplex integrals Lemma
- Restriction of a foliation transverse to the boundary Lemma
- The de Rham complex and pullback extend to manifolds with boundary Lemma
- Trace of a holomorphic differential along a nonconstant map to the sphere Lemma
- A diffeomorphism pulls back tensor fields and forms isomorphically Proposition
- De rham cohomology is a contravariant functor Proposition
- Pullback is a homomorphism of de rham cohomology algebras Proposition
- Change of variables on oriented manifolds Theorem
- Compact Kähler Hodge decomposition from elliptic harmonic forms Theorem
- Coordinate independence of chart integrals Theorem
- Naturality of de rham mayer vietoris for maps of covered manifolds Theorem
- Stokes theorem for smooth singular chains Theorem
- The exterior derivative commutes with pullback Theorem
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
- Will J. Merry, Differential Geometry (standard reference, not scraped)