Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Isotopy extension for a compact source with boundary

Statement

Assume ACω (The Axiom of Countable Choice (ACω)). Let V be a compact smooth n-manifold with boundary and let N be a smooth n-manifold without boundary (Smooth manifolds and their smooth charts). Let F:V×I→N be a smooth map such that Ft:=F(⋅,t) is a smooth embedding for every t∈I (Smooth embeddings), and suppose F is constant near the ends: for some ε∈(0,12) one has F(x,t)=F(x,0) for t≤ε and F(x,t)=F(x,1) for t≥1−ε, for all x∈V.

Then for every open neighbourhood W⊆N of the compact image F(V×I) there is a smooth map H:N×I→N such that H0=id⁡N, every Ht is a diffeomorphism of N (Diffeomorphisms and local diffeomorphisms of manifolds), Ht∘F0=Ftfor every t∈I, Ht=id⁡N outside W for every t, Ht=id⁡N for t≤ε/2, and Ht=H1 for t≥1−ε/2.

Facts & Assumptions

Given: the compact smooth n-manifold with boundary V, the smooth n-manifold without boundary N, the smooth isotopy of embeddings F:V×I→N constant near the ends with parameter ε, and the open neighbourhood W of F(V×I).

[F1]

Smooth embeddings: a smooth embedding is an injective smooth immersion that is a homeomorphism onto its image with the subspace topology. For an embedding between manifolds of the same dimension the differential is invertible at every point.

[F2]

Smooth maps between manifolds with boundary: a continuous map of manifolds with boundary is smooth when every coordinate representative in boundary charts is smooth on a relatively open subset of a half-space in the local-extension sense, that is, it is the restriction of a smooth map defined on an open subset of the ambient Euclidean space.

[F3]

Choice-free smooth inverse function theorem in Euclidean space: if U⊆Rn is open, f:U→Rn is smooth and Df(a) is invertible, then f restricts to a diffeomorphism from an open neighbourhood of a onto an open subset of Rn. No choice axiom is used.

[F4]

Smooth partitions of unity exist on manifolds: every open cover of a smooth manifold admits a smooth partition of unity subordinate to it.

[F5]

A smooth Urysohn lemma for a closed set in an open set: for a closed set inside an open set there is a smooth cutoff that equals 1 on a neighbourhood of the closed set and has support in the open set.

[F6]

In a locally compact Hausdorff space every open set containing a point contains an open set containing it whose closure is compact and still inside; such a space is regular: every point of a locally compact Hausdorff space has basic open neighbourhoods with compact closure; smooth manifolds are locally compact Hausdorff.

[F7]

Time-dependent vector fields have local smooth evolution operators: for a smooth time-dependent vector field Xt on a manifold M and every (s,p) there are an open interval around s and neighbourhoods of the evolving points carrying a smooth evolution map Ψ whose curves are the unique solutions of γ˙(t)=Xt(γ(t)) with γ(s)=p.

[F8]

Time-dependent evolution satisfies the two-time cocycle law: evolution operators of a smooth time-dependent vector field satisfy Ψu,t∘Ψt,s=Ψu,s and Ψs,s=id⁡ wherever both sides are defined.

[F9]

Compactly supported time-dependent vector fields have global evolution on a compact time interval: a smooth time-dependent vector field on M whose union of supports over a compact interval J is contained in a compact subset of M has a global evolution operator Ψt,s:M→M for all s,t∈J.

[F10]

A smooth vector field is a smooth section of the tangent bundle and Time-dependent vector fields and their evolution operators: a time-dependent vector field on N over R is a smooth map X:R×N→TN with X(t,y)∈TyN; a horizontal field on the product R×N is one of this form, placed in the second summand of T(R×N).

[F11]

Embedded smooth submanifolds with boundary: a subset of a smooth manifold is an embedded smooth submanifold with boundary when it carries a manifold-with-boundary smooth structure for which the inclusion is a smooth embedding.

