LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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.

The first essential loop in a transverse family is a vanishing cycle

Statement

Assume Countable Choice ${A C}_{ω}$ . Let $H_{t} : S^{1} \to M$ , $0 \leq t \leq 1$ , be a jointly $C^{2}$ family whose loops lie in leaves and whose point tracks are transverse to a $C^{2}$ cooriented codimension-one foliation. If $H_{0}$ is null-homotopic in its leaf and $H_{1}$ is nontrivial in its leaf, there is a parameter $t_{*} \in (0, 1]$ such that $H_{t}$ is null-homotopic for every $t < t_{*}$ and $H_{t_{*}}$ is nontrivial. After reparametrization, $(H_{t})_{0 \leq t \leq t_{*}}$ is a vanishing cycle and its endpoint determines a nonzero class in the limitwise-nullhomotopy subgroup on the approached side.

Facts & Assumptions

Given: A jointly $C^{2}$ family $H_{t} : S^{1} \to M$ , $0 \leq t \leq 1$ , whose loops lie in leaves of a $C^{2}$ cooriented codimension-one foliation and whose point tracks are transverse, with $H_{0}$ null-homotopic in its leaf and $H_{1}$ nontrivial in its leaf.

[F1]

A vanishing cycle supported on a leaf $L_{1}$ is a jointly $C^{2}$ family of loops lying in leaves with $[σ_{1}]$ nonzero, earlier loops null-homotopic in their leaves, and transverse point tracks, and it determines a nonzero class in the appropriate limitwise-nullhomotopy subgroup. (Vanishing cycles of a codimension-one foliation).

Proof

technique · direct

1.1given

Let $S$ be the set of parameters $s$ such that every loop $H_{t}$ with $0 \leq t \leq s$ is null-homotopic in its leaf; the loop $H_{0}$ has a compact null-homotopy, and the persistence result for compact transverse deformations (lem-nullhomotopy-persists-under-a-compact-transverse-deformation) transports it to nearby loops of the family, so $S$ contains a positive interval.

2.1step 1.1

Let $t_{*} = \sup S$ , which lies in $(0, 1]$ ; for every $t < t_{*}$ the definition of supremum gives $s \in S$ with $s > t$ , hence $H_{t}$ is null-homotopic in its leaf.

3.1step 2.1

If $t_{*} < 1$ and $H_{t_{*}}$ were null-homotopic, the compact-disk persistence lemma would make the loops null-homotopic on a right-hand interval of $t_{*}$ , contradicting the supremum; if $t_{*} = 1$ then nontriviality of $H_{1}$ is the hypothesis, so in either case $H_{t_{*}}$ is nontrivial in its leaf.

4.1F1step 3.1∎

After reparametrizing the restricted family $(H_{t})_{0 \leq t \leq t_{*}}$ one obtains a vanishing cycle in the sense of [F1], and the bridge result that a vanishing cycle determines a nontrivial limitwise-nullhomotopy class (A vanishing cycle determines a nonzero limitwise-nullhomotopy class) gives the nonzero class in $Π_{1}^{j}$ on the approached side; only the standing countable choice is used.

Depends on

Used by

Dependency tree · two levels

26 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

S. P. Novikov, The Topology of Foliations (English translation by J. A. Zilber; complete PDF of the translation) (standard reference, not scraped)