Immersion extension on a disk: absolute and relative parametric forms

The formal evaluation has the section $c(y,L)(x)=(y,L)$. The homotopy $(f(x),F_x)\mapsto (f(tx),F_{tx})$, $1\ge t\ge 0$, is a homotopy through formal immersions from the identity to $c{e}_F$: here $F_{tx}$ is read using the fixed trivialization of $T{D}^k$, without multiplication by $t$. It is continuous in the weak smooth topology and fixes constant formal data. Thus $e_F$ is a homotopy equivalence.

For each frame $(y,L)$, the maps $x\mapsto r(y+aLx)$ are defined and are immersions for all sufficiently small $a>0$, uniformly for frames in a neighbourhood of $(y,L)$. Indeed their derivatives divided by $a$ are $d{r}_{y+aLx}L$, which converge uniformly for $x\in D^k$ to the injective map $L$. Choose neighbourhoods with positive constant bounds on $a$ and a subordinate locally finite smooth partition; the weighted average of smaller such constants gives a positive smooth function $ϵ(y,L)$ such that every $0<a\le ϵ(y,L)$ works. Hence $s(y,L)(x)=r(y+ϵ(y,L)Lx)$ defines a continuous map $s:V_k(TN)\to \mathrm{Imm}(D^k,N)$. Its evaluation is $(y,ϵ(y,L)L)$, homotopic to $(y,L)$ by positive scalar multiplication.

Let $K$ be a compact parameter space and $g:K\to \mathrm{Imm}(D^k,N)$ a continuous family. Put $y_p=g_p(0)$ and $L_p=d{g}_p(0)$. Choose a common $\delta >0$ smaller than every $ϵ(y_p,L_p)$ and sufficiently small for the following construction. First precompose with $x\mapsto tx$, $1\ge t\ge \delta$, obtaining $g_p(\delta x)$ through immersions. Next, for $\delta \ge t>0$, set $h_{p,t}(x)=r(y_p+\delta (g_p(tx)-y_p)\mathrm{/}t)$ and at $t=0$ set $h_{p,0}(x)=r(y_p+\delta L_{p}x)$. Taylor's integral formula gives $(g_p(tx)-y_p)\mathrm{/}t={\int }_0^{1}d{g}_p(utx)xdu$, so this formula extends continuously in every spatial derivative to $t=0$. Its derivative divided by $\delta$ is $d{r}_{y_p+\delta (g_p(tx)-y_p)\mathrm{/}t}d{g}_p(tx)$ and is uniformly close to $L_p$ for $0\le t\le \delta$. Compactness gives a uniform positive injectivity margin, so all $h_{p,t}$ are immersions and their arguments lie in $W$. At $t=\delta$ this is $g_p(\delta x)$, since $r$ fixes $N$.

Increase $a$ from $\delta$ to $ϵ(y_p,L_p)$ in $r(y_p+a{L}_{p}x)$. Step 1.2 keeps this a family of immersions and joins the endpoint of step 2.1 to $s{e}_I(g_p)$. Thus every compact family is homotopic through immersions to $s{e}_I$ of that family. This applies to spheres and to homotopies parametrized by disks or sphere-times-interval, and together with $e_{I}s\simeq \mathrm{i}\mathrm{d}$ proves that $e_I$ induces a bijection on path components and isomorphisms on all homotopy groups, with the usual basepoint paths provided by these homotopies. Consequently $e_I$ is a weak homotopy equivalence. For $k=0$ all spaces and evaluations are simply $N$.

The derivative map $D:g\mapsto (g,dg)$ satisfies $e_{F}D=e_I$. Since both evaluations are weak homotopy equivalences by steps 1.1 and 3.1, $D$ is a weak homotopy equivalence. This constructively proves the absolute weak-equivalence assertion in every dimension $k\le n$, including equality; it does not use a genuine-immersion restriction fibration.

