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 normal model map is a foliated local diffeomorphism

Statement

Assume ${A C}_{ω}$ (The countable-choice principle used in the foliation pair). In the situation of Transverse holonomy transport is well defined and equivariant on the model, the map $Φ$ is $H$ -equivariant, so it descends to a smooth map $\overline{Φ} : N = (\hat{L} \times D) / H ⟶ M, \overline{Φ} ([(\hat{y}, t)]) : = Φ (\hat{y}, t) .$ Then: (i) $\overline{Φ}$ maps leaves of the model foliation into leaves of $F$ ; (ii) $\overline{Φ}$ is a local diffeomorphism; (iii) the differential of $\overline{Φ}$ is invertible at every point of the central leaf and induces the canonical identification of the central leaf with $L$ ; (iv) $\overline{Φ}$ is a foliated local diffeomorphism, carrying the model foliation locally onto $F$ .

Facts & Assumptions

Given: The setting of the model map $Φ : \hat{L} \times D \to M$ , its diagonal $H$ -invariance, and the model $N = (\hat{L} \times D) / H$ .

[F1]

The map $Φ$ is well defined, smooth and invariant under the diagonal action of $H$ ; hence it descends to a smooth map $\overline{Φ} : N \to M$ ; the central leaf of the model is the image of $\hat{L} \times {x}$ and is canonically diffeomorphic to $L$ (Transverse holonomy transport is well defined and equivariant on the model, The finite-holonomy normal model of a compact leaf, The quotient foliation under a free and properly discontinuous foliated action).

[F2]

Each map $t \mapsto Φ (\hat{y}, t)$ is a transverse transport along a leafwise path, hence a germ of a local diffeomorphism of the transversal, and the maps $Φ (\cdot, t)$ are obtained by plaque transport inside the leaves of $F$ (Transverse holonomy transport is well defined and equivariant on the model, Finite holonomy acts on a small transverse disk).

[F3]

A smooth map whose differential is invertible at a point is a local diffeomorphism near that point (The smooth inverse function theorem on manifolds, Diffeomorphisms and local diffeomorphisms of manifolds, Smooth manifolds and their smooth charts).

Proof

technique · direct

1.1F1F2

(Descent and mapping of leaves.) By [F1] the $H$ -invariance of $Φ$ descends it to the smooth map $\overline{Φ}$ on the model, and on the central leaf $\overline{Φ}$ restricts to the canonical identification with $L$ . Each slice $\hat{L} \times {t}$ is carried by $Φ$ into the leaf of $F$ through $t$ by plaque transport [F2], and the model leaves are exactly the images of the slices [F1]; hence $\overline{Φ}$ maps model leaves into leaves of $F$ .

1.2F1F2

(Invertible differential along the central leaf.) At a central point $(\hat{y}, x)$ the derivative of $\overline{Φ}$ restricted to the leaf direction is the derivative of the covering $p$ at $\hat{y}$ , which is invertible because a covering is a local diffeomorphism [F1]. In the transverse direction the derivative is the derivative at $t = x$ of the transport germ $t \mapsto Φ (\hat{y}, t)$ , which is invertible because it is a germ of a local diffeomorphism [F2]. The leaf direction and the transverse direction are complementary: the transversal $T$ is transverse to the plaques by the definition of a local transversal, and their images span $T_{Φ (\hat{y}, x)} M$ . Hence $d \overline{Φ}$ is invertible at every central point, and by continuity it stays invertible on a neighbourhood of the central leaf.

2.1F2F3step 1.1step 1.2

(Local diffeomorphism everywhere.) For an arbitrary point $[(\hat{y}, t)]$ of the model, the same argument applies with the slice through $t$ in place of the central slice: the leafwise direction is given by plaque transport along the leaf through $t$ , a local diffeomorphism, and the transverse direction by the transport germ $t \mapsto Φ (\hat{y}, t)$ at the corresponding point, which is a germ of a local diffeomorphism, and the two directions are complementary because plaque directions and transverse directions are complementary everywhere by [F2]. Therefore $d \overline{Φ}$ is invertible at every point and $\overline{Φ}$ is a local diffeomorphism by [F3]. It carries the model foliation locally onto the foliation $F$ because it is a local diffeomorphism mapping model leaves into leaves [F3, step 1.1].

3.1step 1.1step 1.2step 2.1∎

The descended map $\overline{Φ}$ is a smooth map of the model to $M$ that carries leaves to leaves, is a local diffeomorphism everywhere, restricts to the canonical identification of the central leaf with $L$ , and is therefore a foliated local diffeomorphism.

Depends on

Used by

The normal model map restricts to a diffeomorphism onto a saturated neighbourhood Lemma

Dependency tree · two levels

57 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

Ieke Moerdijk and Janez Mrčun, Introduction to Foliations and Lie Groupoids (Cambridge Studies in Advanced Mathematics 91, 2003) (standard reference, not scraped)
Matias del Hoyo and Rui Loja Fernandes, On deformations of compact foliations (Proc. AMS 147, 2019, 4555–4561) (standard reference, not scraped)