ExampleConstruction: Literature-sourcedVerification: 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.

A fibration over the circle has zero Godbillon-Vey class

Example

Assume Countable Choice ${A C}_{ω}$ . Let $q : M \to S^{1}$ be a smooth fibre bundle with connected fibre and let $F$ be the foliation of $M$ by the fibres of $q$ . Then $F$ is a transversely oriented codimension-one foliation defined by the closed nowhere- vanishing $1$ -form $ω = q^{*} d θ$ , where $d θ$ is the standard volume form on $S^{1}$ , and consequently $G V (F) = 0$ in $H_{d R}^{3} (M; R)$ . In particular the fibre foliation of the mapping torus of a diffeomorphism of a closed surface has zero Godbillon-Vey class.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ . A smooth fibre bundle $q : M \to S^{1}$ with connected fibre, its fibre foliation $F$ , and the volume form $d θ$ on $S^{1}$ .

[F1]

A transversely oriented codimension-one foliation defined by a closed nowhere-vanishing one-form has zero Godbillon-Vey class in $H_{d R}^{3} (M; R)$ . (Closed defining forms have vanishing Godbillon-Vey class).

Verification

technique · direct

1.1givenalgebra

The pullback $ω = q^{*} d θ$ is closed because $d θ$ is closed and pullback commutes with $d$ , and it is nowhere vanishing because $q$ is a submersion and $d θ$ is a volume form; its kernel foliation has the fibres of $q$ as leaves, and since the fibres are connected they are exactly the leaves, so $F$ is a transversely oriented codimension-one foliation defined by the closed form $ω$ .

2.1F1step 1.1∎

By [F1] the Godbillon-Vey class vanishes, $G V (F) = 0$ in $H_{d R}^{3} (M; R)$ ; in particular for the mapping torus of a diffeomorphism of a closed surface the base projection is the bundle map, so its fibre foliation also has zero Godbillon-Vey class, and only the standing countable choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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)