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: theory: category theory

Topic: enriched and internal

Morgan Rogers (he/him) (Apr 06 2020 at 09:31):

Christian Williams said:

This is satisfying; but it depends on the fact that you can interpret sets as discrete categories. The equivalence $\mathrm{Set}/X \simeq [X,\mathrm{Set}]$ does not even make sense for a general (locally cartesian closed) category. But surely there's a way to continue this nice "universal" version of the story to that level of generality...

Any object in a category with pullbacks gives an internal category with object of objects equal to object of morphisms, and identity maps for the structure morphism. You need to do a little work to internalise the idea of presheaves, and while it's not exposed especially well in Johnstone's Sketches of an Elephant, that is what is done in sections B2.3 and B3.2 there.

Christian Williams (Apr 06 2020 at 17:09):

Thanks @Morgan Rogers; I need to think about this. When $C$ is locally cartesian closed, it is in particular self-enriched. Then if $c\in C$ can be made into a trivial internal category, the question is whether it can be translated to an enriched category so that we can ask whether $C/c \simeq [c,C]$.

Christian Williams (Apr 06 2020 at 17:11):

It seems pretty hopeful, but if so that would be awesome. This would fully solidify $\mathrm{Ran}$ as generalizing $\Pi$ and $\mathrm{Lan}$ as generalizing $\Sigma$.

Christian Williams (Apr 06 2020 at 17:12):

Eventually all of the nice dependent type theory that lives in locally cartesian closed categories might be generalized to certain nice bicategories or fibrant double categories. (right above I'm suggesting the case for $V\mathrm{Cat}$ or $V\mathrm{Prof}$.) (but I don't yet know enough DTT to back this stuff up.)

Morgan Rogers (he/him) (Apr 06 2020 at 17:34):

Christian Williams said:

Thanks Morgan Rogers; I need to think about this. When $C$ is locally cartesian closed, it is in particular self-enriched. Then if $c\in C$ can be made into a trivial internal category, the question is whether it can be translated to an enriched category so that we can ask whether $C/c \simeq [c,C]$.

For a small category written as an internal category in Set, we construct homsets via pullbacks:
WhatsApp-Image-2020-04-06-at-19.29.08.jpeg
This picture works in any cartesian-closed category, and any LCC category if you replace concrete objects (morphisms $1 \to C_0$) with "generalised objects" (morphisms from arbitrary objects to $C_0$), and since the result is an object of the ambient category it's definitely enriched in the way you want. I'll leave you to check under what conditions this hom construction has the universal property it's required do have, though.

Morgan Rogers (he/him) (Apr 06 2020 at 17:35):

I may not have given enough context about internal categories for this to make total sense; let me know if you want a better explanation of the background or the diagram above!

Christian Williams (Apr 06 2020 at 17:37):

Yes, I understand. Maybe we can move this to a new topic.

Christian Williams (Apr 06 2020 at 17:41):

We were starting to discuss in the Sheaves reading group about the relation between enrichment and internalization.

In "Enriched and internal categories: an extensive relationship" https://www.researchgate.net/publication/321664282_Enriched_and_internal_categories_an_extensive_relationship
there is an adjunction between $V$-enriched categories and categories internal to $V$.

Christian Williams (Apr 06 2020 at 17:42):

-- provided that $V$ is "extensive"; it has some notion of disjointness of coproducts, so that you can "pull apart" the thing of morphisms $C_1$ into homs indexed by pairs of objects.

Christian Williams (Apr 06 2020 at 17:43):

Morgan Rogers said:

Christian Williams said:

Thanks Morgan Rogers; I need to think about this. When $C$ is locally cartesian closed, it is in particular self-enriched. Then if $c\in C$ can be made into a trivial internal category, the question is whether it can be translated to an enriched category so that we can ask whether $C/c \simeq [c,C]$.

For a small category written as an internal category in Set, we construct homsets via pullbacks:
WhatsApp-Image-2020-04-06-at-19.29.08.jpeg
This picture works in any cartesian-closed category, and any LCC category if you replace concrete objects (morphisms $1 \to C_0$) with "generalised objects" (morphisms from arbitrary objects to $C_0$), and since the result is an object of the ambient category it's definitely enriched in the way you want. I'll leave you to check under what conditions this hom construction has the universal property it's required do have, though.

copying this over.

Christian Williams (Apr 06 2020 at 17:44):

Thanks, I need to work through this now.

Christian Williams (Apr 06 2020 at 17:45):

Certainly a lot of information will be destroyed in the process, but I know it will work.

Christian Williams (Apr 06 2020 at 17:49):

