Alphabeta Math
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.

Transverse holonomy transport is well defined and equivariant on the model

Statement

Assume ACω. Let F be a smooth regular foliation of M, let L be a compact leaf, let x∈L, and suppose its holonomy group H is finite. Let p:L^→L be the holonomy cover with the left deck identification of The deck group of the holonomy cover is the holonomy group. Choose a tubular projection onto L, whose fibre Tx is the endpoint transversal at x, and realize H on an invariant disk D⊆Tx as in Finite holonomy acts on a small transverse disk. After shrinking D, there is a smooth map Φ:L^×D→M with Φ(y^,x)=p(y^), Φ(hy^,ht)=Φ(y^,t), and with each slice L^×{t} mapped into the leaf through t. Locally in y^, the map is represented by plaque transport to the tubular fibre at p(y^); its germ depends only on the path class represented by y^. Its actual values on D are furnished by a compatible finite family of representatives. Arbitrary transport representatives of equal germs need not agree on all of D; no assertion that every arbitrarily chosen path chain is defined there is made.

Facts & Assumptions

Given: The compact smooth leaf, finite holonomy, fixed tubular endpoint fibres, holonomy cover and the stated choice assumption.

[F2]

With reversed-loop holonomy and left deck multiplication, the deck element corresponding to the forward germ hγ prepends γ−1. The holonomy cover of a compact finite-holonomy leaf is finite-sheeted (The deck group of the holonomy cover is the holonomy group).

[F3]

A finite germ group has a smooth action on an invariant disk, conjugate by the averaged coordinate k to its derivative action (Finite holonomy acts on a small transverse disk, proof step 3.1).

[F4]

Crainic–Mărcuț, Reeb–Thurston stability for symplectic foliations, §2, Lemma 1, PDF pp. 5–7, establishes a foliated diffeomorphism from an open neighborhood of the central leaf in the finite linear-holonomy model onto an open neighborhood of an embedded finite-holonomy leaf. Its complete proof constructs the map by transport between fixed tubular fibres. It uses domains On for chains of length at most n, verifies representative comparisons on those domains and proves H~(y^g,h(g−1)v)=H~(y^,v) for its right-deck/forward-transport convention. This external lemma, not just the statement of classical Reeb stability, is the construction input here.

[F5]

A closed smooth embedded submanifold has a tubular neighborhood under ACω (The tubular neighbourhood theorem in a smooth ambient manifold). A continuous injective immersion with compact intrinsic source into a Hausdorff manifold is embedded: compact images of closed subsets are closed, so the inverse onto its image is continuous (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Proof

technique · use the fully proved external construction with explicit conventions
1.1F1F5

The smooth plaque charts make the inclusion of L an injective immersion. Its intrinsic compactness and ambient Hausdorffness give an embedding by F5; compactness also makes its image closed. Choose a tubular neighborhood by F5 and shrink it so its fibres are transverse to the foliation, which holds along L and persists nearby. This specifies the endpoint transversals required by F1.

1.2F2F3F4

Apply F4 to this tubular setting. It gives a foliated map on an open neighborhood of the zero section in the linear model. Compactness of the finite cover L^ gives a common transverse ball inside the lifted domain: finitely many product neighborhoods covering L^×{0} suffice, and the intersection of their transverse neighborhoods contains a ball. Make this ball invariant by averaging an inner product over the finite derivative action. Conjugate back using F3, whose coordinate k has identity derivative. Thus the external construction supplies compatible actual representatives on L^×D, rather than promoting infinitely many unrelated germ equalities to a uniform-domain equality.

2.1F1F2F4step 1.2

In the source convention the right deck action prepends γ and pairs it with inverse forward transport. Our left deck element h=hγ prepends γ−1 by F2. Substituting g corresponding to γ−1 into the source formula gives Φ(hy^,ht)=Φ(y^,t). A chosen local transport family follows the leaf from the initial point t, so its image lies in that leaf. Source transport is between the specified tubular fibres, and F1 identifies its local germ with the path class represented by y^.

3.1F2F4step 1.2step 2.1∎

On the zero slice the construction is fixed on L, so Φ(y^,x)=p(y^). Its smoothness, leafwise property, actual diagonal invariance and compatible local transport representatives follow from the external construction and steps 1.2–2.1. It therefore descends to a smooth map on (L^×D)/H.

Depends on

Used by

Dependency tree · two levels

89 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