PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Local coordinate expression for a differential form

Statement

On a chart $(U, x^{1}, \dots, x^{n})$ , every smooth differential $k$ -form $ω$ has a unique expression

ω = \sum_{1 \leq i_{1} < \dots < i_{k} \leq n} ω_{i_{1} \dots i_{k}} d x^{i_{1}} \land \dots \land d x^{i_{k}}

with smooth coefficient functions $ω_{i_{1} \dots i_{k}}$ on $U$ .

Facts & Assumptions

Given: A smooth $k$ -form $ω$ on a chart domain $U$ with coordinates $x^{1}, \dots, x^{n}$ .

[F1]

A smooth $k$ -form is a smooth section of $⋀^{k} T^{*} M$ (A smooth differential $k$ -form).

[L1]

The coordinate differentials $d x^{1}, \dots, d x^{n}$ form the dual basis of the cotangent fibres, and their increasing wedges form a basis of the alternating $k$ -covectors (Coordinate differentials form the dual cotangent basis, Wedge monomials in a dual basis form a basis).

[L2]

Smoothness of a section is equivalent to smoothness of its local components (Smoothness of a section is equivalent to smooth local components).

Proof

technique · direct

1.1

At each point $p \in U$ , [L1] gives a basis of $⋀^{k} T_{p}^{*} M$ , so $ω_{p}$ has a unique expansion $ω_{p} = \sum_{I} ω_{I} (p) d x_{p}^{I}$ over increasing multi-indices $I$ .

F1L1given

2.1

The coefficient functions $p \mapsto ω_{I} (p)$ are exactly the local components of the section $ω$ in the bundle frame from [L1]. Therefore [L2] makes them smooth on $U$ .

L1L2step 1.1

3.1

This gives the unique local coordinate expression for $ω$ .

step 1.1step 2.1∎

Depends on

Used by

Interior product of a form by a vector field Definition
The area form in polar coordinates Example

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)