PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck 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.

Suspension holonomy is the germ of the represented monodromy action

Statement

Assume Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). In the suspension $M_{ρ}$ of a representation $ρ : π_{1} (B, b_{0}) \to Diff (F)$ as in The suspension foliation of a representation of the fundamental group let $γ : [0, 1] \to B$ be a loop at $b_{0}$ with class $[γ] \in π_{1} (B, b_{0})$ , let $\tilde{x} = {\tilde{b}}_{0}$ be the fixed point of $\tilde{B}$ used for the deck identification in that definition, let ${\tilde{x}}_{γ}$ be the lift of $γ$ with ${\tilde{x}}_{γ} (0) = \tilde{x}$ , so that ${\tilde{x}}_{γ} (1) = [γ] \cdot \tilde{x}$ Based loops and the fundamental group, and let $y \in F$ . Then $a (t) : = π ({\tilde{x}}_{γ} (t), y)$ is a leafwise path of $F_{ρ}$ , and its holonomy germ between the local transversal $T = π ({\tilde{x}} \times F)$ at the start and the corresponding slice at the end is the germ at $y$ of $ρ ([γ])^{- 1}$ : $h_{a} = {germ}_{y} (ρ ([γ])^{- 1}) .$ Moreover the leaf $L_{y} = π (\tilde{B} \times {y})$ is diffeomorphic to $\tilde{B} / K_{y}$ with $K_{y} = {γ : ρ (γ) y = y}$ the stabiliser of $y$ , and under $π_{1} (L_{y}) ≅ K_{y}$ the holonomy representation of the leaf (as a homomorphism with traversal-order loop multiplication) is $γ \mapsto {germ}_{y} (ρ (γ))$ . The forward-path holonomy is the inverse germ. Both maps have the same image and kernel.

Facts & Assumptions

Given: A representation $ρ$ of $π_{1} (B, b_{0})$ in the diffeomorphism group of $F$ , the diagonal action on $\tilde{B} \times F$ , the quotient $M_{ρ} = (\tilde{B} \times F) / π_{1} (B, b_{0})$ with orbit map $π$ and suspension foliation $F_{ρ}$ , a loop $γ$ at $b_{0}$ , a point $\tilde{x} \in \tilde{B}$ over $b_{0}$ , its lift ${\tilde{x}}_{γ}$ with ${\tilde{x}}_{γ} (1) = [γ] \cdot \tilde{x}$ , and a point $y \in F$ .

[F1]

