LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck 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.

Formal-immersion homotopies extend over a collar

Statement

Assume countable choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $X$ be a compact smooth $m$ -manifold with boundary, and attach an outward collar to form $X^{+} = X \cup_{\partial X} (\partial X \times [- 1, 0])$ , using a fixed smooth collar to give the union its smooth structure. Let $X^{\circ} = int X$ and let $N$ be a smooth manifold with $\dim N \geq m$ . Then each restriction map in $Imm (X^{+}, N) ⟶ Imm (X, N) ⟶ Imm (X^{\circ}, N)$ and in the analogous sequence for $FImm$ is a homotopy equivalence for the weak compact-open smooth topology. Consequently the derivative map is a weak homotopy equivalence on any one of $X^{+}$ , $X$ , and $X^{\circ}$ if and only if it is one on the other two. The homotopy inverses and their comparison homotopies are given by precomposition with smooth embeddings supported in a collar; they apply simultaneously to parameter families and fix data on a core outside that collar. Thus formal-immersion families and homotopies extend across the attached collar up to these comparison homotopies.

All three source manifolds have dimension $m$ . An immersion of $X \times [0, 1]$ has source dimension $m + 1$ and is a different object from a path of immersions of $X$ ; no product-source assertion is intended.

Facts & Assumptions

Given: Countable choice, $X$ , its attached collar $X^{+}$ and interior $X^{\circ}$ , and $N$ as in the Statement.

[F1]

Under countable choice $X$ admits a smooth collar (Collar neighborhood theorem, Smooth collars of a manifold boundary). Rescale its coordinate so that the combined collar in $X^{+}$ has coordinates $(z, u) \in \partial X \times [- 1, 4)$ , with $X$ given by $u \geq 0$ there.

[F2]

If $e : M \to M^{'}$ is a smooth embedding of manifolds of the same dimension, precomposition sends an immersion $g$ to $g \circ e$ , and a formal immersion $(f, F)$ to $(f \circ e, F \circ d e)$ . These operations commute with the derivative map (The derivative map from immersions to formal immersions, Space of immersions and space of formal immersions).

[F3]

A homotopy equivalence induces a weak homotopy equivalence, and weak homotopy equivalences satisfy two-of-three (Weak homotopy equivalence).

Proof

technique · direct

1.1F1constructchoose

Choose a smooth strictly increasing diffeomorphism $ϕ : [- 1, 4) \to [0, 4)$ equal to $u$ near $u \geq 3$ , and satisfying $ϕ (u) \geq u$ . One explicit construction is $ϕ (u) = u + b (u)$ , where $b (u) = \int_{u}^{3} ρ (v) d v$ for $u \leq 3$ , extended by zero for $u \geq 3$ , and $ρ$ is a smooth nonnegative bump in $(- 1, 3)$ with integral one and $ρ < 1$ ; such a bump exists because the interval has length four. Thus $ϕ (- 1) = 0$ and $ϕ^{'} = 1 - ρ > 0$ . The map $c : X^{+} \to X$ given by $(z, u) \mapsto (z, ϕ (u))$ in the collar and by the identity elsewhere is a diffeomorphism. If $j : X ↪ X^{+}$ is inclusion, the interpolation $ϕ_{t} (u) = (1 - t) u + t ϕ (u)$ gives homotopies through embeddings from ${i d}_{X^{+}}$ to $j c$ and from ${i d}_{X}$ to $c j$ (restrict to $u \geq 0$ for the latter). These maps are identity off the collar.

1.2F1constructchoose

Choose a smooth nonnegative function $χ$ on $[0, 4)$ equal to one near zero and zero for $u \geq 3$ . Choose $a > 0$ with $a < 1$ and $a \sup ∣ χ^{'} ∣ < 1$ . The maps $u \mapsto u + t a χ (u)$ have positive derivative for $0 \leq t \leq 1$ , match the identity near $u \geq 3$ , and stay nonnegative; at $t = 1$ they send all of $[0, 4)$ into $(0, 4)$ . They therefore define embeddings $q_{t} : X \to X$ , with $q_{0} = {i d}_{X}$ and $q = q_{1} : X \to X^{\circ}$ . For $i : X^{\circ} ↪ X$ , the same homotopy gives $i q ≃ {i d}_{X}$ and, restricted to $u > 0$ , $q i ≃ {i d}_{X^{\circ}}$ through embeddings of the indicated sources.

2.1F2step 1.1step 1.2

Apply precomposition to step 1.1. For either genuine or formal immersion spaces, $c^{*}$ is a homotopy inverse to restriction $j^{*}$ : their composites are precomposition with $j c$ and $c j$ , whose homotopies are supplied there. Similarly $q^{*}$ is a homotopy inverse to $i^{*}$ by step 1.2. The precomposition homotopies are continuous in the weak smooth topology: for each compact source set, its image under the smooth embedding homotopy is compact, and the chain rule bounds each tested derivative by finitely many derivatives on that compact image. This also covers the noncompact source $X^{\circ}$ .

3.1F2F3step 2.1∎

These constructions act on every member of a parameter family using the same source embeddings. They therefore extend families or homotopies from $X$ to $X^{+}$ by $c^{*}$ , with their restrictions compared to the original families by the homotopy from $c j$ to ${i d}_{X}$ ; likewise $q^{*}$ compares the interior and compact source. All comparisons fix the core where the embeddings are identity. In each restriction square the derivative maps commute by [F2] and the horizontal maps are homotopy equivalences by step 2.1. Two-of-three consequently makes the derivative map a weak homotopy equivalence on one source exactly when it is on the other sources.

Remarks

The argument supplies homotopy equivalences and comparison homotopies. It does not identify a restriction fibre with a path space, or assert that restriction is a Serre fibration with contractible fibres. Such a fibre assertion is stronger than the collar compression argument and is unnecessary for the interior comparison. Exact extension of a prescribed homotopy with a prescribed initial lift requires a separate lifting theorem.

Depends on

Used by

Dependency tree · two levels

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