Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: learning: questions

Topic: Currying characterizes exponentials?


view this post on Zulip Nick Smith (Jul 22 2021 at 04:54):

The nLab page on closed monoidal categories says "Currying can be read as a characterization of the internal hom". I want to check I'm understanding this statement correctly, because it seems pretty important. Let me ask a question:

If I have a category, and a canonical way to compose every pair of morphisms f:SXf: S \to X and g:X×YTg: X \times Y \to T in the category to get a morphism h:S×YTh: S \times Y \to T, is that equivalent to saying I have a Cartesian closed category? i.e. is the concept of an "internal hom" fully captured by this property? Or phrased another way: if I have "partial composition" of morphisms as above, can I ignore the perspective that my category has exponential objects? Or by doing so, would I be ignoring other interesting properties of a Cartesian closed category?

view this post on Zulip Robin Piedeleu (Jul 22 2021 at 09:04):

I've probably misunderstood your question, but in a monoidal (not necessarily closed) category you already have a canonical way of composing f:SXf : S \rightarrow X and g:XYTg : X\otimes Y \rightarrow T to get h:SYTh : S \otimes Y \rightarrow T. It's just h=g(fidY)h = g \circ (f \otimes id_Y), isn't it?

view this post on Zulip Nick Smith (Jul 22 2021 at 12:47):

Oh, I guess that works! I was thinking of an alternative process where you take the equivalent g, namely g:XTYg': X \to T^Y, and then compose. Since the style of composition we're discussing doesn't depend on Cartesian closure after all, it obviously does not capture what it means to be Cartesian closed. I will have to think about this more and modify my question.

view this post on Zulip James Wood (Jul 22 2021 at 13:00):

The paragraph before says “This natural isomorphism [Hom(a⊗b,c)≃Hom(a,[b,c])] is called currying.”, so I think the remark just means that an internal hom is anything satisfying that natural isomorphism. The adjunction definition unfolds to exactly this.