LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck 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 extends to a neighbourhood

Statement

Assume ${A C}_{ω}$ . Let $M$ be a compact smooth manifold, $N$ a smooth manifold, $F : M \times I \to N$ a smooth isotopy of embeddings with track $S \subseteq N \times I$ and horizontal velocity $Y$ (The velocity field of an isotopy is well defined along its image). Then:

There are an open neighbourhood $Ω$ of $S$ in $N \times I$ and a smooth map $\tilde{Y} : Ω \to T N$ with $\tilde{Y} (y, t) \in T_{y} N$ and $\tilde{Y} ∣_{S} = Y$ .
If $N$ has boundary and $F$ takes values in $\partial N$ , then, after shrinking $Ω$ , the extension can be chosen tangent to $\partial N$ along $Ω \cap (\partial N \times I)$ ; if $F$ takes values in the interior, the extension can be chosen with values in $T (N ∖ \partial N)$ , which is its natural value on the part of $Ω$ lying over the interior.
For every open neighbourhood $W$ of $S$ in $N \times I$ there is such an extension with $Ω \subseteq W$ ; more generally, if $A \subseteq S$ is compact and ${\tilde{Y}}_{0}$ is a smooth extension of $Y$ defined on a neighbourhood of $A$ , the extension may be chosen to agree with ${\tilde{Y}}_{0}$ on a (possibly smaller) neighbourhood of $A$ . If boundary tangency is also required, the prescribed extension must satisfy that tangency on its domain.

The extension is horizontal: only the $T N$ component is prescribed or changed, not the unit time component.

Facts & Assumptions

Given: Countable choice, a compact smooth manifold $M$ , a smooth manifold $N$ , a smooth isotopy $F$ with track $S$ and horizontal velocity $Y$ .

[F1]

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 track is compact, closed and smoothly embedded, with local graph coordinates and smooth horizontal velocity up to the endpoint faces (The velocity field of an isotopy is well defined along its image, proof steps 2.2 and 4.1).

[L1]

The boundaryless field-extension lemma uses local coefficient extension and partitions of unity (A vector field along an embedded submanifold extends to a neighbourhood and globally when the submanifold is closed). Here steps 1.1 and 1.2 give that construction explicitly in product coordinates, including endpoint and ambient boundary faces.

[L3]

For the compact sets used here, a cutoff equal to one near the set and supported in a prescribed open set follows from finitely many Euclidean chart bumps, restricted to the product chart faces, as in step 1.1. Sum bumps equal to one on smaller neighbourhoods covering the compact set and compose with a smooth scalar cutoff equal to one above $1 / 2$ . This proves the needed product-corner version directly (A Euclidean bump for a compact set inside an open set); the ordinary versions are A smooth Urysohn lemma for a closed set in an open set and Smooth partitions of unity exist on manifolds with boundary.

[L4]

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$ ; a vector is tangent to the stratum exactly when its last coordinate vanishes (Interior and boundary of a manifold with boundary, Neat submanifolds of a manifold with boundary, Smooth vector bundles, rank, fibres, and trivial bundles).

[A1]

Countable choice is used exactly for the countable selections of cutoffs and partition-of-unity functions in [L1] and [L3]; no other selection occurs (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

A compact subset of a Hausdorff space is closed, and smooth maps are continuous (Smooth maps are continuous, Embedded submanifolds and slice charts).

Proof

technique · direct

1.1F1L1A1construct

In a product chart $(y, t)$ near a track point, the graph coordinates of [F1] give a smooth local inverse $(p (y), t) \mapsto (u (y, t), t)$ , where $p$ selects target coordinates. Extend the coordinate functions of $F$ locally across time endpoints and, if necessary, the target boundary chart. Define the $j$ th target component of a local field by $(\partial_{t} F^{j}) (u (y, t), t)$ . On the track it equals the $j$ th velocity component. Interpret these coefficients in the coordinate basis of $T N$ and assign zero time component; horizontality follows directly, without assuming slice charts preserve the horizontal subbundle. Take finitely many such chart domains covering compact $S$ . In their Euclidean extensions choose finitely many nonnegative smooth bumps with compact supports inside these domains by A Euclidean bump for a compact set inside an open set and positive sum near $S$ , and restrict them to $N \times I$ . Dividing each by their sum gives smooth weights summing to one on a neighbourhood $Ω$ of $S$ . The weighted sum of the local horizontal fields is smooth, horizontal and equals $Y$ on $S$ . These restricted coordinate bumps also handle the corners of $N \times I$ when $N$ has boundary. This proves clause 1.

2.1F1L4step 1.1construct

If $F$ takes values in $\partial N$ , perform the graph construction of step 1.1 first in the boundary coordinates $y^{'}$ , choosing $p$ from those coordinates, since the slice differential is injective into $T \partial N$ . Extend the tangential coefficients independently of the inward coordinate $y_{n}$ and set the $y_{n}$ component identically zero. Restricted product-chart bumps patch these fields as in step 1.1. Each is tangent to $\partial N$ there, so their sum is tangent too; boundary coordinate changes preserve this condition. If the track lies in the interior, restrict $Ω$ to $Int N \times I$ . These are the two alternatives of clause 2.

2.2step 1.1construct

For a prescribed open neighbourhood $W$ of $S$ , simply restrict the extension to $Ω^{'} : = Ω \cap W$ . This is an open neighbourhood of $S$ contained in $W$ ; no tubular theorem for a boundary or cornered track is required.

3.1F2L3L4step 2.2construct

Clause 3, relative form: let $A \subseteq S$ be compact and let ${\tilde{Y}}_{0}$ be a smooth extension of $Y$ defined on an open neighbourhood $Ω_{0}$ of $A$ (it agrees with $Y$ at every point of $S$ in its domain). The set $A$ is closed in the manifold $N \times I$ by [F2], and both $Ω^{'}$ from step 2.2 and $Ω_{0}$ are open neighbourhoods of $A$ ; by [L3] choose a smooth cutoff $χ$ equal to $1$ on a neighbourhood $A^{'} \subseteq Ω^{'} \cap Ω_{0}$ of $A$ with support in $Ω^{'} \cap Ω_{0}$ . Define ${\tilde{Y}}_{1} : = \tilde{Y} + χ ({\tilde{Y}}_{0} - \tilde{Y})$ on $Ω^{'} \cap Ω_{0}$ , extended by $\tilde{Y}$ outside $supp χ$ . This is a smooth map into $T N$ because the fibrewise vector-space operations of a smooth vector bundle are smooth in local trivialisations ([L4]), it agrees with ${\tilde{Y}}_{0}$ on $A^{'}$ and with $\tilde{Y}$ outside $supp χ$ , and it restricts to $Y$ on $S \cap Ω^{'}$ ; hence it is an extension of $Y$ agreeing with ${\tilde{Y}}_{0}$ near $A$ . When both fields are boundary-tangent, their blend is boundary-tangent too.

4.1step 1.1step 2.1step 2.2step 3.1∎

The constructions prove all three clauses. They modify only the horizontal component and preserve the stated relative and boundary conditions.

Depends on

Used by

Dependency tree · two levels

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