Proof

Given: the objects and hypotheses of the statement; write K:=F(V×I) for the compact image and fix the parameter ε of constancy near the ends.

1.1F6F12given

The product V×I is compact: for an open cover and each time, compactness of V supplies finitely many product neighbourhoods covering that time slice; intersect their time intervals to obtain a neighbourhood of that time, and compactness of I supplies finitely many such neighbourhoods. Thus a finite subcover exists. The image K=F(V×I) is compact, being the continuous image of the compact space V×I, and K⊆W; every point of K has by [F6] an open neighbourhood with compact closure contained in W, finitely many of these cover K, and their union V′ is an open neighbourhood of K with V′‾ compact and V′‾⊆W.

1.2givenconstructalgebra

Extend F in the time direction by F~(t,x)=F(x,0) for t≤0, F~(t,x)=F(x,t) for 0≤t≤1 and F~(t,x)=F(x,1) for t≥1: the prescriptions agree on the overlaps because F is constant for t≤ε and for t≥1−ε, so F~:R×V→N is smooth and each F~t is a smooth embedding; let Θ:R×V→R×N, Θ(t,x)=(t,F~(t,x)), be the graph map.

2.1F1F2F3step 1.2

The graph map is an injective immersion with invertible differential at every point: injectivity is immediate from the first coordinate, and at (t0,x0) a boundary chart of V at x0 and a chart of N at F~(t0,x0) present the coordinate representative of Θ as a map smooth on a relatively open subset of a half-space in the sense of [F2], hence as the restriction of a smooth map Φ defined near (t0,u(x0)) in an open set; the differential of F~t0 at x0 is invertible by [F1] because F~t0 is an embedding between n-manifolds, so the differential of Φ there is invertible and [F3] restricts Φ to a local diffeomorphism, exhibiting Θ locally as the restriction of an ambient diffeomorphism to the source half-space. At a boundary point its image is a half-space neighbourhood, not an ambient open set; in the interior it is open.

3.1F11F12step 1.2step 2.1

The graph map is proper: for a compact L⊆R×N the time projection π1(L) is compact, Θ−1(L) is closed in the compact set π1(L)×V by continuity and closedness of L, hence Θ−1(L) is compact; a proper continuous map into this locally compact Hausdorff target is closed: for a closed source subset A and y outside its image, choose a compact target neighbourhood L of y; the image of A∩Θ−1(L) is compact and hence closed in the Hausdorff target, and deleting it from the interior of L gives a neighbourhood of y missing the image of A. Therefore Θ is closed, its image S:=Θ(R×V) is closed in R×N and Θ is a homeomorphism onto S whose inverse is smooth by step 2.1, so S is an embedded smooth submanifold with boundary of R×N in the sense of [F11] with ∂S=Θ(R×∂V).

4.1F10step 3.1algebra

Define the horizontal velocity along the graph by placing Y(Θ(t,x)):=(0,∂tF~(t,x)) in {0}⊕TF~(t,x)N⊆T(t,F~(t,x))(R×N): the assignment is well defined because Θ is injective and smooth because Θ−1 is smooth by step 3.1, it is a horizontal smooth field along S in the sense of [F10], and Y=0 at every point of S whose first coordinate lies outside [0,1], because F~ is constant in t there.

5.1F2F10step 1.1step 2.1step 4.1construct

