ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generated

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.

The product foliation near a compact leaf with trivial holonomy

Example

Assume Countable Choice ${A C}_{ω}$ (The countable-choice principle used in the foliation pair). Let $L = S^{1}$ and consider the product foliation of $M = S^{1} \times R$ by the circles $L_{t} = S^{1} \times {t}$ . Each leaf is compact and has trivial holonomy: a local transversal is a vertical interval ${u} \times (t_{0} - ε, t_{0} + ε)$ and the holonomy of any leafwise loop is the identity. For every leaf $L_{t_{0}}$ and every $δ > 0$ the open set $U_{δ} = S^{1} \times (t_{0} - δ, t_{0} + δ)$ is a saturated neighbourhood of $L_{t_{0}}$ foliated-diffeomorphic to the product $S^{1} \times (- δ, δ)$ with the product foliation, so the conclusion of Trivial holonomy gives a product foliated neighbourhood is realised exactly. The same computation with $L = T^{2}$ gives compact leaves with infinite fundamental group and trivial holonomy, showing that trivial holonomy does not require finiteness of $π_{1}$ .

Verification

Given: The product foliation of $M = S^{1} \times R$ by the circles $S^{1} \times {t}$ , a leaf $L_{t_{0}}$ , and $δ > 0$ .

[F1] The product $S^{1} \times R$ carries the product smooth structure and the product foliation by the slices $S^{1} \times {t}$ , whose leaves are the maximal connected integral manifolds of the kernel of $d t$ (Products of smooth manifolds have a canonical product smooth structure, Regular foliation atlases).

[F2] A local transversal to the product foliation at a point of $S^{1} \times {t_{0}}$ can be taken to be the vertical interval ${u} \times (t_{0} - ε, t_{0} + ε)$ , and the plaque transport in product coordinates is the identity (Local transversals to a regular foliation).

[F3] Trivial holonomy on a compact leaf gives a fundamental system of product foliated neighbourhoods $L \times D$ , whose leaves are compact and diffeomorphic to $L$ (Trivial holonomy gives a product foliated neighbourhood).

[F4] The fundamental group of the two-dimensional torus is $Z^{2}$ , hence infinite ( $π_{1} (T^{2}) ≅ Z \times Z$ , The two-dimensional torus $T^{2} = (R / Z)^{2}$ ).

Proof technique: direct verification.

1.1F1F2

(Leaves and their holonomy.) The slices $S^{1} \times {t}$ are the maximal connected integral manifolds of the kernel of $d t$ , hence the leaves of the product foliation [F1]. A leafwise loop lies inside a single slice $L_{t}$ , and following it transports the vertical transversal ${u} \times (t - ε, t + ε)$ by the identity in product coordinates, since the second coordinate is constant along the slices; hence the holonomy representation of every leaf is trivial [F2].

1.2F1F3

(Product neighbourhoods.) Fix $t_{0}$ and $δ > 0$ . The set $U_{δ} = S^{1} \times (t_{0} - δ, t_{0} + δ)$ is open, contains $L_{t_{0}}$ , and is a union of slices, hence saturated; the translation $(u, t) \mapsto (u, t - t_{0})$ is a foliated diffeomorphism onto $S^{1} \times (- δ, δ)$ with the product foliation, and these neighbourhoods for shrinking $δ$ form a fundamental system. This is exactly the conclusion of the product corollary for a compact leaf of trivial holonomy [F3].

2.1F3F4step 1.1∎

(The torus variant.) Replacing $S^{1}$ by $T^{2}$ in the same argument gives the product foliation of $T^{2} \times R$ : the slices are compact leaves with trivial holonomy by the same computation, while their fundamental group is $Z^{2}$ , which is infinite [F4]. Hence trivial holonomy does not require finiteness of $π_{1}$ , and the same direct product calculation applies to every nonempty connected closed smooth fibre $L$ , independently of its fundamental group.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

Leiden NCG seminar, Noncommutative Geometry of Foliations (2023 seminar notes; complete PDF) (standard reference, not scraped)
Danny Calegari, Foliations and the Geometry of 3-Manifolds (Oxford Mathematical Monographs; complete author-hosted PDF) (standard reference, not scraped)