LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck pass

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.

Divisibility by a nowhere-vanishing one-form

Statement

Assume Countable Choice ${A C}_{ω}$ . Let $M$ be a smooth manifold, with boundary allowed, and let $ω$ be a nowhere-vanishing smooth $1$ -form on $M$ . (i) If $α \in Ω^{1} (M)$ satisfies $α \land ω = 0$ , then there is a unique $f \in C^{\infty} (M)$ with $α = f ω$ . (ii) If $θ \in Ω^{2} (M)$ satisfies $θ \land ω = 0$ , then there is $β \in Ω^{1} (M)$ with $θ = β \land ω$ .

Facts & Assumptions

Given: A smooth manifold $M$ with a nowhere-vanishing smooth one-form $ω$ , a one-form $α$ with $α \land ω = 0$ , and a two-form $θ$ with $θ \land ω = 0$ .

[F1]

The graded vector space $Ω^{*} (M)$ with the wedge product is an associative graded-commutative algebra. (Differential forms form a graded commutative algebra).

[F2]

If $(f_{i})$ are smooth functions on the members of an open cover and $(ϕ_{i})$ is a smooth partition of unity subordinate to that cover, then $F (p) = \sum_{i} ϕ_{i} (p) f_{i} (p)$ is a smooth function on $M$ . (Smooth locally defined functions can be glued by a partition of unity).

[F3]

Under ${A C}_{ω}$ , every smooth-manifold open cover admits a subordinate smooth partition of unity (Smooth partitions of unity exist on manifolds, Smooth partitions of unity exist on manifolds with boundary).

Proof

technique · direct

1.1givenalgebra

Fix $p \in M$ and choose $v \in T_{p} M$ with $ω_{p} (v) \neq 0$ , which exists because $ω$ is nowhere vanishing; evaluating the two-form $α \land ω$ on a pair $(u, v)$ and using its definition for a one-form times a one-form gives $0 = (α \land ω) (u, v) = α_{p} (u) ω_{p} (v) - α_{p} (v) ω_{p} (u)$ for every $u$ , so $α_{p} (u) = (α_{p} (v) / ω_{p} (v)) ω_{p} (u)$ ; the quotient $f (p) : = α_{p} (v) / ω_{p} (v)$ is independent of the choice of $v$ because it equals the value of the unique scalar with $α_{p} = f (p) ω_{p}$ , and such a scalar is unique as $ω_{p} \neq 0$ .

2.1F1step 1.1

To see that $f$ is smooth, fix a chart domain $U$ with coordinates $x_{1}, \dots, x_{m}$ and write $ω = \sum_{i} ω_{i} d x_{i}$ , $α = \sum_{j} a_{j} d x_{j}$ with smooth coefficient functions; by [F1] the wedge product expands as $α \land ω = \sum_{j < k} (a_{j} ω_{k} - a_{k} ω_{j}) d x_{j} \land d x_{k}$ , and the $d x_{j} \land d x_{k}$ are linearly independent over the coefficient functions, so $a_{j} ω_{k} = a_{k} ω_{j}$ on $U$ ; shrinking about any point at which some $ω_{i} \neq 0$ , one gets $a_{j} = a_{i} ω_{j} / ω_{i}$ for all $j$ , hence $α = (a_{i} / ω_{i}) ω$ there with smooth quotient $a_{i} / ω_{i}$ ; comparing with step 1.1 shows $f = a_{i} / ω_{i}$ on that smaller domain, and since smoothness is local $f$ is smooth on all of $M$ , giving (i).

2.2F1step 1.1

For (ii), fix a chart domain $U$ with coordinates as above and write $θ = \sum_{i < j} c_{i j} d x_{i} \land d x_{j}$ with $c_{j i} : = - c_{i j}$ ; by [F1] the wedge $θ \land ω$ has coefficient $c_{i j} ω_{k} - c_{i k} ω_{j} + c_{j k} ω_{i}$ on $d x_{i} \land d x_{j} \land d x_{k}$ for each triple $i < j < k$ , so $θ \land ω = 0$ gives those three-term identities; shrinking to a domain on which a fixed coefficient $ω_{i_{0}}$ is nowhere zero, define $b_{i} : = c_{i i_{0}} / ω_{i_{0}}$ for $i \neq i_{0}$ and $b_{i_{0}} : = 0$ , and let $β = \sum_{i} b_{i} d x_{i}$ ; substituting these definitions into the three-term identities in each of the three index orders, and using $c_{i j} = - c_{j i}$ , gives $c_{i j} = b_{i} ω_{j} - b_{j} ω_{i}$ for every pair ${i, j}$ , hence $θ = β \land ω$ on $U$ with smooth $β$ .

3.1F2F3step 2.2

Cover $M$ by such chart domains $U$ with local solutions $β_{U}$ , and use [F3] to obtain a smooth partition of unity $(ϕ_{U})$ subordinate to the cover; for overlapping domains, $(β_{U} - β_{V}) \land ω = 0$ , so by (i) there is a smooth function $f_{U V}$ with $β_{U} - β_{V} = f_{U V} ω$ on the overlap, and the local forms $ϕ_{U} β_{U}$ , extended by zero, satisfy $\sum_{U} ϕ_{U} β_{U} \land ω = \sum_{U} ϕ_{U} θ = θ$ ; thus $β : = \sum_{U} ϕ_{U} β_{U}$ is a globally defined smooth one-form by [F2] with $θ = β \land ω$ , which is (ii).

4.1F3step 1.1step 2.1step 3.1∎

Part (i) follows from steps 1.1 and 2.1, and part (ii) from step 3.1. Countable choice is used for the subordinate partition in [F3]; the local coefficients are explicit formulas in each chart.

Depends on

Used by

Dependency tree · two levels

34 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

Raoul Bott, Lectures on Characteristic Classes and Foliations (Lecture Notes in Mathematics 279; complete scan of the 178-page volume) (standard reference, not scraped)