LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Holonomy respects path concatenation and reversal

Statement

Assume Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $a$ be a leafwise path from $x$ to $y$ , let $b$ be a leafwise path from $y$ to $z$ , and let $T, S, R$ be local transversals at $x, y, z$ (Local transversals to a regular foliation). Then, with $a * b$ the concatenation (traverse $a$ , then $b$ ), $h_{a * b} (R, T) = h_{b} (R, S) \circ h_{a} (S, T) .$ Also $h_{a^{- 1}} (T, S) = (h_{a} (S, T))^{- 1}$ , where $a^{- 1}$ is the reversed leafwise path.

Facts & Assumptions

Given: Leafwise paths $a$ from $x$ to $y$ and $b$ from $y$ to $z$ in a regular foliation $F$ of $M$ , local transversals $T$ at $x$ , $S$ at $y$ , $R$ at $z$ , and the concatenation $a * b$ and reversal $a^{- 1}$ of leafwise paths.

[F1]

The holonomy germ $h_{a} (T^{'}, T) : (T, x) \to (T^{'}, y)$ of a leafwise path is well defined, independent of the chart chain, the subdivision and the auxiliary transversals, and in a single foliation chart it is the germ matching points of the transversals with equal transverse coordinates (The holonomy germ is independent of the foliation chart chain, Plaques of a flat chart, Regular foliation atlases).

[F2]

Concatenation and reversal of leafwise paths are leafwise paths: the concatenation traverses $a$ on the first half and $b$ on the second, the reversal traverses $a$ backwards; both lie in the common leaf (Leafwise paths and leafwise homotopy relative to endpoints).

[F3]

Germs of local diffeomorphisms at a point form a group under composition, so germs have inverses and composites of germs are germs; two germs are equal when representatives agree near the source point (Germs of local diffeomorphisms at a point form a group, Germs of local diffeomorphisms at a point).

Proof

technique · direct

1.1F1F2F3

Single-chart computation. Suppose that both $a$ and $b$ have images in a single foliation chart $U$ with coordinates $(x, y)$ ; then so does $a * b$ , and $x, y, z$ lie in one plaque of $U$ because a leafwise path segment in a chart stays in a plaque. By [F1] each of the three transports matches transverse coordinates in $U$ : $h_{a} (S, T)$ sends $u \in T$ to the point of $S$ with the same $y$ -coordinate, $h_{b} (R, S)$ sends that point to the point of $R$ with the same $y$ -coordinate, and $h_{a * b} (R, T)$ sends $u$ directly to the point of $R$ with the same $y$ -coordinate. The composite therefore agrees with the direct transport on a neighbourhood of $x$ , so their germs are equal by [F3]. Similarly, traversing $a$ backwards exchanges source and target and inverts the coordinate matching, so $h_{a^{- 1}} (T, S)$ is the inverse germ of $h_{a} (S, T)$ .

1.2F1F2

General chain computation. Choose a chart chain for $a$ with endpoint transversals $T, S$ and a chart chain for $b$ with endpoint transversals $S, R$ . Concatenating the two chains and the two subdivisions at the middle time gives a chart chain for $a * b$ with endpoint transversals $T, R$ and the intermediate transversal $S$ at the middle point. By definition of the holonomy germ as the composite of the chart-wise transports, the germ obtained from this concatenated chain is exactly $h_{b} (R, S) \circ h_{a} (S, T)$ ; by chain independence [F1] it equals the intrinsic germ $h_{a * b} (R, T)$ .

2.1F1F3step 1.1

Reversal. Choose a chart chain for $a$ ; reading the same charts and subdivision backwards gives a chart chain for $a^{- 1}$ with the endpoint transversals exchanged. In each chart the reversed transport is the inverse of the forward transport by step 1.1, and by the group law for germs [F3] the composite of the inverses is the inverse of the composite, so $h_{a^{- 1}} (T, S) = (h_{a} (S, T))^{- 1}$ by [F1].

3.1step 1.2step 2.1∎

Conclusion. Steps 1.2 and 2.1 give $h_{a * b} (R, T) = h_{b} (R, S) \circ h_{a} (S, T)$ and $h_{a^{- 1}} (T, S) = (h_{a} (S, T))^{- 1}$ for arbitrary leafwise paths $a, b$ and endpoint transversals.

Depends on

Used by

Two nonhomotopic leaf loops can have the same holonomy germ Counterexample
The holonomy groupoid of a foliation Definition
The holonomy representation and the holonomy group of a leaf Definition
Holonomy classes form a groupoid congruence Lemma
The deck group of the holonomy cover is the holonomy group Lemma
Suspension holonomy is the germ of the represented monodromy action Proposition
The isotropy of the holonomy groupoid is the leaf holonomy group Proposition

Dependency tree · two levels

35 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

Danny Calegari, Foliations and the Geometry of 3-Manifolds (Oxford Mathematical Monographs) (standard reference, not scraped)
Leiden NCG seminar, Noncommutative Geometry of Foliations (2023 seminar notes) (standard reference, not scraped)
Eckhard Meinrenken, Lie Groupoids and Lie Algebroids, lecture notes (University of Toronto MAT1341, Fall 2017) (standard reference, not scraped)