The absolute comparison also holds for full $m$-column core data on $D^j$, $j\le m\le n$, whose first $j$ columns are the core derivative on the genuine side. Forget the extra $m-j$ columns. The genuine and formal forgetful maps have the same fibres: a transversal $(m-j)$-frame modulo the tangent image, with arbitrary tangent components of its lifts. For nearby base data, identify target tangent fibres by the local addition, then identify tangent images and normal complements by orthogonal projection. This gives local product charts on each locus where the fibre is nonempty. These admissible loci are open and path-saturated: finite successive normal transports along a compact path carry any existing transverse frame to the endpoint. Therefore an ordinary weak equivalence restricts to those loci before their extra-column fibration comparison is used. Compact-cube homotopies lift by finite successive projection transports, followed by the collar/frame operators in [F4]. Thus these maps are Serre fibrations, and their derivative square has identical fibre maps. The ordinary disk equivalence from step 4.1 and the exact sequences [F4] give the full-column core equivalence. This argument does not integrate cocore directions as parameters; it carries their transverse derivative columns as bundle data.

We prove boundary-relative core comparison by induction on $j<n$, simultaneously for every $j\le m\le n$. The $j=0$ case is the equality of the genuine and formal point/frame data, with empty boundary. Suppose the comparison is proved below $j$. The ordinary derivative map for $S^{j-1}$ is a weak equivalence: assemble its two $(j-1)$-disks along their common boundary, using the previously proved relative core comparison. First-jet matching can be made matching of actual immersion germs. In an inner collar let $g,h$ be the two extensions of the same full boundary jet, with $h$ the canonical local-addition extension. In target logarithm coordinates $g-h=O(r^2)$ and $d(g-h)=O(r)$, uniformly over compact parameter families. Replacing $g$ by $h+\chi (r\mathrm{/}ϵ)(g-h)$ changes its derivative by $O(ϵ)$, because $d\chi (r\mathrm{/}ϵ)(g-h)=O(ϵ)$; therefore a sufficiently small common $ϵ$ keeps the full derivative injective and makes $g=h$ on a smaller collar. This pinching is relative where the maps already agree, and parametric cutoffs keep a supplied genuine family on a parameter neighbourhood unchanged. Formal full jets are matched by the analogous collar operator. The resulting disk homotopies glue smoothly to the sphere. Applying the same extra-column forgetful comparison as in step 5.1 gives the weak equivalence on full-column boundary data over $S^{j-1}$. The formal boundary space also retains the actual radial derivative $C$ of its base map, independently of $B(r)$. Those $C$ fields have an affine contractible fibre; the linear homotopy $C\mapsto (1-s)C+sB(r)$ retracts it to the graph supplied by genuine data. Thus this additional actual base jet does not change the boundary comparison, and it ensures formal base maps as well as bundle columns match their first jets when pasted.

Compare the genuine and formal restriction fibrations of [F4] for the $j$-disk. Their total-space map is the equivalence of step 5.1, and their boundary-space map is the equivalence of step 6.1. Their fibre map over each corresponding genuine boundary datum is therefore a weak equivalence, by the exact-sequence comparison, including degrees zero and one. Existence of a genuine extension when a formal extension exists follows too: choose a genuine total datum in the formal extension's component; its boundary datum lies in the component of the prescribed boundary datum by the boundary equivalence. Lift a genuine boundary path backwards using [F4] to obtain a genuine extension of the prescribed boundary. Thus no formal extension component is silently excluded by an empty genuine fibre. For boundary data varying with a finite CW parameter, pull back both restriction fibrations over that boundary family. The fibre comparison just proved gives fibrewise lifting up to homotopy: factor it by the fibrewise mapping-path space, whose fibre over a parameter is the homotopy fibre of that weak equivalence, hence weakly contractible. The projection of this fibrewise mapping-path replacement to the formal extension space pulled back over genuine boundary data is a Serre fibration: lift the genuine endpoint along the boundary track, then lift the formal connecting-path rectangle with both endpoints prescribed, by the relative cubical construction of [F4]. Its fibres are the weakly contractible homotopy fibres just identified, so its exact sequence makes that projection a weak equivalence. Apply [F5] to a finite CW parameter pair and this projection, with the constant connecting paths on prescribed genuine parameters. It gives a lift up to homotopy relative to those parameters. Lift that homotopy backwards through the projection to obtain an exact lift of the original formal section. Its connecting paths remain in the fibres over the original boundary data. Thus the resulting sections and formal homotopies preserve that spatial boundary family throughout. Prescribed genuine parameter cells stay fixed. Thus finite-relative lifting holonomizes every finite CW parameter family of formal extensions, fixing its prescribed genuine parameters and boundary jets. The pinching construction in step 6.1 upgrades fixed boundary jets to the prescribed actual collar germ, so the original spatial collar data remain fixed. This completes the core-dimension induction.

