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.

Independence of the auxiliary form eta up to exact forms

Statement

Assume Countable Choice ${A C}_{ω}$ . Let $F$ be a transversely oriented codimension-one foliation with defining form $ω$ , and let $η, η^{'}$ be smooth $1$ -forms with $d ω = η \land ω = η^{'} \land ω$ . If $η^{'} - η = f ω$ with $f \in C^{\infty} (M)$ , then $η^{'} \land d η^{'} = η \land d η - d (f d ω) = η \land d η + d (d f \land ω)$ , and in particular $[η^{'} \land d η^{'}] = [η \land d η]$ in $H_{d R}^{3} (M; R)$ .

Facts & Assumptions

Given: A transversely oriented codimension-one foliation with defining form $ω$ and one-forms $η, η^{'}$ satisfying $d ω = η \land ω = η^{'} \land ω$ , with $η^{'} - η = f ω$ .

[F1]

With $d ω = η \land ω$ one has $d η \land ω = 0$ and $η \land d η$ is closed. (The Godbillon-Vey form eta wedge d eta is closed).

[F2]

For homogeneous smooth forms $α, β$ of degrees $p, q$ one has $d (α \land β) = d α \land β + (- 1)^{p} α \land d β$ . (The exterior derivative is a graded derivation).

[F3]

The wedge product is associative and graded-commutative, so odd-degree forms anticommute and $ω \land ω = 0$ . (The wedge product is associative and graded commutative).

[F4]

For every differential form $ω$ , $d (d ω) = 0$ . (The exterior derivative squares to zero).

Proof

technique · direct

1.1F2F4given

Write $η^{'} = η + f ω$ ; differentiating and using $d ω = η \land ω$ and $d (f ω) = d f \land ω + f d ω$ from [F2] gives $d η^{'} = d η + d f \land ω + f d ω$ , while $d (d ω) = 0$ by [F4] is compatible with $d ω = η^{'} \land ω$ .

2.1F1F3step 1.1

Expanding $η^{'} \land d η^{'} - η \land d η = (f ω) \land d η + η \land (d f \land ω + f d ω) + (f ω) \land (d f \land ω + f d ω)$ , every term containing $η \land η$ , $d η \land ω$ , $ω \land d η$ , $ω \land d ω$ or $ω \land ω$ vanishes by [F1] and the graded commutativity and $ω \land ω = 0$ of [F3], leaving $η \land d f \land ω = - d f \land d ω$ .

3.1F2F3step 2.1∎

Since $d η \land ω = 0$ by [F1] and $d η^{'} = d η + d f \land ω + f d ω$ , the identity $d (d f \land ω) = d (d f) \land ω - d f \land d ω = - d f \land d ω$ from [F2] and [F4] shows that $η^{'} \land d η^{'} = η \land d η - d (f d ω) = η \land d η + d (d f \land ω)$ , an exact modification; hence the two forms have the same de Rham class, and no choice principle is used.

Depends on

Used by

The Godbillon-Vey class of a codimension-one foliation Definition

Dependency tree · two levels

27 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

Steven Hurder and Remi Langevin, Dynamics and the Godbillon-Vey Class of C1 Foliations (complete author-hosted PDF) (standard reference, not scraped)