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 velocity field of an isotopy is well defined along its image

Statement

Let $M$ be a compact smooth manifold, let $N$ be a smooth manifold and let $F : M \times I \to N$ be a smooth isotopy of embeddings with track $\overline{F}$ and $S : = \overline{F} (M \times I) \subseteq N \times I$ (Smooth isotopies, diffeotopies and ambient isotopies). Then:

$\overline{F}$ is a smooth embedding and its image $S$ is closed and diffeomorphic to $M \times I$ . Here embedding and diffeomorphism use the local coordinate-extension convention of the isotopy definition. The domain $M \times I$ has product corners at $\partial M \times {0, 1}$ when $M$ has boundary, and $S$ carries the corresponding embedded track charts. If $\partial M = \emptyset$ , only the time-endpoint boundary faces occur. No neatness relative to the boundary faces of $N \times I$ is asserted.
The horizontal velocity $Y$ , well defined by $Y (F (x, t), t) : = d F_{(x, t)} (0, \partial_{t}) \in T_{F (x, t)} N \subseteq T_{(F (x, t), t)} (N \times I),$ is a smooth horizontal field along $S$ : its pullback by $\overline{F}$ is smooth up to the time endpoints, it takes values in the subbundle $T N \oplus 0$ , and it satisfies $d {\overline{F}}_{(x, t)} (\partial_{t}) = (Y (\overline{F} (x, t)), \partial_{t})$ .
If $F$ takes values in $\partial N$ , then $Y$ takes values in the subbundle $T (\partial N)$ ; if $F$ takes values in the interior of $N$ , then so does the base point of $Y$ .

No orientation, properness or injectivity beyond that of the isotopy is used, and no choice principle is needed.

Facts & Assumptions

Given: A compact smooth manifold $M$ , a smooth manifold $N$ , a smooth isotopy of embeddings $F : M \times I \to N$ , its track $\overline{F}$ and the set $S = \overline{F} (M \times I)$ .

[F1]

$F$ is smooth, each slice $F_{t}$ is a smooth embedding, and $\overline{F} (x, t) = (F (x, t), t)$ ; the horizontal velocity is defined by the displayed formula, $\partial_{t}$ denoting the standard unit tangent vector on the $I$ factor (Smooth isotopies, diffeotopies and ambient isotopies, The differential of a smooth map).

[F2]

A smooth embedding is an injective immersion and a homeomorphism onto its image with the subspace topology (Smooth embeddings); a tangent vector in $T_{(x, t)} (M \times I)$ is a pair of components in $T_{x} M$ and $T_{t} I$ (The tangent bundle as a disjoint union).

[L2]

The boundaryless embedding-image and product results do not themselves apply at $t = 0, 1$ . Smoothness at source boundary faces and time endpoints means local smooth extension of coordinate functions across these faces (Smooth maps between manifolds with boundary). The local inverse needed here is established in step 2.2 using The smooth inverse function theorem on manifolds.

[L4]

Use product coordinates $(u, t)$ on $M \times I$ , with smooth local extensions across source boundary faces and time endpoints. Smoothness and product differentials are computed componentwise in these coordinates, exactly as for the boundaryless product results (Products of smooth manifolds have a canonical product smooth structure, A map into a product is smooth iff its components are smooth).

[L5]

For smooth $G, H$ one has $d (H \circ G)_{p} = d H_{G (p)} \circ d G_{p}$ (The chain rule for differentials of smooth maps), and the diagonal entry of a product differential is computed componentwise. Smooth maps are continuous (Smooth maps are continuous).

[L6]

Compact subsets admit finite subcovers from ambient open covers (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it). The interval $I = [0, 1]$ is compact and a finite product of compact spaces is compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, A product of finitely many compact spaces is compact in the product topology); a smooth manifold is Hausdorff, a compact subset of a Hausdorff space is closed, and a closed subset of a compact space is compact (Smooth manifolds and their smooth charts, In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L7]

In a boundary chart of $N$ the boundary stratum is the coordinate hyperplane of last coordinate $0$ and the interior is the open half-space of last coordinate $> 0$ (Interior and boundary of a manifold with boundary, Smooth maps between manifolds with boundary).

Proof

technique · direct

1.1F1F2L4