The same relative core comparison applies to an $m$-dimensional $j$-handle. Realize its holonomic full-column core data by local addition in the $m-j$ cocore directions; the derivative along the core is the full monomorphism, hence the maps are immersions on a common compact-parameter neighbourhood of the core. Near the attaching collar use the already prescribed genuine maps. Their first jets agree on the attaching core, so the $O(r^2)$ pinching argument matches their germs on the overlap while preserving rank. This gives an immersion on a neighbourhood of the union of the core and the attaching collar. Relative parameter control requires retaining the original whole-handle immersion on a smaller parameter neighbourhood of $Q$. On the transition strip inside its given genuine neighbourhood, blend this original map with the canonical core realization in target logarithm coordinates. They share full core first jets, so their difference is $O(\mathrm{\mid }v{\mathrm{\mid }}^2)$ and its derivative is $O(\mathrm{\mid }v\mathrm{\mid })$; differentiated cocore cutoffs therefore contribute $O(\delta )$ and preserve rank for a common sufficiently small radius. Use the original map throughout the smaller parameter neighbourhood. Compress the whole handle into the resulting domain by embeddings $(x,v)\mapsto (x,\lambda (p,x)v)$, with $0<\lambda \le 1$, equal to one near $Q$ and on a smaller attaching collar and small away from slightly larger neighbourhoods of those regions. Transition inside the region already covered by the prescribed genuine maps. Its derivative has triangular blocks $I,\lambda I$, so is invertible even though $d\lambda$ is nonzero. The isotopy from $\lambda =1$ gives the comparison with the original formal family, is fixed on the attaching collar, and never drops cocore rank. The formal comparison transports tangent summands with the nonzero scale, or uses the horizontal/vertical identity transport at the collapsed core, rather than setting vertical derivatives to zero. This proves the fixed-source relative handle comparison required by the core argument.

We explain the compact smooth parameter pair, rather than identifying it with an arbitrary compact pair. Let $W$ be the open parameter neighbourhood of $Q$ on which the original family is genuine. Choose a smooth bump equal to one near $Q$ with support in $W$, and a regular level to obtain a compact collared parameter neighbourhood $U$ with $Q\subset \mathrm{int}U\subset U\subset W$. For interval/corner factors work in a compact smooth parameter neighbourhood $P_0\times D_R^d$ containing $P_0\times [0,1{]}^d$. Extend the continuous family by clamping the interval coordinates. On a neighbourhood of $Q$, use the given smooth local extensions instead: a finite parameter cover and parameter-only partition paste smooth extensions of the prescribed genuine maps in the target embedding, then retract to $N$ and set their formal columns equal to the source derivative of that pasted map. On this neighbourhood the columns are not extended independently, so holonomicity is retained. The extensions agree on $P$; compactness and openness of full rank preserve holonomicity on a smaller ambient neighbourhood of $Q$. A cutoff inside the original neighbourhood pastes this with the clamped continuous family. After the deformation restrict back to $P$. The finite Morse/handle construction in [F5] applied to $U$ and the compact complement of its interior produces a finite CW model $(K,L)$ of the parameter pair $(P,U)$. If $U$ has only a finite CW model, replace it by that model before attaching the finitely many complement cells: transport the attaching maps through its homotopy inverse, with attaching collars carrying the required homotopies. This gives maps of pairs $a:(P,U)\to (K,L)$ and $b:(K,L)\to (P,U)$ with pair homotopies $ba\simeq \mathrm{i}\mathrm{d}$ and $ab\simeq \mathrm{i}\mathrm{d}$. Every track starting in $U$ stays in $U$, where the given family is genuine. Apply the fibrewise finite lifting of step 7.1 on $(K,L)$ and pull back by $a$. If the spatial boundary family was pulled back through $ba$, transport it back along the pair homotopy using the compact-parameter lifting supplied in [F4]. Do this also for the formal deformation with its genuine endpoints prescribed; the endpoint-relative cubical lifts in the path variable keep those endpoints. The resulting boundary track followed by its reverse contracts to the fixed original boundary family, and another such lift makes the deformation stationary on that spatial boundary. On $U$ the resulting genuine family is regularly homotopic to the prescribed one, via its composite with the pair homotopy. Extend the reverse regular homotopy to all of $P$ using the homotopy extension property of the collared inclusion $U\subset P$. This extension may move spatial boundary data. Write its projected boundary track as $\beta (p,t)$, starting at the original $b_p$; it is constant on $U$. For each $(p,t)$ lift the reversed track $s\mapsto \beta (p,(1-s)t)$, starting from the extended genuine datum. The compact-parameter lifting formulas of [F4] are stationary on constant tracks, so these lifts preserve the prescribed correction on $U$ and the initial datum at $t=0$. Their endpoints give a corrected genuine homotopy over the original $b_p$ for every $p,t$, ending at the original family on $U$. Concatenating the formal homotopy with this correction produces on $U$ a track followed by its reverse. Contract these loops, and use the same collar homotopy extension property on $P\times I$ relative to $P\times \mathrm{\partial }I\cup U\times I$. Rebase this formal extension too: lift its reversed projected boundary tracks, now with parameters $P\times I$ and the contraction variable, by the formal version of [F4]. On the prescribed ends and on $U$ those projections are constant, so stationary lifting leaves the given loop contraction and both endpoints unchanged. The resulting homotopy is stationary on $U$ and lies over the original spatial boundary throughout. The jet pinching of step 6.1 retains the full prescribed spatial collar germ. Thus it is relative to $Q$. All choices are finite, except the explicitly countable-choice suppliers in [F5].

