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: definition of exponential object without cartesianness

Josselin Poiret (Aug 02 2022 at 10:17):

Hi everyone,
As an aside to my current musings on internal universes, I may have stumbled upon the following:
for $X, Y \in C$, an exponential object is an object $X^Y \in C$ with an isomorphism $y(X^Y) \simeq yX^{yY}$ in $\mathrm{Psh}(C)$.
in the case where $X \times Y$ exists, it reduces to the usual definition (at least in my calculations).
I couldn't find such a definition in the nLab and don't really remember anything of the sort, so I'm wondering if this is folklore, and if there are examples of this definition put to use in cases where products don't exist. My first hunch was the definition of implication in posets without a lattice structure, but I'm not that familiar with those.

Lucas Queiroz (he/him/his) (Aug 02 2022 at 12:45):

This question is very interesting. I am interested in seeing it answered.

Morgan Rogers (he/him) (Aug 02 2022 at 13:49):

You could check out [[closed category]], for an axiomatization of the adjoint to a monoidal product for situations where there may not actually be such a product.

Morgan Rogers (he/him) (Aug 02 2022 at 14:04):

For your particular case, you can extract an "elementary" definition from the description in terms of presheaves by using the fact that the product of two objects is covered by the representables corresponding to spans over those objects in the category. It's pretty unwieldy, but it does technically work:
An exponential object $X^Y$ (when it exists) is such that for each span $X^Y \xleftarrow{p} S \xrightarrow{q} Y$ there is a morphism $\mathrm{ev}_{p,q}: S \to X$ compatible with morphisms of spans (this corresponds to the evaluation map in the presheaf topos), and given any object $Z$, for each span from $Z \xleftarrow{u} R \xrightarrow{v} Y$ and each morphism $f : R \to X$, there is a unique morphism $\tilde{f}: Z \to X^Y$ such that $f = \mathrm{ev}_{\tilde{f} \circ u,v}$.

Morgan Rogers (he/him) (Aug 02 2022 at 14:07):

The first part can be expressed more concisely with a diagram of functors involving the category of spans, but it requires about the same amount of set-up.

Morgan Rogers (he/him) (Aug 02 2022 at 14:12):

Ah, I'm missing a condition: conversely, we need every $g:Z \to X^Y$ to yield at least one span $Z \xleftarrow{u} R \xrightarrow{v} Y$ such that $\mathrm{ev}_{g \circ u,v}^{\sim} = g$.

Josselin Poiret (Aug 02 2022 at 14:16):

In the "given any object $Z$" part, don't you mean to say: for each choice of morphism $f : R \rightarrow X$ for a span $Z \leftarrow R \rightarrow Y$ natural in $R$ (ie. compatible with spans, as you're saying), rather than just for each span and each morphism

Morgan Rogers (he/him) (Aug 02 2022 at 14:17):

Yes, there is at least one naturality condition missing in that definition, well spotted :)

Morgan Rogers (he/him) (Aug 02 2022 at 14:19):

As for whether this is folklore... I'm finding it hard to come up with examples where products aren't present, honestly, and since most definitions given in the literature are inspired by particular cases of interest, it seems unlikely that there would have been layed out. The fact that the Yoneda embedding preserves (and reflects) any exponentials which exist is well-known, however, (it just hasn't been applied to situations without products because they're not common enough) so your original observation that these can be defined via Yoneda does fall into the realm of folklore.

Morgan Rogers (he/him) (Aug 02 2022 at 14:21):

That doesn't preclude you from presenting it as you see fit if you find some interesting examples, however, it just means that there aren't any good references for the specific situation you were wondering about.

Josselin Poiret (Aug 02 2022 at 14:22):

I'll try coming up with some examples that are not too far fetched, but this is coming from some investigations into logic and type theory, where you're free not to assume the existence of products :). This was one of the reasons why I mentioned posets with implication

Josselin Poiret (Aug 02 2022 at 14:25):

In the case of posets, you can see $a \rightarrow b$ as the maximum (not supremum, as i wrote initially) of the set of elements $p$ such that for any $x$, $x \leq p$ and $x \leq a$ implies $x \leq b$ (thankfully we can just ignore the naturalities in that case)

Josselin Poiret (Aug 02 2022 at 14:30):

I wonder if this method could be adapted to other concepts valid inside $Psh(C)$ because they're inherited from $Set$, further internalized into $C$ directly.

Morgan Rogers (he/him) (Aug 02 2022 at 14:34):

Josselin Poiret said:

This was one of the reasons why I mentioned posets with implication