So, let $c\in C$ be any object in a locally cartesian closed category. It could be made into a trivial internal category with identity morphisms for structure maps, or it could be made into an enriched category by the way Morgan is describing. There, the set of objects is given by the hom-set $C(1,c)$.

Christian Williams (Apr 06 2020 at 17:51):

WhatsApp-Image-2020-04-06-at-19.29.08.jpeg
copying the picture over for reference.

Christian Williams (Apr 06 2020 at 17:54):

Then given two such points $x,y:1\to c$, the hom "$c(x,y)$" is constructed by the pullback described above. However since the structure maps of $c$ are just identity morphisms, we have $[x,-]\to c$ is still $x$ and $[-,y]\to c$ is still $y$. Then what is the pullback of two points $x,y:1\to c$? In $\mathrm{Set}$ it's trivial, but maybe it's not in general...

Christian Williams (Apr 06 2020 at 17:57):

Ah yeah, since $1$ is terminal, taking the pullback of points must be terminal if $x=y$, and empty otherwise.

Christian Williams (Apr 06 2020 at 17:58):

So this is only recreating the "sets as discrete categories" phenomenon, and nothing more. I guess it's not that surprising, because we were really trying to squeeze water from a stone.

Christian Williams (Apr 06 2020 at 18:00):

In general internal categories are great and powerful; it's just the image of $C\rightarrowtail \mathrm{Cat}(C)$ that's not very interesting.

Christian Williams (Apr 06 2020 at 18:05):

But you were also describing a more general idea, where you are making $C/c$ enriched using these pullbacks, applied not to points but generalized elements of $c$. That is promising... but that seems to go in another direction than the goal of $C/c \simeq [c,C]$. If $c$ as a $C$-enriched category is trivial... well, actually even then I suppose $[c,C]$ is still $C$-enriched. Hm.

Christian Williams (Apr 06 2020 at 18:05):

It seems like a long shot, but so far I haven't found any evidence that it's impossible. I'll keep thinking.

Christian Williams (Apr 06 2020 at 18:08):

[The motivation for this conversation is
https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category.20theory/topic/Reading.20group.20on.20.22Sheaves.20in.20Geometry.20and.20Logic.22/near/192989321 -- I was trying to make a canonical proof of quantifiers as adjoints by thinking of existential/universal as $\mathrm{Prop}$-enriched left/right Kan extensions. Right now this only works for $\mathrm{Set}$, and it would be great to generalize this to any locally cartesian closed category.]

Christian Williams (Apr 06 2020 at 18:13):

It's probably not going to work. Given $p:d\to c, q:e\to c$ this hom would be just their pullback. But in the proof of the $\Pi,\Sigma$ adjoints for an LCCC, they of course depend on the actual internal hom of $C/c$, which is different. So this is probably wishful thinking.

Christian Williams (Apr 06 2020 at 18:14):

But any way, people please share thoughts and ask questions. This is a more general topic about the connection of enrichment and internalization.

Cody Roux (Apr 07 2020 at 01:33):

Yea, I had a question a while back about how to state and prove the Yoneda lemma for internal presheaves. Is there a good reference for this? What are sufficient conditions?

Mike Shulman (Apr 07 2020 at 02:56):

In my totally biased opinion, a nice place for comparing internal and enriched categories is a context that includes them both.

Cody Roux (Apr 07 2020 at 13:18):

Cool!

Christian Williams (Apr 07 2020 at 17:20):

Yes, absolutely. Do you have ideas for how left/right Kan extension generalize quantifiers as adjoints?
($\mathrm{Lan}_p \sim \exists_f$ and hopefully $\Sigma_f$ ; $\mathrm{Ran}_p \sim \forall_f$ and hopefully $\Pi_f$)

Cody Roux (Apr 07 2020 at 19:24):

I feel like @Ryan Wisnesky is quite well placed to answer this question...

Stelios Tsampas (Apr 07 2020 at 19:30):

@John Baez This might be on the wrong stream :rolling_on_the_floor_laughing:

John Baez (Apr 07 2020 at 19:57):

My Zulip often shows one topic with another name right on top of it.

Nathanael Arkor (Apr 07 2020 at 19:58):

if you click on the correct topic, it will focus in on that one

Nathanael Arkor (Apr 07 2020 at 19:58):

(if you just click on a stream, or "All messages", it will show multiple topics at once, which can be confusing)

John Baez (Apr 07 2020 at 20:25):

Yup. But I usually want to plow through "All messages" at once. I just gotta be careful.

Ryan Wisnesky (Apr 07 2020 at 20:42):