The track $\overline{F}$ is smooth by [L4], its two components being $F$ and the projection $M \times I \to I$ , which are smooth. It is injective: if $\overline{F} (x, t) = \overline{F} (x^{'}, t^{'})$ then reading the second coordinate gives $t = t^{'}$ and the first gives $F_{t} (x) = F_{t} (x^{'})$ , so $x = x^{'}$ because $F_{t}$ is injective by [F2].

1.2F1F2L5

The track is an immersion. Let $(v, a) \in T_{x} M \oplus T_{t} I$ satisfy $d {\overline{F}}_{(x, t)} (v, a) = 0$ . Applying $d π_{I}$ and [L5] to $π_{I} \circ \overline{F} = {p r}_{I}$ gives $a = 0$ ; then applying $d π_{N}$ to $π_{N} \circ \overline{F} = F$ gives $d (F_{t})_{x} (v) = 0$ , so $v = 0$ because $F_{t}$ is an immersion. Hence $d {\overline{F}}_{(x, t)}$ is injective for every $(x, t)$ .

2.1L5L6step 1.1

The track is proper: $M \times I$ is compact by [L6] and $\overline{F}$ is continuous by [F1] and [L5]. For a compact $K \subseteq N \times I$ , the target being Hausdorff by [L6], $K$ is closed, so ${\overline{F}}^{- 1} (K)$ is closed in the compact space $M \times I$ and hence compact by [L6].

2.2L2L6step 1.1step 1.2construct

A continuous injective map from the compact space $M \times I$ into the Hausdorff space $N \times I$ is a homeomorphism onto its image: it sends closed sets to compact, hence closed, sets by [L6]. With step 1.2 this makes the track an embedding. For its smooth inverse, choose source coordinates $u$ in a Euclidean open set or half-space of dimension $\dim M$ and target coordinates $y$ near one track point. Select $\dim M$ target components $p (y)$ for which $D_{u} (p \circ F)$ is invertible. The map $(u, t) \mapsto (p (F (u, t)), t)$ has invertible block differential. Locally extend its coordinate functions across any source boundary face and time endpoint and apply [L2]'s inverse function theorem in Euclidean open sets. Its smooth inverse recovers $(u, t)$ from $(p (y), t)$ along the track. The other target components are smooth functions of these coordinates, giving the local graph model and the smooth inverse on $S$ , including its source boundary and endpoint faces and their intersections. If $N$ has boundary, extend its coordinate functions in Euclidean space for this calculation and then restrict back; no neatness or boundaryless slice theorem is invoked. Finally $S$ is compact and therefore closed by [L6].

3.1F2step 1.1step 2.2

The velocity $Y$ is well defined: a point of $S$ has the form $\overline{F} (x, t)$ for a unique $(x, t)$ , because $\overline{F}$ is injective by step 1.1, so the prescription $Y (\overline{F} (x, t)) : = d F_{(x, t)} (0, \partial_{t})$ is independent of choices; this value lies in $T_{F (x, t)} N$ seen inside $T_{(F (x, t), t)} (N \times I)$ by [F2].

4.1L2L4step 2.2step 3.1

On $S$ one has $Y = V \circ {\overline{F}}^{- 1}$ , where $V (x, t) : = d F_{(x, t)} (0, \partial_{t})$ . The inverse is smooth in the local graph coordinates of step 2.2. The target components of $V$ are time partial derivatives of the coordinate functions of $F$ , hence are smooth, including at product corners by differentiating their local extensions. Thus $Y$ is smooth along $S$ in the stated local-extension sense.

4.2L5F1step 3.1

The tangent identity $d {\overline{F}}_{(x, t)} (\partial_{t}) = (Y (\overline{F} (x, t)), \partial_{t})$ holds: by [L5] applied to the two components $π_{N} \circ \overline{F} = F$ and $π_{I} \circ \overline{F} = {p r}_{I}$ , the first component of $d {\overline{F}}_{(x, t)} (\partial_{t})$ is $d F_{(x, t)} (0, \partial_{t}) = Y (\overline{F} (x, t))$ and the second is $d {p r}_{I} (\partial_{t}) = \partial_{t}$ .

5.1step 3.1step 4.1step 4.2

Consequently $Y$ is a smooth field along the closed track, takes values in $T N \oplus 0$ by construction, and satisfies the tangent identity of step 4.2; this is clause 2.

6.1F1L7step 3.1∎

Assume $F$ takes values in $\partial N$ . Fix $(x, t) \in M \times I$ and a boundary chart of $N$ at $F (x, t)$ with last coordinate $u_{n}$ ; by [L7] the last coordinate of the curve $s \mapsto F (x, s)$ is identically $0$ near $s = t$ , so its derivative, which is the $T N$ -component $Y (\overline{F} (x, t))$ of the velocity, has last coordinate $0$ and therefore lies in $T (\partial N)$ . If instead $F$ takes values in the interior of $N$ , then the base point $F (x, t)$ of $Y (\overline{F} (x, t))$ lies in the interior by hypothesis. This is clause 3.

Depends on

Used by

Dependency tree · two levels

94 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.