j-dense monomorphism (source code)

= j-dense monomorphism

A monomorphism is $j$-dense when its $j$-closure is its whole codomain. It is $j$-closed when it equals its closure. Dense monomorphisms are stable under pullback, and a monomorphism that is both dense and closed is an isomorphism.