First prepare a common holonomic neighbourhood of $A$ in $U$. If $P$ is empty the conclusion is immediate; otherwise $F=df$ on $P\times A$, so $df$ has a positive minimum least singular value $c$ there. Joint smoothness and compactness give a source neighbourhood $V$ of $A$, with compact closure in $U$, on which the least singular value of $df$ is greater than $c\mathrm{/}2$ and $\mathrm{\parallel }F-df\mathrm{\parallel }<c\mathrm{/}4$, uniformly in $p$. Choose a smooth source cutoff $\chi =1$ on a neighbourhood of $A$, supported in $V$, and replace $F$ by $(1-s\chi )F+s\chi df$. Every interpolated map remains injective by these estimates. The base map is unchanged; the bundle homotopy fixes $A$ and the given parameter neighbourhood of $Q$, since $F=df$ there. At its endpoint the family is holonomic on one common open source neighbourhood of $A$, including an outer strip beyond $\mathrm{\partial }{D}^k$, without assuming any uniform width for the original pointwise holonomic neighbourhoods. Cut a smaller disk inside this prepared holonomic collar and leave all original data on $A$ unchanged. Apply steps 7.1 and 9.1 with $j=m=k<n$ to that disk and its now common collar-holonomic data. They give the relative deformation on the smaller disk. Extend it by the prepared data on the surrounding holonomic collar and on the rest of $U$; the agreement on an open collar makes the extension smooth in the source. Smooth genuine output families are obtained with the genuine smoothing supplier, fixing the original parameter neighbourhood of $Q$ and prescribed spatial collar. Make the formal deformation constant on small temporal endpoint collars and use formal-family smoothing relative to those endpoint and parameter neighbourhoods. These smoothing operations preserve full fibrewise rank, since their compact jet errors may be chosen below the positive injectivity margin. Multiply their parameter-mollification correction by a fixed smooth source cutoff zero on the prescribed collar, with transition inside a region where the original reference is already jointly smooth. Its differentiated error has the additional term $d\chi$ times the zeroth-order mollification error, also tending uniformly to zero. Thus first jets remain small and the prescribed spatial collar maps and bundle columns are kept exactly. Thus a smooth relative deformation is obtained when the input is smooth. The absolute case $k=n$ was already proved in step 4.1 and is not used as a spatially relative disk theorem.

