cartesian closed categories [tt-004S]
cartesian closed categories [tt-004S]
definition 1. evaluation [leinster2016basic, 6.2.4] [tt-0044]
definition 1. evaluation [leinster2016basic, 6.2.4] [tt-0044]
Let \({\cal S}\) be a small category, \({\cal C}\) a locally small category. For each \(X \in {\cal S}\), there is a functor \[ \begin {array}{lccc} \operatorname {ev}_X: & [{\cal S}, {\cal C}] & \to & {\cal C} \\ & \mathscr {F} & \mapsto & \mathscr {F}(X) \end {array} \] called evaluation at \(X\).
Given a diagram \(\mathscr {D}: {\cal J} \to [{\cal S}, {\cal C}]\), we have for each \(X \in {\cal S}\) a functor \[ \begin {array}{lccc} \mathscr {D} \mathbin {\bullet } \operatorname {ev}_X : & {\cal J} & \to & {\cal C} \\ & J & \mapsto & \mathscr {D}(J)(X) \end {array} \]
We write \(\mathscr {D} \mathbin {\bullet } \operatorname {ev}_X\) as \(\mathscr {D}(-)(X)\).
definition 2. cartesian product functor [kostecki2011introduction, 5.13] [tt-004F]
definition 2. cartesian product functor [kostecki2011introduction, 5.13] [tt-004F]
If \({\cal C}\) is a category with binary products, we can define for every \(X\) the cartesian product functor \(X \times (-)\) : \({\cal C} \rightarrow {\cal C}\), with the following action: \[ \begin {aligned} & (X \times (-))(Y)=X \times Y \\ & (X \times (-))(f)=\operatorname {id}_X \times f \end {aligned} \]
definition 3. exponential [kostecki2011introduction, 5.13] [tt-004G]
definition 3. exponential [kostecki2011introduction, 5.13] [tt-004G]
If for \(X \in {\cal C}\), a cartesian product functor \(X \times (-)\) has a right adjoint, it is called an exponential or the exponential object, denoted \((-)^X\).
Explicitly, \(X \times (-) \dashv (-)^X\) means there is a natural isomorphism of bifunctors \(\operatorname {Hom}(X \times (-),-) \cong \operatorname {Hom}(-, (-)^X)\), i.e. for any arrow \(f: X \times Y \to Z\) there is a unique arrow \(f^b: Y \to Z^X\), which is the transpose of the adjunction, called exponential transpose.
The arrow \(\operatorname {ev} : X \times (-)^X \to (-)\) is called the evaluation arrow of the exponential, and is the counit of the adjunction.
Diagramatically, the diagram
commutes.
We say that category \({\cal C}\) has exponentials if for any \(X \in {\cal C}\), there exists an exponential \((-)^X\).
definition 4. cartesian closed category [kostecki2011introduction, 5.14] [tt-004H]
definition 4. cartesian closed category [kostecki2011introduction, 5.14] [tt-004H]
A category \({\cal C}\) is called cartesian closed iff \({\cal C}\) has exponentials and has finite products.
definition 5. power object [kostecki2011introduction, 6.8] [tt-004L]
definition 5. power object [kostecki2011introduction, 6.8] [tt-004L]
The power object \(P(X)\) of an object \(X\) in a cartesian closed category \({\cal C}\) with subobject classifier \(\Omega \) is defined as the exponential object \(\Omega ^X\).
If \(\Omega ^X\) exists for any \(X\) in \({\cal C}\), we say that \({\cal C}\) has power objects.
lemma 6. properties of cartesian closed categories [kostecki2011introduction, 5.15] [tt-004N]
For any cartesian closed category \({\cal C}\), and any objects \(X, Y, Z\) of \({\cal C}\), we have
lemma 6. properties of cartesian closed categories [kostecki2011introduction, 5.15] [tt-004N]
- \(\mathrm {0} \times X \cong \mathrm {0}\) if \(\mathrm {0}\) exists in \({\cal C}\)
- \(1 \times X \cong X\)
- \(X^{\mathrm {0}} \cong \mathrm {1}\) if \(\mathrm {0}\) exists in \({\cal C}\)
- \(X^1 \cong X\)
- \(\mathrm {1}^X \cong 1\)
- \(X \times Y \cong Y \times X\)
- \((X \times Y) \times Z \cong X \times (Y \times Z)\)
- \(Y^X \times Z^X \cong (Y \times Z)^X\)
- \(Z^{X \times Y} \cong \left (Z^X\right )^Y\)
- \(X+Y \cong Y+X\)
- \((X+Y)+Z \cong X+(Y+Z)\)
- \(Z^X \times Z^Y \cong Z^{X+Y}\) if \({\cal C}\) has binary coproducts
- \((X \times Y)+(X \times Z) \cong X \times (Y+Z)\) if \({\cal C}\) has binary coproducts