Regular homotopy of immersions

Assume ${\mathrm{A}\mathrm{C}}_{\omega }$ for the associated tangent-bundle mapping spaces (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)), and let $M^m,N^n$ be smooth manifolds with $m\le n$. A regular homotopy between immersions $f_0,f_1:M\to N$ is a smooth map $H:M\times [0,1]\to N$ such that $H_t:=H(\cdot ,t)$ is an immersion for every $t\in [0,1]$, with $H_0=f_0$ and $H_1=f_1$. Equivalently, $H$ is a path in $\mathrm{Imm}(M,N)$ whose adjoint is smooth; for compact $M$ the smoothing lemma identifies such paths, up to homotopy rel the ends, with arbitrary continuous paths in the weak topology, while for noncompact $M$ only the smooth direction is asserted. A regular homotopy is relative to a closed subset $A\subseteq M$ when $H(a,t)=f_0(a)=f_1(a)$ for every $a\in A$ and $t\in [0,1]$; the value may vary with $a$. A smooth homotopy of formal immersions is a path in $\mathrm{FImm}(M,N)$ with jointly smooth base maps and bundle maps, fixing both of them pointwise over $A$ in the relative case.

The map $H:M\times [0,1]\to N$ is smooth in the sense of Smooth maps between manifolds with boundary, and it is a smooth family in the sense of Smooth families of maps and their evaluation maps over the boundary parameter interval. By Compact parameter pairs and relative families a smooth family over a boundaryless compact parameter manifold $P$ is a smooth map $P\times M\to N$; a path $t\mapsto H_t$ into $\mathrm{Imm}(M,N)$ whose adjoint $M\times [0,1]\to N$ is smooth is the same datum as a regular homotopy, and for compact $M$ Smoothing continuous families of genuine immersions shows conversely that every continuous path in the weak topology is homotopic rel its ends to such a smooth path. For noncompact $M$ only the smooth-to-continuous direction is asserted here.