Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
1  
In the last sentence do you mean unit instead of counit? –  Stefan Hamcke Sep 7 '13 at 17:34
    
@StefanH. yes, I did indeed, and I've fixed it. Thanks! –  Joshua Taylor Sep 7 '13 at 17:39
    
My inbox tells me that there was a comment beginning with "I'd almost be inclined to call it $\lambda$ from $\lambda$-calculus, but that's not quite...", but since it's not appearing here, I'm guessing that it was deleted. I agree that it's not quite $\lambda$, and the way that I've seen $\lambda$ used in notation regarding exponentials is that for an arrow $f \colon A \times C \to B$, the corresponding arrow is $\lambda f\colon A \to B^C$. –  Joshua Taylor Sep 7 '13 at 17:43
    
I used to call it $\lambda$, but I think it's probably better to call it something like $\mathsf{pair}$. –  Zhen Lin Sep 7 '13 at 18:08
    
@ZhenLin Perhaps this obvious, but it just hit me that the the arrow that I called $\lambda f$ is just the more general case; this particular case is just the $\lambda \mathrm{id}_{A \times C}\colon A \to (A \times C)^C$. I think you're right to call it $\lambda$ (or curry (see my answer)). –  Joshua Taylor Sep 7 '13 at 18:32

1 Answer 1

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$$

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.