generally in differential cohesion
The function is called an immersion precisely if the canonical morphism
is a monomorphism.
Equivalently this means the following.
The function is an immersion precisely if for every point the differential
A smooth function between smooth manifolds is canonically regarded as a morphism in the cohesive (∞,1)-topos SynthDiff∞Grpd. With respect to the canonical infinitesimal neighbourhood inclusion Smooth∞Grpd SynthDiff∞Grpd there is a notion of formally unramified morphism in .
is an immersion precisely if it is formally unramified with respect to this infinitesimal cohesion.
See the discussion at SynthDiff∞Grpd for details.