Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
terminal_morphism [2014/07/21 16:49] nikolaj |
terminal_morphism [2014/09/12 10:53] nikolaj |
||
|---|---|---|---|
| Line 37: | Line 37: | ||
| $\mathrm{hom}(X\times Y,Z)$ being isomorphic to $\mathrm{hom}(X,Z^Y)$. The nice thing is, of course, that this doesn't just work for categories with function, but the same construction also works when reasoning about logic, where currying then is the tautology | $\mathrm{hom}(X\times Y,Z)$ being isomorphic to $\mathrm{hom}(X,Z^Y)$. The nice thing is, of course, that this doesn't just work for categories with function, but the same construction also works when reasoning about logic, where currying then is the tautology | ||
| $\left((A\land B)\implies C\right)\Leftrightarrow \left(A\implies(B\implies C)\right)$. | $\left((A\land B)\implies C\right)\Leftrightarrow \left(A\implies(B\implies C)\right)$. | ||
| - | |||
| - | === Adjoint functors === | ||
| - | To state the definition again, with a little different notation: A terminal morphism from $F$ to $X$ is a pair $\langle O_X,\varepsilon_X\rangle$, where $\varepsilon_X:FO_X\to X$, such that for any $f:FY\to X$, there is a morphism $g_f:Y\to O_X$ in the other category, so that $f$ factors as $f=\varepsilon_X\circ F(g_f)$. | ||
| - | |||
| - | Now if that construction happens to work for all $X$, then it gives rise for the dual initial morphism construction in the other category as follows: By assumption now, for all $X$, there is a universal morphism $\langle O_X,\varepsilon_X\rangle$ from $F$ to $X$. In particular, the factoring works for the identity morphism at $FY$, i.e. $\mathrm{id}_{FY}=\varepsilon_Y\circ F(g_{\mathrm{id}_{FY}})$ with $g_{\mathrm{id}_{FY}}:FY\to O_{FY}$. We denote the so constructed morphism by $\eta_Y:=f_{\mathrm{id}_{FY}}$ and it's the pendant of $\varepsilon_X$ in the other category. We can now introduce a functor $G$ by setting the object map $GX:=O_X$ and the arrow map such that the following diagram commutes | ||
| - | |||
| - | {{adjointfunctorsymmetry.png}} | ||
| - | |||
| - | Even more, we find $\varepsilon:\mathrm{nat}(FG,1_{\bf C})$ and $\eta:\mathrm{nat}(1_{\bf D},GF)$. Therefore, all of this is equivalent to the gadgetry defined in [[counit-unit adjunction]]. | ||
| === Reference === | === Reference === | ||
