Definition:Exponential (Category Theory)

From ProofWiki
Jump to navigation Jump to search


Let $\mathbf C$ be a metacategory with binary products.

Let $B$ and $C$ be objects of $\mathbf C$.

An exponential of $C$ by $B$ consists of an object $C^B$ of $\mathbf C$ and a morphism:

$\epsilon: C^B \times B \to C$

subject to the following UMP:

For all objects $A$ and morphisms $f: A \times B \to C$, there exists a unique morphism:
$\tilde f: A \to C^B$
such that:
$\begin{xy}\xymatrix@[email protected]+3px{ C^B \times B \ar[r]^*+{\epsilon} & C \\ A \times B \ar[u]_*+{\tilde f \times \operatorname{id}_B \hskip{2cm}} \ar[ur]_*+{f} }\end{xy}$
is a commutative diagram, i.e. $\epsilon \circ \paren {\tilde f \times \operatorname{id}_B} = f$.

Evaluation Morphism

The morphism:

$\epsilon: C^B \times B \to C$

associated to $C^B$ is called the evaluation morphism.

Exponential Transpose

For a morphism $f: A \times B \to C$, the unique:

$\tilde f: A \to C^B$

provided by the UMP for $C^B$ is called the exponential transpose of $f$.

For a morphism $g: A \to C^B$, the morphism $\bar g: A \times B \to C$ defined by:

$\bar g = \epsilon \circ \paren {g \times \operatorname{id}_B}$

is also called the exponential transpose of $g$.

Category with Exponentials

Suppose $\mathbf C$ has an exponential $C^B$ for all objects $B$ and $C$ of $\mathbf C$.

Then $\mathbf C$ is called a category with exponentials.

Also see