In the suspension the quotient $M_{ρ}$ is a smooth manifold, $π$ is a covering map and a local diffeomorphism, and the product foliation of $\tilde{B} \times F$ with leaves $\tilde{B} \times {y^{'}}$ descends to the regular foliation $F_{ρ}$ whose leaves are the images of those product leaves (The suspension foliation of a representation of the fundamental group, The quotient foliation under a free and properly discontinuous foliated action).

[F2]

The slice ${\tilde{x}} \times F$ is a local transversal to the product foliation at each of its points: the product foliation has tangent distribution $T \tilde{B} \times {0}$ and the slice has tangent space ${0} \times T F$ , a complementary direct summand (Local transversals to a regular foliation, Plaques of a flat chart).

[F3]

In a product chart of the product foliation the plaques keep the $F$ -coordinate fixed, so the transport between two slices of the form ${{\tilde{x}}_{0}} \times F$ and ${{\tilde{x}}_{1}} \times F$ along a leafwise path in a leaf $\tilde{B} \times {y}$ keeps the second coordinate: it sends $({\tilde{x}}_{0}, y_{0})$ to $({\tilde{x}}_{1}, y_{0})$ (The holonomy germ is independent of the foliation chart chain, Plaques of a flat chart).

[F4]

The $π_{1} (B, b_{0})$ -action on $\tilde{B} \times F$ is diagonal, $γ_{0} \cdot ({\tilde{x}}_{0}, y_{0}) = (γ_{0} {\tilde{x}}_{0}, ρ (γ_{0}) y_{0})$ , so $(γ_{0} {\tilde{x}}_{0}, y_{0})$ and $({\tilde{x}}_{0}, ρ (γ_{0})^{- 1} y_{0})$ lie in the same orbit, and $π$ identifies them; moreover $π ({\tilde{x}}_{0}, y_{0}) = π ({\tilde{x}}_{1}, y_{1})$ holds exactly when $({\tilde{x}}_{1}, y_{1}) = γ_{0} \cdot ({\tilde{x}}_{0}, y_{0})$ for some $γ_{0}$ (The suspension foliation of a representation of the fundamental group, The quotient foliation under a free and properly discontinuous foliated action).

[F5]

Holonomy germs are well defined, invariant under leafwise homotopy relative to endpoints, and multiplicative under concatenation (The holonomy germ is independent of the foliation chart chain, Holonomy depends only on leafwise homotopy relative to endpoints, Holonomy respects path concatenation and reversal).

[F7]

Intrinsic leaves are integral immersions with plaque charts (Existence and uniqueness of maximal connected integral manifolds). With traversal-order loop multiplication, the holonomy representation uses the inverse of forward-path holonomy (The holonomy representation and the holonomy group of a leaf).

[F6]

For a covering-space action of a group $G$ on a path-connected space $E$ the orbit map $E \to E / G$ is a covering whose deck group consists exactly of the transformations supplied by $G$ ; for a universal cover the deck group is isomorphic to the fundamental group of the base, the isomorphism moving a chosen fibre point to the lifted endpoint of the corresponding loop (The orbit map of a covering-space action is a covering, with the acting group equal to the deck group when the total space is path-connected, For a path-connected locally path-connected semilocally simply connected base, the deck group of a universal cover is isomorphic to the fundamental group, Universal covering spaces).

Proof

technique · direct

1.1F1F2construct

The lifted path is leafwise. The path $\tilde{t} \mapsto ({\tilde{x}}_{γ} (t), y)$ lies in the product leaf $\tilde{B} \times {y}$ ; applying the local diffeomorphism $π$ by [F1] gives a leafwise path $a (t) = π ({\tilde{x}}_{γ} (t), y)$ of $F_{ρ}$ . Both $T = π ({\tilde{x}} \times F)$ and the end slice $π ({{\tilde{x}}_{γ} (1)} \times F) = π ({[γ] \tilde{x}} \times F)$ are local transversals to $F_{ρ}$ at the endpoints, being local diffeomorphic images of the transversals of [F2].

1.2F3

Transport upstairs. In the product foliation the transport along the path $t \mapsto ({\tilde{x}}_{γ} (t), y)$ from the slice ${\tilde{x}} \times F$ to the slice ${{\tilde{x}}_{γ} (1)} \times F$ keeps the $F$ -coordinate by [F3]: a point $(\tilde{x}, y_{0})$ is sent to $({\tilde{x}}_{γ} (1), y_{0})$ .

1.3F1F4F6F7construct

The leaf through $y$ . The restriction $\tilde{B} \times {y} \to M_{ρ}$ is tangent to the descended distribution. In the quotient's local product charts it maps into plaque neighborhoods of the intrinsic leaf $L_{y}$ , so it factors smoothly as $Φ : \tilde{B} \to L_{y}$ and is a local diffeomorphism between manifolds of dimension $\dim B$ by [F7]. By [F4], its fibres are exactly the $K_{y}$ -orbits. The group $K_{y}$ acts freely and properly discontinuously on $\tilde{B}$ by the deck action; the quotient proposition supplies its smooth quotient and orbit local diffeomorphism. Hence $Φ$ descends to a bijective local diffeomorphism $\tilde{B} / K_{y} \to L_{y}$ , and is a diffeomorphism. In particular $\tilde{B} \to L_{y}$ is the corresponding orbit covering.

2.1F1F3F4step 1.1step 1.2

Descending the transport. In $M_{ρ}$ the point $({\tilde{x}}_{γ} (1), y_{0}) = ([γ] \tilde{x}, y_{0})$ is identified by [F4] with $(\tilde{x}, ρ ([γ])^{- 1} y_{0})$ . Since $π$ is a local diffeomorphism and the holonomy germ of $a$ is computed by transporting along the descended local product structure, which is the corresponding chart-wise transport, the holonomy germ $h_{a}$ satisfies, after identifying both the start and the end transversal with $F$ through the maps $y_{0} \mapsto π (\tilde{x}, y_{0})$ , $h_{a} = {germ}_{y} (y_{0} \mapsto ρ ([γ])^{- 1} y_{0}) .$

2.2F6step 1.3

The fundamental group of the leaf. The group $K_{y}$ acts on $\tilde{B}$ by a covering-space action (the restriction of the deck action, which consists of homeomorphisms over $B$ ) and $\tilde{B}$ is path-connected and simply connected, being a universal cover; the covering $\tilde{B} \to \tilde{B} / K_{y} ≅ L_{y}$ is then a universal cover of $L_{y}$ whose deck group consists exactly of the transformations from $K_{y}$ by [F6]. Hence $π_{1} (L_{y}) ≅ K_{y}$ .

3.1F5F7step 1.3step 2.1step 2.2

The holonomy representation of the leaf. For $γ \in K_{y}$ , the projected path associated to a based loop representing $γ$ closes because $ρ (γ) y = y$ , and corresponds to $γ$ under step 2.2. Its forward holonomy is ${germ}_{y} (ρ (γ)^{- 1})$ by step 2.1. The representation in [F7] uses the reversed loop, and thus takes the inverse germ, namely ${germ}_{y} (ρ (γ))$ . This is a homomorphism on $K_{y}$ ; the unreversed transport is an antihomomorphism.

4.1step 1.1step 2.1step 1.3step 2.2step 3.1∎

Conclusion. Steps 1.1 and 2.1 give the stated holonomy germ $h_{a} = {germ}_{y} (ρ ([γ])^{- 1})$ of a base loop, and steps 1.3, 2.2 and 3.1 give the description of the leaf $L_{y}$ as $\tilde{B} / K_{y}$ together with its holonomy representation.

Depends on

Used by

Dependency tree · two levels

81 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)
Eckhard Meinrenken, Lie Groupoids and Lie Algebroids, lecture notes (University of Toronto MAT1341, Fall 2017) (standard reference, not scraped)