Discrete-indiscrete adjunction (source code)

= Discrete-indiscrete adjunction
{title2=$D\dashv J:\mathbf{Top}\to\mathbf{Top}$}

Discretization $D$ and indiscretization $J$ retain underlying sets. Every function $DX\to Y$ is continuous, and every function $X\to JY$ is continuous, giving the <adjunction>. Its induced <monad> and <comonad> are idempotent, since repeated <discrete topology> or <indiscrete topology> construction changes nothing.