Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
dependent_product_functor [2015/04/15 16:17] nikolaj |
dependent_product_functor [2015/10/13 20:50] nikolaj |
||
---|---|---|---|
Line 32: | Line 32: | ||
== Explanation starting from the exp-hom adjunction == | == Explanation starting from the exp-hom adjunction == | ||
- | A function space $Y^X$ can be characterized by the isomorphism $(A\to Y^X)\cong((A\times X)\to Y)$. Setting $\theta'(\langle a,x\rangle):=\langle \theta(a),x\rangle$ lets us moreover identify $(A\times X)\to Y$ with the space of function from that $\theta':(A\times X)\to (Y\times X)$ with the additional requirement that the second component is mapped to itself. | + | A function space $Y^X$ can be characterized by the isomorphism $(A\to Y^X)\cong((A\times X)\to Y)$. |
+ | Let us moreover identify $(A\times X)\to Y$ with the space of function from that $(A\times X)\to (Y\times X)$ with the additional requirement that the second component is mapped to itself, i.e. according to the scheme | ||
+ | $\theta'(\langle a,x\rangle):=\langle \theta(a),x\rangle$. | ||
Again, in diagrams: Functions in | Again, in diagrams: Functions in | ||
Line 117: | Line 119: | ||
nLab: [[http://ncatlab.org/nlab/show/dependent+product|Dependent product]] | nLab: [[http://ncatlab.org/nlab/show/dependent+product|Dependent product]] | ||
- | Wikipedia: [[http://en.wikipedia.org/wiki/Adjoint_functors#Categorical_logic|Adjoint functors#Categorical logic]] (here I made the left adjunction explicit in ${\bf{Set}}$) | + | Wikipedia: [[http://en.wikipedia.org/wiki/Adjoint_functors#Categorical_logic|Adjoint functors#Categorical logic]] |
+ | (Here I made the left adjunction explicit in ${\bf{Set}}$.) | ||
---- | ---- |