It remains to make the family genuine on all of $U$. For $k=0$ every formal datum is already holonomic. Otherwise, the common holonomic neighbourhood prepared in step 10.1 contains an annulus about $\mathrm{\partial }{D}^k$. Choose $ϵ>0$ small enough that the closed disk $B$ of radius $1+ϵ$ lies in $U$ and its outer collar lies in that annulus. The inner-disk integration of step 10.1, joined to the unchanged prepared annulus, therefore ends genuine on an open neighbourhood of $B$. Choose regular compact sublevels $K_i$ of the exhaustion in [F6], with $B\subset \mathrm{int}{K}_0$, $K_i\subset \mathrm{int}{K}_{i+1}$, and union $U$. The regular levels can be selected by least eligible rational values: properness makes the critical-value set closed on bounded intervals, and Sard makes it have empty interior. Fix collars and finite handle presentations for $K_0\setminus \mathrm{int}B$ and for all subsequent bands before deforming any data; this is an independent countable selection. Every handle has index $j\le k<n$. Apply the relative integration of steps 7.1–9.1, with full source rank $m=k$, to each finite presentation, fixing the preceding genuine compact stage and a smaller collar and a fixed parameter neighbourhood of $Q$. These steps do not require absence of top-index $k$-handles, since $k<n$. Each finite-stage deformation extends to global formal data: its formulas are defined on a neighbourhood of the compact handle, and substitution of the time $t\chi (x)$, with $\chi =1$ near the processed region and supported in that neighbourhood, leaves a formal monomorphism at every point. The same time is substituted in its base map and bundle columns. On the incoming fixed germ the deformation is stationary. A top-index handle has all its boundary in that germ, so extension there is by the identity; other handles have an outgoing cocore buffer for the cutoff.

The successive deformation choices in step 11.1 can be made without dependent choice. Fix countable coordinate, framed and bump data for the parameter, source and time charts. On each compact stage, finite rational combinations of translated and rescaled bumps form a countable dense family of smooth ambient corrections in the first-jet norm: mollify, approximate the integral and its first derivatives by finite Riemann sums, and then approximate their centres, scales and coefficients by rationals. Multiply corrections by fixed masks vanishing on the frozen source and parameter neighbourhoods and the initial time collar; include countably many collar widths and temporal subdivisions. At final time set the candidate bundle columns equal to the differential of its candidate base map on a smaller processed source neighbourhood, using a cutoff supported in the genuine endpoint collar of a successful witness. Make candidates constant on temporal endpoint collars, retract their base maps to $N$, and project columns to its tangent spaces. A successful smooth witness exists by steps 8.1–10.1 applied to this compact stage. Approximation sufficiently close to that witness preserves its compact injectivity margins and the tubular domain, including the bounded derivatives of the masks. The endpoint derivative replacement is also close to the witness, which is already holonomic there. Thus at least one candidate works. Select the least working candidate in the fixed enumeration; select the least eligible dyadic collar widths in the explicit lifting formulas. Recursion by these uniquely specified integers determines the stages; only the fixed geometric data and band presentations used countable choice.

Concatenate the finite-stage homotopies on intervals tending to $1$, with smooth reparametrizations constant near their ends. Keep a fixed open neighbourhood of each completed $K_i$ unchanged thereafter. Every compact subset of $U$ lies in some $K_i$, so all its source derivatives are eventually stationary; the endpoint at time $1$ is a genuine immersion everywhere on $U$, and the homotopy is continuous in the weak smooth topology. With smooth stage data it is jointly smooth, since locally it is constant near time $1$. It fixes $A$ and the retained neighbourhood of $Q$. This proves the original all-$U$ conclusion, including any additional components. Steps 5.1–8.1 and 9.1 prove (iii). For (iv), choose a compact collared parameter neighbourhood $R$ with $Q\subset \mathrm{int}R\subset R\subset W$, where the given data on $W$ are smooth and genuine. The finite pair model $(K,L)\simeq (P,R)$ of [F5] and finite relative lifting give a genuine family after pullback, agreeing on $R$ with the prescribed family composed with the pair-model homotopy inverse. The pair homotopy gives a genuine track on $R$ back to the original family; extend it over $P$ by the collar HEP. Concatenate this correction with the formal deformation. On $R$ its track is the pair-homotopy track followed by its reverse. Contract that retraced loop and extend the contraction by HEP on $P\times I$ relative to $P\times \mathrm{\partial }I\cup R\times I$. The endpoints stay fixed and the formal deformation becomes stationary on $R$. This is the part of step 9.1 that does not require any spatial-boundary rebasings, so it applies to any derivative weak equivalence on compact $X$. Interval factors use the ambient parameter extension described there. Smooth the genuine endpoint relative to a smaller neighbourhood of $Q$, using compactness of $X$. For smooth original data, make the formal deformation constant near its temporal ends and apply formal smoothing relative to those ends and that neighbourhood; both temporal endpoint families are then smooth, so this gives a smooth formal homotopy with genuine endpoint. Continuous original data require only the continuous formal deformation already constructed. This proves (iv) and completes all assertions.