Adjoint functors and the unit–counit equations

Let $F:\mathcal C\to\mathcal D$ and $G:\mathcal D\to\mathcal C$. Saying that $F$ is left adjoint to $G$ means there is a bijection from $\mathcal D(Fc,d)$ to $\mathcal C(c,Gd)$, natural in both $c$ and $d$. Precomposing in $c$ and postcomposing in $d$ must commute with the bijection. Equal cardinalities for particular finite objects are insufficient: the same correspondence must respect every allowed map in both categories.

For a fixed set $A$, the functor $F(X)=A\times X$ is left adjoint to $G(Y)=Y^A$. A function on a pair is converted into a function that assigns to each second coordinate a function of the first coordinate. This is currying. Its inverse evaluates the assigned function on the first coordinate. The two formulas undo each other pointwise, and their compatibility with source and target maps follows by substitution.

The unit $\eta:\mathrm{Id}_{\mathcal C}\Rightarrow GF$ is the transpose of the identity on $Fc$. The counit $\varepsilon:FG\Rightarrow\mathrm{Id}_{\mathcal D}$ transposes back from the identity on $Gd$. In the currying adjunction, the unit sends $x$ to the function $a\mapsto(a,x)$, and the counit evaluates $(a,k)$ to $k(a)$. These are generally not isomorphisms, so an adjunction need not be an equivalence.

The two triangle identities say that the appropriate round trips act as identities on $F$ and $G$. Their components have different types and should not be interchanged. Conversely, natural unit and counit maps satisfying these identities define the Hom bijection by sending $f$ to $G(f)\eta_c$ and sending $g$ back to $\varepsilon_dF(g)$. Expanding a round trip and using naturality plus a triangle identity proves that these formulas are inverse.

Regard posets as categories with at most one arrow between two objects. A Hom bijection then states that an inequality on one side holds exactly when its partner inequality holds on the other. For a function $f:X\to Y$, direct image sends subsets of $X$ to subsets of $Y$, and inverse image goes back. They are monotone, and direct image is left adjoint to inverse image because every element of a subset lands in a target subset exactly when it belongs to that subset's inverse image.

The unit becomes $S\subseteq f^{-1}(f(S))$, and the counit becomes $f(f^{-1}(B))\subseteq B$. These inclusions can be strict: the first adds points sharing an image, while the second excludes target points not hit by the function. They therefore illustrate why adjoint does not mean inverse. Here inverse image is a functor between two powerset posets for one fixed function, not the direct-image powerset endofunctor used later to construct a monad.