I challenge you to find a finite example of a poset with implication which does not have meets :stuck_out_tongue_wink:

Josselin Poiret said:

I wonder if this method could be adapted to other concepts valid inside $Psh(C)$ because they're inherited from $Set$, further internalized into $C$ directly.

Indeed: you can also express any limits you like in this way, and compiling out produces the usual elementary definitions.

Josselin Poiret (Aug 02 2022 at 14:42):

right, but exponentials aren't limits (at least i'm not aware they are)! Maybe there are other things, i'm thinking NNOs and the like, although NNO is fundamentally dual to those above and one would need to use the copresheaves

Morgan Rogers (he/him) (Aug 02 2022 at 14:43):

Morgan Rogers (he/him) said:

Josselin Poiret said:

This was one of the reasons why I mentioned posets with implication

I challenge you to find a finite example of a poset with implication which does not have meets :stuck_out_tongue_wink:

(This is not a trick question, by the way, at least I think it's not. The challenge could be to find the smallest one.)

Morgan Rogers (he/him) (Aug 02 2022 at 14:46):

Josselin Poiret said:

right, but exponentials aren't limits (at least i'm not aware they are)!

That's true, but what they have in common with limits is that they have a universal property defined in terms of morphisms into them, which is the kind of property that Yoneda preserves and reflects because presheaves are entirely determined by the morphisms into them (from representables).

Morgan Rogers (he/him) (Aug 02 2022 at 14:55):

That summary isn't universally true: there are structures with universal properties of that general shape which you could come up with that aren't easier to define at the presheaf level because the universal objects still don't exist. For instance, in a category with exponentials I can define a silly exponential $X \uparrow Y$, when it exists, to be an object such that $\mathrm{Hom}(Z,X\uparrow Y) \cong \mathrm{Hom}(Z^X, Y)$, naturally in $Z$. If such an object exists for fixed $X$ and all $Y$, this would amount to the existence of a right adjoint to exponentiation by $X$. These objects don't typically exist in presheaf toposes.

Morgan Rogers (he/him) (Aug 02 2022 at 14:57):

(when such objects exist for a given $X$, that $X$ is called an internally tiny object, see Definition 1.3 at [[tiny object]]).

Josselin Poiret (Aug 02 2022 at 14:58):

Morgan Rogers (he/him) said:

Morgan Rogers (he/him) said:

I challenge you to find a finite example of a poset with implication which does not have meets :stuck_out_tongue_wink:

