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

Topic: How to get Poly from Groth. construction on dependent sets?

André Muricy Santos (Apr 26 2024 at 17:51):

Hi, I and a few others are going through the categorical systems theory book (http://davidjaz.com/Papers/DynamicalBook.pdf) and Example 2.6.2.8 claims that the Grothendieck construction on the indexed category of dependent sets (Set^- : Set^op -> Cat) gives one dependent lenses (morphisms in Poly) but I am struggling to recover this for myself; my map on directions is going FORWARD somehow.

See here, say we have two sets and one bundle living on top of each. A map in the grothendieck construction will consist of a function f : A -> B and a map from S : Set^A to T ∘ f : Set^A (in the CST book, the notation is given two pairs (C, A(C)) and (C', A(C')), a map in the grothendieck construction is given by a function f : C -> C' and a map A(C) -> f(A(C'))). My issue is exactly this: the map A(C) -> f(A(C')) goes forward.
attempt1.jpeg

Here's another drawing I came to while attempting to construct another minimal example:
attempt2.png

In this one I drew the indexing (the dependent sets T and T') explicitly: I see how the f* functor given by T' ∘ f works as a reindexing just fine, but where does one get the map backwards from the bundle on the right to the bundle on the left? This is the question expressed by the orange arrow. That's what would give a map in Poly, right?

André Muricy Santos (Apr 26 2024 at 17:52):

(sorry that in the first drawing i start by referring to the bundles as X and Y then change to S and T)

Spencer Breiner (Apr 26 2024 at 18:23):

Your maps are indeed going in the wrong direction. From Prop. 2.6.2.5:

The category of lenses in C is the Grothendieck construction of the indexed category of opposites of the categories of maps with context...

André Muricy Santos (Apr 26 2024 at 18:43):

omg, yes. I always forget that second opposite. Thanks Spencer. Interesting that this leads to charts/arrow category though...

Dylan Braithwaite (Apr 27 2024 at 18:58):

André Muricy Santos said:

Interesting that this leads to charts/arrow category though...

Yeah that's a good observation! David's book uses this later (in definition 3.5.0.8) to define a generalised version of $\mathcal A$-charts and $\mathcal A$-lenses for any indexed category $\mathcal A$

Bruno Gavranović (Apr 27 2024 at 21:09):

In case it helps, in my thesis (specifically Appendix D, Definition D.10 onwards) I carefully unpack all of this: I define the different variants of the Grothendieck construction, relate them via the 2-functor $\mathsf{op}$ on $\mathbf{Cat}$ (which is the culprit behind the 'opposite category 'confusion), and unpack the details of how $\mathbf{Poly}$ and its close cousins arise from these Grothendieck constructions.

Screenshot_20240427_220243.png