LemmaStatement: Literature-sourcedProof: 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 deck group of the holonomy cover is the holonomy group

Statement

Assume ${A C}_{ω}$ (The countable-choice principle used in the foliation pair). Let $F$ be a regular foliation, $L$ a leaf, $x \in L$ , $T$ a local transversal at $x$ , $ρ_{x} : π_{1} (L, x) \to {Diff}_{x} (T)$ the holonomy homomorphism with the convention $ρ_{x} ([a]) = h_{a^{- 1}} (T, T)$ , and $p : \hat{L} \to L$ the holonomy cover, with $\hat{x} \in p^{- 1} (x)$ and $p_{*} π_{1} (\hat{L}, \hat{x}) = \ker ρ_{x}$ (The holonomy cover of a leaf). Then:

$p$ is a regular covering, $π_{1} (L, x) / \ker ρ_{x}$ acts faithfully on $\hat{L}$ by deck transformations, and $Deck (p) ≅ π_{1} (L, x) / \ker ρ_{x} ≅ Hol (L, x) = ρ_{x} (π_{1} (L, x))$ ;
the deck action is a covering-space action, $\hat{L} / Deck (p) ≅ L$ , and the quotient map is $p$ ;
the holonomy group acts through transverse germs via $ρ_{x}$ ; when those germs are realized on a common invariant transverse neighbourhood $D$ , the diagonal action of $H = Hol (L, x)$ on $\hat{L} \times D$ is free and a covering-space action. In particular, when $H$ is finite, $p$ is a finite-sheeted covering of degree $∣ H ∣$ .

Traversal-order loop multiplication and composition-order germs require this reversed-loop convention, as in The holonomy representation and the holonomy group of a leaf. Forward transport is an antihomomorphism with the same image and kernel as sets. The reversed-loop convention makes the deck identification and diagonal action homomorphic.

Facts & Assumptions

Given: A regular foliation $F$ , a leaf $L$ with $x \in L$ , a local transversal $T$ at $x$ , the holonomy representation $ρ_{x}$ with kernel $K = \ker ρ_{x}$ , and the holonomy cover $p : \hat{L} \to L$ with base point $\hat{x}$ over $x$ .

[F1]

The holonomy cover is the connected covering $p : \hat{L} = \tilde{L} / K \to L$ associated with $K = \ker ρ_{x}$ , where $\tilde{L} \to L$ is the universal cover, so that $p_{*} π_{1} (\hat{L}, \hat{x}) = K$ ; $K$ is normal in $π_{1} (L, x)$ because it is a kernel (The holonomy cover of a leaf, The covering of a leaf associated with the holonomy kernel exists, The homomorphism on fundamental groups induced by a pointed continuous map).

[F2]

The deck group of the universal cover of $L$ is isomorphic to $π_{1} (L, x)$ , and a covering of a path-connected, locally path-connected base with $p_{*} π_{1} (\hat{L}, \hat{x}) = K$ normal is regular, with $Deck (p) ≅ π_{1} (L, x) / K$ (A connected covering is regular exactly when its induced subgroup is normal, exactly when deck transformations act transitively on a fibre, For a path-connected locally path-connected semilocally simply connected base, the deck group of a universal cover is isomorphic to the fundamental group, A regular connected covering has deck group $π_{1} (B, b_{0}) / p_{*} π_{1} (E, e_{0})$ , Deck transformations and the deck-transformation group of a covering, Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

The holonomy group is $Hol (L, x) = ρ_{x} (π_{1} (L, x))$ , and $K = \ker ρ_{x}$ ; the first isomorphism theorem gives $π_{1} (L, x) / K ≅ Hol (L, x)$ (The holonomy representation and the holonomy group of a leaf, First isomorphism theorem for groups: $G / \ker f ≅ im f$ ).

[F4]

The deck group of a covering acts by a covering-space action, deck transformations are determined by their value at one point and act freely, and a connected regular covering has its deck group acting freely and transitively on each fibre, so its number of sheets is the order of that group (The deck group of a connected covering acts by a covering-space action, On a connected covering space, a deck transformation is determined by one point and the deck action is free).

[F5]

The library product traverses the first loop before the second, and transports satisfy $h_{a * b} = h_{b} \circ h_{a}$ and $h_{a^{- 1}} = h_{a}^{- 1}$ (Based loops and the fundamental group, Holonomy respects path concatenation and reversal).

Proof

technique · direct

1.1F1F2F5

(Convention and kernel.) By F5, $ρ_{x} ([a]) = h_{a^{- 1}}$ satisfies $ρ_{x} ([a] [b]) = ρ_{x} ([a]) \circ ρ_{x} ([b])$ . Its image is the same set of transport germs as the forward assignment, and its kernel is the same subgroup $K$ , because taking inverses preserves the identity. Therefore the holonomy cover of F1 is still the connected cover associated to this normal kernel. The universal-cover deck convention of F2 prepends $a$ to a path when applying the deck transformation associated with $[a]$ . Consequently the deck transformation corresponding to the germ $h_{γ} = ρ_{x} ([γ^{- 1}])$ prepends $γ^{- 1}$ . This fixes the precise convention consumed by the normal model.

2.1F2F3F4step 1.1

(The deck group.) Since $p_{*} π_{1} (\hat{L}, \hat{x}) = K$ is normal in $π_{1} (L, x)$ , the covering $p$ is regular and [F2] gives $Deck (p) ≅ π_{1} (L, x) / K$ [F1, F2]. By the first isomorphism theorem applied to the holonomy representation, $π_{1} (L, x) / K ≅ ρ_{x} (π_{1} (L, x)) = Hol (L, x)$ [F3]. Hence $Deck (p) ≅ Hol (L, x)$ , the deck action is faithful by the determination property [F4].

3.1F2F4step 2.1

(Quotient and finite degree.) Regularity in step 2.1 makes the deck group transitive on each covering fibre, and F4 makes its action free. Thus each fibre is a torsor for $Deck (p)$ , its quotient is $L$ , and the induced quotient topology agrees with that of $L$ in covering trivializations. The deck action is a covering-space action by F4. If $H$ is finite, every fibre has exactly $∣ H ∣$ points, so $p$ is a finite-sheeted cover of that degree.

4.1F3F4step 3.1

(The diagonal action.) The germs of $H$ act on the transversal $T$ through $ρ_{x}$ , and when they are realized on a common invariant transverse neighbourhood $D$ the formula $h \cdot (\hat{y}, t) : = (h \hat{y}, h t)$ defines an action of $H$ on $\hat{L} \times D$ preserving the product foliation by the slices. It is free: if $h \cdot (\hat{y}, t) = (\hat{y}, t)$ , then $h$ fixes $\hat{y}$ , so $h$ is the identity deck transformation by freeness of the deck action [F4]. It is a covering-space action, being the product of the covering-space action on $\hat{L}$ and any action on $D$ : a deck-separating neighborhood $V$ gives the neighborhood $V \times D$ whose nonidentity translates are disjoint [F4]. This is the diagonal model used by the finite-holonomy normal construction.

5.1step 1.1step 2.1step 3.1step 4.1∎

Therefore the deck group of the holonomy cover is the holonomy group, the deck action is a covering-space action with quotient $L$ , and the diagonal action on $\hat{L} \times D$ is free and a covering-space action; for finite $H$ the cover is finite-sheeted of degree $∣ H ∣$ .

Depends on

Used by

Dependency tree · two levels

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