(This is not a trick question, by the way, at least I think it's not. The challenge could be to find the smallest one.)

i'm pretty sure if you take $\{a, b, \top\}$ and $a, b \leq \top$ it works.

Morgan Rogers (he/him) (Aug 02 2022 at 15:11):

That was much smaller than I expected :rolling_on_the_floor_laughing: Interesting that $(p \rightarrow q) \equiv q$ in this case!

Josselin Poiret (Aug 02 2022 at 15:12):

Morgan Rogers (he/him) said:

That summary isn't universally true: there are structures with universal properties of that general shape which you could come up with that aren't easier to define at the presheaf level because the universal objects still don't exist. For instance, in a category with exponentials I can define a silly exponential $X \uparrow Y$, when it exists, to be an object such that $\mathrm{Hom}(Z,X\uparrow Y) \cong \mathrm{Hom}(Z^X, Y)$, naturally in $Z$. If such an object exists for fixed $X$ and all $Y$, this would amount to the existence of a right adjoint to exponentiation by $X$. These objects don't typically exist in presheaf toposes.

The thing that would preclude this here i think is that the naturality in $Y$ is property rather than structure and can't be internalized easily imo. Maybe the deal with sheaf topoi is that they have quantifiers, which could make the naturality condition "internalizable".

Josselin Poiret (Aug 02 2022 at 15:13):

note that above we only had the existence of point-wise exponents, formulating that an object is exponentiable is another matter i think

Morgan Rogers (he/him) (Aug 02 2022 at 15:14):

The thing I described typically doesn't even exist pointwise except for special choices of the objects.

Josselin Poiret (Aug 02 2022 at 15:19):

hmm, though nothing is stopping me from defining $(F \uparrow G)(X) = Hom(yX^F, G)$, right? Then I could say that $X, Y \in C$ admit a silly exponential if we have $X \uparrow Y$ st $y(X \uparrow Y) \simeq yX \uparrow yY$.

Josselin Poiret (Aug 02 2022 at 15:20):

you could even consider these silly exponentials existing without an internal exponentiation

Josselin Poiret (Aug 02 2022 at 15:21):

(I haven't checked this reduces to your case in case it does exist, let me see if that's the case instead of going on a wild goose chase)
actually by yoneda it does i think

Morgan Rogers (he/him) (Aug 02 2022 at 16:38):

Indeed, if they exist they're preserved and reflected by Yoneda, I was pointing out that you can't use your original observation to define them, we have to use the universal property (and we can iterate the universal property to avoid needing exponentials, as you pointed out).

Morgan Rogers (he/him) (Aug 11 2022 at 15:43):

@Josselin Poiret did you find some nice examples?
@William Troiani this is the discussion I mentioned.

William Troiani (Aug 11 2022 at 15:48):

Nice, this is exactly what I was thinking about, thanks for linking me.

I think the category of lambda terms in my paper with Dan Murfet would be an example: https://arxiv.org/abs/2008.10131 it's natural too because it comes right from the usual definition of simply typed lambda calculus (that is, without product types).

Since we don't have product types, the category does not admit products. However we have arrow types, and hence lambda-abstraction, so maybe there's a notion of exponential sitting there.

Mike Shulman (Aug 11 2022 at 17:26):

I think I didn't see the original question in this thread. Using the Yoneda embedding to define cartesian exponentials in the absence of products is a cute idea. An equivalent way to say it should be that the full subcategory of the presheaf category on the representables is a [[cartesian multicategory]] (since it is a full subcategory of a category with products), and we can therefore ask it to be a closed multicategory.

Josselin Poiret (Aug 12 2022 at 12:58):

Here's a crumb of context: Initially, I was trying to understand Tarski universes in type theory in the most naive way possible. Be aware that this is very sketchy, I'm not sure if some errors made their way into the following.
In a dependent type theory, a universe is a type $\vdash U$ with a dependent type $U \vdash \mathrm{el}$, respectively of types and terms of that type. Then, if you have $\Gamma \vdash A : U$, you get $\Gamma \vdash el(A)$. If you implement that in the naive dependent type theory given by the category $\mathrm{Psh}(C)$, you can define $U: X \mapsto \mathrm{Ob}(C)$ and $\mathrm{el}: X \mapsto \{\text{arrows with source } X\}$ and with projection the morphism that selects the target of a given arrow. That way, when you have $\vdash A : U$ (which is equivalently $A \in C$), you get $\vdash \mathrm{el}(A) = yA$. Now, the idea I had was to define local structures on $U$ like products by, whenever we have $\vdash A : U, \vdash B : U$, just asking for $\vdash A \times B : U$ and an isomorphism $\mathrm{el}(A \times B) \simeq \mathrm{el}(A) \times \mathrm{el}(B)$ (which I'm not sure how to formulate type theoretically without exponentials and identity types). Turns out this works for products and exponentials, but not for concepts that are defined by "mapping out" rather than "mapping in", quite obviously. That's how the definition came out, obviously.
One cool thing though, is that you can do the same for the dual category of copresheaves, and with Isbell duality you can still kind of go around both ways and see mechanically how objects defined by "mapping in" should map out to other objects, even when they don't exist, and reciprocally. You should try it with $A \times B$, it's quite fun and you find a definition quite alike the unwounded exponential definition above, although it won't be enough to define products. I'm not sure if the NNO thing I talked about earlier can be coerced into fitting here, or if that definition is unreachable by those methods.

Mike Shulman (Aug 12 2022 at 17:11):

I think Steve Awodey's paper Natural models of homotopy type theory formulates structure on a universe in a way kind of like that.

Jon Sterling (Aug 13 2022 at 10:37):

By the way, to extend your discussion to things that map out rather than in, the tool you are looking for is orthogonality. Awodey's paper that Mike mentions also gives some examples of this (e.g. for the identity type).

Josselin Poiret (Aug 14 2022 at 08:41):

Jon Sterling said:

By the way, to extend your discussion to things that map out rather than in, the tool you are looking for is orthogonality. Awodey's paper that Mike mentions also gives some examples of this (e.g. for the identity type).

Oh, you're right, I could successfully translate it for coproducts! Although because the filler is not unique, eta-conversion for those type is not admissible, I wonder how important it is for the theory though.

Nathanael Arkor (Sep 23 2022 at 08:36):

I've just spotted that Richard Garner proposed this definition in a categories mailing list post (and essentially suggests they should be examples of [[prounital closed categories]], though this concept wasn't around at the time).

Morgan Rogers (he/him) (Oct 06 2022 at 13:24):

@Josselin Poiret did you write about this anywhere or find more references/examples for categories which have exponentials without products? I'm thinking about "transposed monoids" in this context and it would be interesting to have some contexts in which to think about these things.