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: Units in a VDC


view this post on Zulip Noah Chrein (Jan 25 2021 at 18:45):

Hello! I realized I took something for granted in my first read-through of CS09, but I'm having trouble constructing it.

In a Virtual Double Category with units, given a vertical XfYX\overset{f}{\to}Y How does one induce UfU_f ? (see image) Capture.PNG

Thanks!

view this post on Zulip fosco (Jan 25 2021 at 22:13):

There is indeed no explicit definition of UfU_f in the paper (or so it seems after a superficial ctrl-F)! Strange. Isn't it likely that one gets UfU_f with a factorization along a cartesian cell, instead than just from units?

view this post on Zulip Noah Chrein (Jan 25 2021 at 23:57):

I guess that's possible, but it seems like several of the propositions in chapter 5/6 rely on it's construction, but only assume opcartesian cells (and sometimes only units). e.g. T5.2, P5.14, and P6.1

I assume it's not included because it's so glaringly obvious.

There is, however, an analog I tried to follow:

MulticatMonoidalcatVirtualDblPsuedoDblMulticat \to Monoidalcat \sim VirtualDbl \to PsuedoDbl

The monoidal identity in the former case comes from the null list in the free monoid, where-as the analog in virtual double categories would be the empty path in the free category... but I don't yet know how to parse this info into a UfU_f

view this post on Zulip fosco (Jan 26 2021 at 09:07):

I don't have an answer; my suggestion was motivated by the fact that UfU_f must have a universal property of some sort. Since (e.g. in the proarrow equipment of profunctors of small categories) UfU_f is the cell that represents the action of a functor on morphisms, and this is a Kan extension on its own right...

view this post on Zulip fosco (Jan 26 2021 at 13:32):

I don't remember if this is legitimate (I always confused vdcs and augmented vdcs...) but perhaps it works?

image.png

I used opcartesianity of the unit of AA, and a "whiskering" with ff.

view this post on Zulip Mike Shulman (Jan 26 2021 at 15:46):

UfU_f is induced by the universal property of UXU_X applied to the composite of the defining universal cell of UYU_Y with ff. Possibly we neglected to define it explicitly.

view this post on Zulip Noah Chrein (Jan 26 2021 at 15:52):

Thanks! So this is what fosco said... this is also what I "took for granted" in my first reading. However, f is not a cell it is just a vertical morphism...

how do we "whisker" vertical cells with vertical morphisms in a VDC?
(I assumed this whiskering required UfU_f apriori)

view this post on Zulip Noah Chrein (Jan 26 2021 at 16:17):

ah, from the direct axioms of a VDC it is not so clear that one can compose with "null length cells" or just vertical morphisms. But this is actually clear from the fc-multicategory perspective.

Sorry for the dumb Q, but thanks for the help!

view this post on Zulip Mike Shulman (Jan 26 2021 at 17:32):

It's not dumb; I agree we weren't as clear about these points as we could have been.

view this post on Zulip fosco (Jan 26 2021 at 20:36):

The paper is very insightful, IMO you've written something that deserves a lot attention.

@Noah Chrein , I would be interested in knowing why you're studying vdcs :-) I was a fan before it was cool (...is it cool now?), and I still hope I can share my passion with more people :grinning:

view this post on Zulip Noah Chrein (Jan 27 2021 at 20:39):

@fosco yes I assume it became cool this past semester, or at least that's when I learned it from the JHU Cat seminar.

I have a toy model for ontology that requires a formal notion of composition that behaves a lot like Prof / Span. VDCs provide notational convenience in this setting, but I'm also using them to try to understand which ontologies behave like categories via the existence of a yoneda-esq structure (and I call these "yoneda ontologies").

Actually it was your yosegi box paper that originally let me to Shulman/Cruttwell :)

view this post on Zulip fosco (Jan 27 2021 at 21:44):

Oh, yes, now I remember, we've had a conversation about that! What is an ontology again?

view this post on Zulip Noah Chrein (Jan 27 2021 at 22:02):

Broadly speaking its just an "expressive collection of data". It's like when you work with a new class of objects and you don't know it's structure, so you originally call it a "set" and then find it's morphisms or whatever, so you start calling it a "category" and then you realize it has a topology, higher coherance data, bells and whistles, etc. so you call it progressively more complicated names.

"Ontology" is just a word you can use to mean "I don't exactly know what structure this collection has, but I will keep upgrading it as I learn". Instead of claiming immediately that some collection is, ie, a category, you can call it an ontology to signal that it likely has more layers of expressive data.

The main point of the theory (of categories or other "categorical" forms of ontologies) seems to be how one determines objects from the ambient ontological data. One example is the yoneda embedding for categories, so I'm trying to understand this intuition through yoneda-ish formal reasoning. Seems like VDCs are (almost) expressive enough of a setting to formalize all this.