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 finite-holonomy normal model of the Möbius band

Example

Assume Countable Choice ${A C}_{ω}$ (The countable-choice principle used in the foliation pair). Let $M : = (S^{1} \times (- 1, 1)) / Z_{2}$ be the Möbius band, the quotient by the free involution $τ (u, v) : = (u + \frac{1}{2}, - v)$ , foliated by the images of the circles $S^{1} \times {v}$ . The central leaf $L_{0}$ (image of $v = 0$ ) is the circle $R / (\frac{1}{2} Z)$ whose holonomy group is $Z_{2}$ , generated by the reflection germ $v \mapsto - v$ of a transversal interval: going once around the central leaf identifies the transversal coordinate $v$ with $- v$ (The holonomy representation and the holonomy group of a leaf). Its holonomy cover is the connected double cover ${\hat{L}}_{0} = S^{1} \to L_{0}$ (The holonomy cover of a leaf), the deck group is $Z_{2}$ acting by $u \mapsto u + \frac{1}{2}$ , and the finite-holonomy normal model $({\hat{L}}_{0} \times D) / Z_{2}$ with the diagonal action $(u, v) \mapsto (u + \frac{1}{2}, - v)$ is exactly the Möbius band with its foliation: the quotient recovers the surface and the central leaf $({\hat{L}}_{0} \times {0}) / Z_{2} ≅ L_{0}$ . The other leaves are images of $S^{1} \times {v}$ and double-cover the central leaf, as predicted by the finite-holonomy model.

Verification

Given: The involution $τ (u, v) = (u + \frac{1}{2}, - v)$ on $S^{1} \times (- 1, 1)$ with $S^{1} = R / Z$ , the product foliation by the slices $S^{1} \times {v}$ , and the quotient $M$ .

[F1] A free properly discontinuous action by diffeomorphisms preserving a regular foliation descends the foliation to the quotient, whose leaves are the images of the leaves (The quotient foliation under a free and properly discontinuous foliated action).

[F2] The holonomy representation of a leaf and the holonomy cover with deck group isomorphic to the holonomy group are as in The holonomy representation and the holonomy group of a leaf, The holonomy cover of a leaf and The deck group of the holonomy cover is the holonomy group.

[F3] The finite-holonomy normal model is the diagonal quotient $(\hat{L} \times D) / H$ with the deck action on the holonomy cover and the holonomy action on the invariant transverse disk (The finite-holonomy normal model of a compact leaf).

Proof technique: direct verification.

1.1F1

(The quotient is the Möbius band.) The map $τ$ is an involution: $τ^{2} (u, v) = τ (u + \frac{1}{2}, - v) = (u + 1, v) = (u, v)$ in $S^{1} = R / Z$ . It is free: $τ (u, v) = (u, v)$ would give $v = - v$ , hence $v = 0$ , and then $u = u + \frac{1}{2}$ , impossible in $S^{1} = R / Z$ ; since $S^{1} \times (- 1, 1)$ is a surface and the action is free and properly discontinuous, the quotient $M$ is a smooth surface. It is the total space of the interval bundle over $S^{1} = R / (\frac{1}{2} Z)$ with monodromy $v \mapsto - v$ , the non-trivial interval bundle, i.e. the Möbius band.

1.2F1F2

(The foliation descends and the holonomy is $Z_{2}$ .) The involution carries the slice $S^{1} \times {v}$ onto $S^{1} \times {- v}$ , so the product foliation is preserved and descends to a codimension-one foliation of $M$ whose leaves are the images of the slices [F1]. The image of $S^{1} \times {0}$ is the central leaf $L_{0} = R / (\frac{1}{2} Z)$ ; following it once around means passing from $u$ to $u + \frac{1}{2}$ , and the identification in the quotient returns the transversal coordinate $v$ to $- v$ , so the return germ is the reflection $v \mapsto - v$ and the holonomy group is $Z_{2}$ [F2].

2.1F2F3step 1.2

(The holonomy cover and the normal model.) The holonomy cover of $L_{0}$ is the connected double cover ${\hat{L}}_{0} = S^{1} \to L_{0}$ with deck group $Z_{2}$ acting by $u \mapsto u + \frac{1}{2}$ [F2]. With $D$ a small invariant transversal interval and the diagonal action $(u, v) \mapsto (u + \frac{1}{2}, - v)$ , the finite-holonomy normal model $({\hat{L}}_{0} \times D) / Z_{2}$ is the quotient of $S^{1} \times D$ by exactly the involution $τ$ restricted to $S^{1} \times D$ , hence equals the Möbius band over $D$ with the descended foliation; the central leaf is $({\hat{L}}_{0} \times {0}) / Z_{2} ≅ L_{0}$ [F3].

3.1F1F3step 2.1∎

(The other leaves.) For $v \neq 0$ , the map $u \mapsto [(u, v)]$ from $S^{1}$ to the quotient leaf is injective: the only nonidentity group element changes $v$ to $- v$ . It parametrizes that entire leaf, because the other slice at $- v$ has the same image. Under the model retraction to $L_{0} = R / (\frac{1}{2} Z)$ its projection is $u m o d Z \mapsto u m o d (\frac{1}{2} Z)$ , a double covering. In a fixed local transverse fibre the two leaf intersections at $v$ and $- v$ are distinct points; they are not identified in that fibre. This is exactly the stabilizer calculation $[H : H_{v}] = 2$ for $H_{v} = {1}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

63 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)
Ieke Moerdijk and Janez Mrčun, Introduction to Foliations and Lie Groupoids (Cambridge Studies in Advanced Mathematics 91, 2003) (standard reference, not scraped)