The category of
presheaves are cartesien closed
We will prove the title by using coend calculus, as hinted in Coend Calculus by Fosco Loregian.
For consistence letβs first formulate what to prove:
Theorem. For any (small) category
,
its presheaf category
is cartesien closed, i.e., for any presheaves
,
there exist a exponential object
whi is right adjoint to product:
proof: The exponential object
is defined as
.
The theorems/propositions in the comments after each equation are all
in the book Coend Calculus, and
is the standard yoneda embedding.
QED.
Source of TeX:
\begin{align}
\hat{\mathbf{C}}(P, \hat{\mathbf{C}}(\mathbf{y}_ {()} \times Q, R)) & \cong \int_c {\rm Set}(Pc, \hat{\mathbf{C}}(\mathbf{y}_c \times Q, R)) &(\text{By Thm 1.4.1}) \\
& \cong \int_c {\rm Set} (Pc, \int_x {\rm Set}(\mathbf{C}(x, c) \times Qx, Rx)) &(\text{By Thm 1.4.1}) \\
& \cong \int_c\int_x {\rm Set} (Pc, {\rm Set}(\mathbf{C}(x, c) \times Qx, Rx)) &(\text{Representables preserve limits}) \\
& \cong \int_x\int_c {\rm Set} (Pc, {\rm Set}(\mathbf{C}(x, c) \times Qx, Rx)) &(\text{By Thm 1.3.1}) \\
& \cong \int_x\int_c {\rm Set} (Pc \times \mathbf{C}(x, c), {\rm Set} (Qx, Rx)) &(\text{Set is cartesien closed}) \\
& \cong \int_x {\rm Set} (\int^c Pc \times \mathbf{C}(x, c), {\rm Set} (Qx, Rx)) &(\text{Representables turn colimts into limits}) \\
& \cong \int_x {\rm Set} (Px, {\rm Set} (Qx, Rx)) &(\text{By Prop 2.2.1}) \\
& \cong \int_x {\rm Set} (Px \times Qx, Rx) &(\text{Set is cartesien closed}) \\
& \cong \hat{\mathbf{C}}(P \times Q, R) &(\text{By Thm 1.4.1}) \\
\end{align}