At every point q∈S the field Y extends over an open neighbourhood in R×N to a smooth horizontal field: choose (t0,x0)=Θ−1(q) and, by step 2.1, an open neighbourhood U of (t0,x0) in R×V mapped diffeomorphically onto Ω0:=Θ(U); shrink U so that F~(t,x)∈V′ for all (t,x)∈U, possible by continuity because F~(t0,x0)∈K⊆V′. If x0∈int⁡V then Ω0 is open in R×N and Y~q(Θ(t,x)):=(0,∂tF~(t,x)) defines on it a smooth horizontal field restricting to Y on S∩Ω0. If x0∈∂V then Ω0 is only a half-space neighbourhood of q, but in boundary charts of V the horizontal components of Y are smooth functions on that half-space model, so by the local-extension convention of [F2] they extend smoothly to an open neighbourhood of q in R×N while the zero first component extends by zero, giving a smooth horizontal field on a neighbourhood Ω that restricts to Y on S∩Ω; in both cases Ω may be shrunk to lie in R×V′.

6.1F4step 1.1step 4.1step 5.1algebra

The compact set S0:=Θ([0,1]×V)⊆S is covered by finitely many neighbourhoods Ωq1,…,Ωqm from step 5.1, each contained in R×V′; let (ψ0,ψ1,…,ψm) be a smooth partition of unity on R×N subordinate to the open cover {R×N∖S0,Ωq1,…,Ωqm}, which exists by [F4], and define Y~:=∑i=1mψiY~qi with each term extended by zero outside Ωqi; the sum is smooth because supp⁡ψi⊆Ωqi, it takes values in the horizontal subbundle and so is a time-dependent vector field Y~(t,y)=X(t,y)∈TyN on N over R in the sense of [F10], and for q∈S one has Y~(q)=∑iψi(q)Y(q)=(1−ψ0(q))Y(q)=Y(q), because ψ0(q)≠0 forces q∉S0 and then Y(q)=0 by step 4.1; finally supp⁡Y~⊆R×V′‾ because each Ωqi⊆R×V′.

7.1F5F9step 6.1

By [F5] choose a smooth function β:R→[0,1] with β=1 on [ε,1−ε] and β=0 outside (ε/2,1−ε/2), and put Xt′:=β(t)Xt for t∈[0,1]; then ⋃t∈[0,1]supp⁡Xt′ is contained in the compact subset V′‾⊆N, so [F9] provides a global evolution operator Ψt,s:N→N for s,t∈[0,1].

8.1F7F10step 7.1algebra

The isotopy identity: fix x∈V and put γ(t):=Ft(x) for t∈[0,1]; then γ(0)=F0(x) and γ′(t)=∂tF(t,x) equals Xt′(γ(t)) for every t, because on [ε,1−ε] one has β=1 and Xt(γ(t))=∂tF~(t,x)=∂tF(t,x) by step 6.1, while off [ε,1−ε] the derivative ∂tF(t,x) vanishes and is multiplied by β(t)∈[0,1]; the curve t↦Ψt,0(F0(x)) solves the same equation with the same initial value by the defining property of the evolution operator in [F10], both curves are defined on all of [0,1], and the local uniqueness in [F7] makes them agree near every point of the connected interval, so Ht∘F0=Ft for Ht:=Ψt,0.

9.1F7F8step 1.1step 6.1step 7.1step 8.1∎

The remaining properties: H0=Ψ0,0=id⁡N and each Ht is a diffeomorphism with inverse Ψ0,t, since the cocycle law of [F8] gives Ψ0,t∘Ψt,0=Ψ0,0=id⁡N and Ψt,0∘Ψ0,t=Ψt,t=id⁡N; the map (t,y)↦Ht(y) is smooth because near every (t0,y0) it agrees by [F7] with the local smooth evolution map of X′ through the point Ht0(y0) at time t0; if y∉V′‾ then Xt′(y)=0 for all t by step 6.1, so the constant curve at y solves the equation of X′, [F7] gives Ht(y)=y, and hence Ht=id⁡N outside W because V′‾⊆W; finally Xt′=0 for t≤ε/2 and for t≥1−ε/2, so the cocycle law gives Ht=id⁡N for t≤ε/2 and Ht=Ψt,1−ε/2∘H1−ε/2=H1−ε/2=H1 for t≥1−ε/2.

Depends on

Used by

Dependency tree · two levels

86 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