name of the unit of adjunction between $-\times C$ and $\cdot^C$

285 Views Asked by At

Answers to a earlier question about the categorical interpretation of first-order quantification led me to learn more about adjoints. Now, I understand that a category $\mathscr{C}$ with products has exponentials if the $-\times X\colon \mathscr{C} \to \mathscr{C}$ functors have right adjoints. For instance, the functor $-\times C \colon \mathscr{C} \to \mathscr{C}$ takes each object $A$ to $A \times C$ and each arrow $f\colon A \to B$ to $f \times 1_C\colon A\times C \to B \times C$. The right adjoint to this functor, $(\cdot)^C\colon \mathscr{C} \to \mathscr{C}$ takes each object $A$ to $A^C$ and each arrow $f\colon A \to B$ to $f^C\colon A^C \to B^C$.

The counit of this adjunction is a natural transformation $\epsilon\colon -\times C \circ (\cdot)^C \to 1_{\mathscr{C}}$, which is a family of arrows $\epsilon_{A,C}\colon A^C \times C \to A$. These arrows are typically called evaluation or application arrows when speaking of programming language, or modus ponens arrows if looking at logics.

The unit of this adjunction is a natural transformation $\eta\colon 1_{\mathscr{C}}\to (\cdot)^C \circ - \times C$, which is a family of arrows $\eta_A\colon A \to (A \times C)^C$. Are there any typical names for the unit of this adjunction and, if so, what are they?

1

There are 1 best solutions below

0
On BEST ANSWER

After a bit more thinking, and some insight triggered by the comments, I realized that if the category has some schema

$$\frac{f\colon A \times B \to C}{\phi(f)\colon A \to C^B}$$

the natural transformation arrow $\eta_A \colon A \to (A\times C)^C$ is simply $\phi(\mathrm{id}_{A \times C})$. The question then is simply whether there's a name for this special case, which now doesn't seem quite as important, and what notation gets used for it. Now that I know where to look, some notations have been easy to find, though I haven't seen mention of a particular name for the natural transformation.

Lambek & Scott: $(\cdot)^*$

Lambek & Scott (Introduction to higher-order categorical logic, p. 51) call this:

$$(\mathrm{id}_{A \land C})^*\colon A \to (A \land C) \Leftarrow C$$

They use the notation $A \land C$ and $C \Leftarrow B$ rather than $A \times C$ and $B^C$, due of the logic-oriented direction of the book, but the superscript ${}^*$ is the point of interest, not the notations for the product and exponential.

Goldblatt ($\hat{\cdot}$) and Awodey ($\tilde{\cdot}$)

Goldblatt (Topoi: The Categorial Analysis of Logic, pp. 70,71) denotes this type of arrow with $\hat\cdot$. Specifically, for $g\colon C \times A \to B$, there is the arrow $\hat{g}\colon C \to B^A$, and so the unit would be

$$\widehat{\mathrm{id}_{A \times C}} \colon A \to (A \times C)^C$$

Awodey (Category Theory, p. 107) uses a similar notation with a ~:

$$\widetilde{\mathrm{id}_{A \times C}} \colon A \to (A \times C)^C$$

Computer Science: curry

A question on Theoretical Stack Exchange reminds us that in programming language theory, these types of arrow are called curry arrows:

$$\mathrm{curry}(\mathrm{id}_{A\times C})\colon A \to (A\times C)^C$$