the question is how left/right Kan extensions generalize quantifiers? yes, we find the left Kan extensions correspond to an existential like thing that in CQL we call sigma and right Kan extensions to a universal like thing that in CQL we call pi. We tend to think of them as 'changing a schema' as opposed to 'quantifying' anything, however

Cody Roux (Apr 07 2020 at 20:44):

Hey Ryan! There's a similar situation in dependent types, of course, where sigmas and pis are more proof relevant than the simple quantifiers in logic. But maybe there's an additional texture to the Kan extensions?

Dan Doel (Apr 07 2020 at 20:45):

The LCCC Σ and Π are a bit odd with respect to type theory, because they combine things that are typically separate in the latter.

Dan Doel (Apr 07 2020 at 20:47):

It only corresponds to type theory if $f$ is a 'projection', basically.

Dan Doel (Apr 07 2020 at 20:55):

(Hence all the other notions that try to match type theory more closely, I suppose.)

Gershom (Apr 07 2020 at 20:57):

I thought the only gripe against LCCC models was that they were extensional. (oh and they needed to be fixed up because of some laxness issue present in the first, simplest, formulation of such).

Dan Doel (Apr 07 2020 at 20:58):

That's not my only gripe. :mischievous:

Cody Roux (Apr 07 2020 at 22:01):

We're getting dangerously off-topic here, but I wouldn't hate a "LCCCs as models of type theory" discussion as well

Nathanael Arkor (Apr 07 2020 at 23:06):

Dan Doel said:

The LCCC Σ and Π are a bit odd with respect to type theory, because they combine things that are typically separate in the latter.

just to clarify, are you referring to morphisms representing both terms and (dependencies of) types?

Dan Doel (Apr 08 2020 at 00:04):

No, I mean that you can do stuff like $Σ_{\mathsf{suc}}$.

Nathanael Arkor (Apr 08 2020 at 00:11):

I think this is part of what I was trying to say: you only expect to be able to take dependent sums/products of display maps, which are the types/projections, but in a LCCC you can take dependent sums/products of any morphism, including ones corresponding to term (operators), like $\mathsf{suc}$

Dan Doel (Apr 08 2020 at 00:13):

Oh, yes.

Dan Doel (Apr 08 2020 at 00:17):

If you think hard enough, you can imagine anything is a display map, but that doesn't really reflect what type theory is like very well.

Christian Williams (Apr 08 2020 at 00:20):

Yes, this is my fault for not bringing this back to: https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category.20theory/topic/Reading.20group.20on.20.22Sheaves.20in.20Geometry.20and.20Logic.22/near/193071011

Jacques Carette (Jun 09 2020 at 00:42):

Is there an "enriched category theory done slowly with lots of details"? In particular, I'm currently looking at understanding how a closed monoidal category can be seen as enriched over itself, and the details are... elusive. Everything I've found up to now is very sketchy with the details.

Joe Moeller (Jun 09 2020 at 00:47):

I don't have a reference like you're asking for, but what should be the first step in understanding this fact is that V closed => V has internal hom => hom sets are objects in V => V is V-enriched. This is the broad idea. Perhaps most writing about this would expect this is enough for the reader to fill in further details.

Joe Moeller (Jun 09 2020 at 00:48):

Was this broad idea part of what you wanted clarified, or is it just the finer-grain details?

Gershom (Jun 09 2020 at 01:35):

Does Kelly's book not provide sufficient details? (note: I had always thought this was the basic text, and I'm genuinely curious here)

Joe Moeller (Jun 09 2020 at 01:40):

I guess I had assume that Jacques wasn't satisfied with the details in Kelly.

Joe Moeller (Jun 09 2020 at 01:41):

If this isn't the case, please see if you like this: http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf
As Gershom says, it is the standard reference.

Jacques Carette (Jun 09 2020 at 02:33):

I understood the high-level ideas (but thanks). I'm trying to formalize it all - and that's very detail hungry. Kelly's book is still under-detailed - but I'll try again. p.14-15 does seem to have a bit more than other places I've seen.

Evan Patterson (Jun 09 2020 at 02:40):

FWIW, I find Chapter 3 of Riehl's book Categorical Homotopy Theory, available here, to be more readable as an introduction than Kelly's book, although being a single chapter it doesn't cover nearly as much material.

Jacques Carette (Jun 09 2020 at 03:32):

@Evan Patterson That helped. Once I figured out what "is adjunct under [adjoint relation] to ..." meant (that was the hard part!!), then the rest was very precise indeed. That still leaves me with 3 non-trivial proof obligations, but they look doable.