Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
dependent_product_functor [2015/08/17 14:44] nikolaj |
dependent_product_functor [2015/12/22 18:01] 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 62: | Line 64: | ||
| \end{CD} | \end{CD} | ||
| $$ | $$ | ||
| - | Essentially, we get the section space $\prod_X p$ that we are after, if we just replace the projection $\pi_2:X\times Y\to X$ with the more general $p$. A section of this space must in general then not map the second component $x$ to itself, but instead map it into $p^{-1}(x)$. | + | Essentially, we get the section space $\prod_X p$ that we are after, if we just replace the projection $\pi_2:X\times Y\to X$ with the more general $p$. The function space we obtain need the not just be $Y^X$, but can be some more general so called section space. A section of this space must in general then not map an $x$ in $X$ to $x$ in $Y\times X$, but instead merely map it somehow into $p^{-1}(x)$. |
| So for an auxiliary object $A$, consider the projection $\pi_2:(A\times X)\to X$, formally defined as the arrow obtained by pulling back $!_A:A\to*$ along $!_X:X\to*$, i.e. $\pi_2:=!_X{}^*!_A$. This definition is appearent from the commuting square defining the product: | So for an auxiliary object $A$, consider the projection $\pi_2:(A\times X)\to X$, formally defined as the arrow obtained by pulling back $!_A:A\to*$ along $!_X:X\to*$, i.e. $\pi_2:=!_X{}^*!_A$. This definition is appearent from the commuting square defining the product: | ||
