LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Germs of orientation-preserving diffeomorphisms of the line at zero are torsion-free

Statement

Every finite subgroup of the group ${Diff}_{0}^{+} (R, 0)$ of germs at $0$ of orientation-preserving local diffeomorphisms of $R$ fixing $0$ is trivial: if $h$ is such a germ and $h^{n} = i d$ in the group of germs for some $n \geq 1$ , then $h = i d$ . Equivalently, the group of germs of orientation-preserving local diffeomorphisms fixing a point of a one-dimensional manifold is torsion-free.

Facts & Assumptions

Given: A germ $h \in {Diff}_{0}^{+} (R, 0)$ and a positive integer $n$ with $h^{n} = i d$ in the group of germs.

[F1]

A germ of local diffeomorphisms of $R$ at $0$ fixing $0$ is an equivalence class of local diffeomorphisms $f : U \to V$ with $0 \in U$ , $f (0) = 0$ , two representatives being equivalent when they agree on a neighbourhood of $0$ ; the product is represented by the composite and the group structure is as in Germs of local diffeomorphisms at a point form a group (Germs of local diffeomorphisms at a point).

[F2]

Composition of representatives induces a well-defined associative operation with identity and inverses on ${Diff}_{0} (R)$ , so it is a group, and an element is the identity germ exactly when one (equivalently every) representative equals the identity on a neighbourhood of $0$ (Germs of local diffeomorphisms at a point form a group).

[F3]

A local diffeomorphism of $R$ is a $C^{\infty}$ map with $C^{\infty}$ local inverse; an orientation-preserving one fixing $0$ has positive derivative at $0$ and is therefore strictly increasing on a neighbourhood of $0$ (Diffeomorphisms and local diffeomorphisms of manifolds).

Proof

technique · direct

1.1F1F2F3

(A representative with controlled iterates.) By [F1, F2] choose a representative $h : I \to R$ defined on an open interval $I$ containing $0$ , with $h (0) = 0$ and $h$ orientation-preserving; by [F3] $h$ has positive derivative at $0$ and is strictly increasing on a neighbourhood of $0$ . Since $h^{n}$ is the identity germ, some neighbourhood of $0$ is mapped identically by $h^{n}$ [F2]. First shrink $I$ so $h$ is strictly increasing throughout $I$ . Continuity at the fixed point then gives an open interval $J ∋ 0$ so that $h^{n} = i d$ on $J$ and every iterate $h^{k} (J)$ , $0 \leq k \leq n$ , lies in $I$ [F1, F2, F3].

2.1F2F3step 1.1

(No displacement.) Suppose $h$ is not the identity germ. Then, by [F2], for every neighbourhood of $0$ there is a point $t$ of that neighbourhood with $h (t) \neq t$ . Choose such a point $t \in J$ . If $h (t) > t$ , then strict increase of $h$ on $I$ gives $h^{k + 1} (t) > h^{k} (t)$ for every $k < n$ , hence $h^{n} (t) > t$ , contradicting $h^{n} (t) = t$ ; if $h (t) < t$ , the same monotonicity gives $h^{k + 1} (t) < h^{k} (t)$ and $h^{n} (t) < t$ , again a contradiction. Hence no such $t$ exists and $h$ agrees with the identity on a neighbourhood of $0$ , that is, $h = i d$ as a germ.

3.1step 2.1

(Finite subgroups.) Let $H \leq {Diff}_{0}^{+} (R, 0)$ be a finite subgroup and let $h \in H$ . The cyclic subgroup generated by $h$ is contained in $H$ , hence finite, so $h^{k} = i d$ for some $k \geq 1$ ; step 2.1 applied with that $k$ gives $h = i d$ . Therefore every element of $H$ is the identity germ and $H$ is the trivial subgroup: the group of germs is torsion-free.

4.1step 3.1∎

For a one-dimensional manifold $T$ and $x \in T$ , choose a chart at $x$ ; a germ of an orientation-preserving local diffeomorphism of $T$ at $x$ is represented in this chart by a germ of an orientation-preserving local diffeomorphism of $R$ at $0$ , and composition and the identity are preserved by the chart change. Hence the same argument shows that the group of germs at $x$ is torsion-free.

Depends on

Used by

In a transversely oriented codimension-one foliation a compact leaf with finite fundamental group has trivial holonomy Lemma

Dependency tree · two levels

10 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)
Danny Calegari, Foliations and the Geometry of 3-Manifolds (Oxford Mathematical Monographs; complete author-hosted PDF) (standard reference, not scraped)