This is a companion discussion topic for the original entry at https://forest.localcharts.org/ocl-001x.xml
This is a companion discussion topic for the original entry at https://forest.localcharts.org/ocl-001x.xml
The \alpha in the second diagram should be pointing in the opposite direction, I changed it and it displays that way locally, but seems to not be updating even though the build worked… Someone should tell the sysadmin 
Nice construction! As you know, we’ve used both of these categories (the “charts” and the “lenses”) in the papers on diagrammatic equations (1, 2), but not both together in the form of a double category. I wonder if the double category could be used to frame in any interesting constructions. Beyond that, I wonder if using the intuitions from “charts” and “lenses” is helpful here. I haven’t thought about diagrammatic equations in those terms—but then again, I’m not in the habit of thinking about lenses, so it might well be a natural perspective.
2 Likes
One fun thing about these “diagram charts/lenses” is that they take part in a sort of microcosm principle for the Grothendieck (aka chart/lens) construction. Namely, if E : B^{\mathsf{op}} \to \mathsf{Cat} is an indexed category and \mathsf{Chart}(E) is its Grothendieck construction and \mathsf{Lens}(E) the Grothendieck construction of the pointwise opposite, then E lifts against the forgetful functor \mathsf{Diag}^{\to}(\mathsf{Chart}(E)) \to \mathsf{Cat} and \mathsf{Diag}^{\leftarrow}(\mathsf{Lens}(E)) \to \mathsf{Cat}, in each case by equipping E(b) with the functor interpreting it as a vertical chart or lens. Even more, \mathsf{Chart}(E) and \mathsf{Lens}(E) are determined as the initial lifts of E through \mathsf{Diag}^{\to} or \mathsf{Diag}^{\leftarrow}. This is just another way of saying that the Grothendieck construction is the (op)lax colimit of the diagram of categories E.
3 Likes
What is a “microcosm principle”? And what does it meant to lift against a forgetful functor?
The microcosm principle is a Baez-Dolan coinage remarking on how you need to be in a monoidal category to define a monoid, and in a monoidal 2-category to define a monoidal category, and in a monoidal 3-category to define a monoidal 2-category…
By saying that E : B^{\mathsf{op}} \to \mathsf{Cat} lifts against f : \mathsf{Diag}^{\to}(\mathsf{Chart}(E)) \to \mathsf{Cat} I mean there is a functor \hat{E} : B^{\mathsf{op}} \to \mathsf{Diag}^{\to}(\mathsf{Chart}(E)) so that f \circ \hat{E} = E. By the initial lift I mean that if L : B^{\mathsf{op}} \to \mathsf{Diag}^{\to}(C) is any other lift (f \circ L = E), then there is a unique functor \ell : \mathsf{Chart}(E) \to C so that \mathsf{Diag}^{\to}(\ell) \circ \hat{E} = L.