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: Getting pseudofunctors from representable profunctors

Patrick Nicodemus (Jan 09 2024 at 12:00):

It's a well-known theorem of 1-category theory that if $F : C\to\hat{D}$ is a profunctor from $C$ to $D$, and for each $c\in C$ there is a representing object $\overline{F}(c)$ for $F(c)$ in $D$, such a choice extends uniquely to a functor $\overline{F}:C\to D$ which is a lift of $F$ along the Yoneda embedding up to natural isomorphism.
I am wondering whether there are analogous theorems for bicategories and pseudofunctors, it would be nice to get the coherence conditions for a pseudofunctor "for free" somehow as a result of applying this theorem.

Patrick Nicodemus (Jan 09 2024 at 12:02):

Like intuitively it seems to me that if you define a pseudofunctor between bicategories by a choice of object satisfying a universal property then the rest of the argument for the coherence 1 and 2 cells is often quite mundane to write down, there should be a more general theorem I can cite here.

Mike Shulman (Jan 09 2024 at 16:40):

It's definitely the case that pseudofunctors can be constructed in this way. For instance, in Cartesian bicategories, II a bicategorical tensor product is constructed by using a universal property of a cartesian product, as we usually do for 1-categories. However, I'm not sure whether it can be formulated in a general way that would actually save any work; it seems to me, at least a priori, that a "pseudoprofunctor" would have just as many coherence laws as a pseudofunctor.

Mike Shulman (Jan 09 2024 at 16:42):

I suppose in particular cases you might be able to apply a general toolbox for constructing pseudoprofunctors.

Mike Shulman (Jan 09 2024 at 16:43):

Alternatively, you could try a bicategorical generalization of [[anafunctors]]. That would also have the advantage of not requiring a particular variance of universal property.

Patrick Nicodemus (Jan 09 2024 at 16:43):

Yes that's true. I was thinking that maybe because the Cat is a strict 2 category it might be easier to construct functors into it.

Patrick Nicodemus (Jan 09 2024 at 16:44):

Like perhaps in some cases the universal property could be a strict pseudofunctor even though the lift along the Yoneda embedding cannot be made strict.

Mike Shulman (Jan 09 2024 at 16:55):

It's possible, but it seems unlikely to me, given that e.g. even the representable pseudofunctors of a general bicategory are not strict.

Mike Shulman (Jan 09 2024 at 16:56):

It might be more likely if you started with a strict 2-category.

Patrick Nicodemus (Jan 09 2024 at 22:36):

Mike Shulman said:

It's possible, but it seems unlikely to me, given that e.g. even the representable pseudofunctors of a general bicategory are not strict.

Sure. There's some conservation of work principle at play here. I am just being lazy here.
For example we don't have to explicitly prove functoriality when constructing a left adjoint to G because we can appeal to the more general principle that Hom(_, G_) is a distributor for an arbitrary functor G. This is the kind of thing I'm hoping to take advantage of. It should be possible to construct left adjoint pseudofunctors easily by specifying their behavior on 0 cells and 1 cells.

Mike Shulman (Jan 10 2024 at 16:04):

Actually 0-cells should be enough!

Patrick Nicodemus (Jan 10 2024 at 23:31):

Mike Shulman said:

Actually 0-cells should be enough!

Yes this is true. I was thinking more along the lines of, what data do you need to supply before you get a _unique_ extension. I think it should be the 0 cells, 1 cells and the unit pseudonatural transformation.

Mike Shulman (Jan 11 2024 at 00:39):

Well, "uniqueness" of a pseudofunctor should "really" be understood in an up-to-equivalence sense anyway...

Patrick Nicodemus (Jan 11 2024 at 01:20):

@Mike Shulman I have a more philosophical question here which is again driven by laziness. I agree that specifying the 0-cells should be enough to determine a pseudofunctor which is left adjoint to a given pseudofunctor, and we can sit down and work this out and appeal to the coherence conditions. This is fine, if a bit tedious. My question is that why do we claim to know that this is the case without having actually checked the coherence conditions for how a pseudofunctor should play with the associator and lax unity / composition constraints. It is obvious that it should be correct but why is it obvious? Is there a fully rigorous proof of this theorem that does not proceed by directly constructing it and checking the coherence conditions for a pseudofunctor? I am willing to accept an argument that pushes the result elsewhere behind a black box such as the bicategorical Yoneda lemma or even an argument that is partially circular if it is at least conceptually illuminating. I am just curious whether this intuition that "because it is constructed in a natural way, it should be functorial" can be turned directly into a rigorous proof that does not amount to chasing the diagrams.

I would also be curious if one can prove this theorem (or get other such general theorems about constructing pseudo/lax functors and natural transformations) through a proof by appeal to a higher abstraction (for example, using operads or opetopes) in a way that makes it clear why the coherence conditions should hold, even if at the end of the day we still have to do the higher combinatorics.

Patrick Nicodemus (Jan 11 2024 at 01:25):

For example, do we have explicit theorems about constructing functors by left adjoints or universal properties for any/all of these? Are they conceptually illuminating?
https://ncatlab.org/nlab/show/algebraic+definition+of+higher+categories

Patrick Nicodemus (Jan 11 2024 at 02:02):

Mike Shulman said:

Actually 0-cells should be enough!

This is theorem 1.30 of "Fibrations in Bicategories" by Street. No proof is given. Mathematicians are wont to dismiss such tedious verifications and leave them as an exercise for the reader. I might even speculate that Street himself did not even check this theorem carefully given that theorems 1.24 and 1.25 in this paper are incorrect. I feel that if your (not you you, the general "you") attitude is "I am not obligated to check the details because this is trivially true and verification is left to the reader" then there should be an actual clear proof that it's trivially true that does not involve pages of tedious, error-prone equational reasoning which is not very enlightening, and I think it's an interesting challenge to come up with clear rigorous proofs of such theorems which are as concise as our intuitive mental reasoning.

John Baez (Jan 11 2024 at 03:14):

I agree with the last point. One reason I gave up working on n-categories is that there were too many results that felt obvious that I could only prove through pages of tedious, error-prone equational reasoning. I figure the right approach is to patiently build up the right ways of thinking n-categorically to make these results have concise or at least conceptually clear rigorous proofs. But I didn't have what it takes for that. It probably requires a big community effort, like what we're seeing in homotopy type theory.

Mike Shulman (Jan 11 2024 at 04:00):

It's an interesting question! To start with,

I feel that if your attitude is "I am not obligated to check the details because this is trivially true and verification is left to the reader" then there should be an actual clear proof that it's trivially true that does not involve pages of tedious, error-prone equational reasoning which is not very enlightening

I'm not sure I agree with that. I think pages of tedious reasoning can in some cases still be considered "trivial". For instance, if it's entirely mechanical and you could easily program a computer to do it. Or if all you have to do is "follow your nose", even if it takes a long time for your nose to get there.

Of course "follow your nose" also has a "you" problem: maybe all Street had to do was follow his nose, but the average reader may not have as well-developed a nose. In the future, maybe we'll have zoomable wiki mathematics papers where whoever feels the need to write out the proof explicitly can do it and provide a link to expand it out for whoever else feels the need to read it.

Mike Shulman (Jan 11 2024 at 04:04):

As for why it's obvious, I think part of it is just based on experience proving other similar things, where it always works out. There's a sort of general intuition that anything you can do with categories you can do with bicategories and higher categories... except for the things you can't.

Patrick Nicodemus (Jan 11 2024 at 04:11):

Yes, certainly a fundamental obstacle to proving general theorems of the form "The intuitive argument works" is that the result may be false which is why we have to check.

Since the tricategory of bicategories can be strictified to a Gray category I wonder if you could rephrase this coherence result to give a nice metatheorem of the form "any argument that works for 2-categories and doesn't rely on the interchange law goes through for bicategories."

Mike Shulman (Jan 11 2024 at 04:38):

It certainly is possible to prove some general theorems, and when working with, say, $(\infty,1)$-categories that's what people often do (at least when they're trying to be rigorous). You can also sometimes get some mileage out of working at homotopy-category level, e.g. there is a proarrow equipment of bicategories and pseudofunctors that you can use to talk about some limits and stuff in the same formal language that works for 1-categories (but that doesn't help for this particular example).

Patrick Nicodemus (Jan 24 2024 at 16:02):

Mike Shulman said:

Well, "uniqueness" of a pseudofunctor should "really" be understood in an up-to-equivalence sense anyway...

I am still thinking about this. This is a good point but what is going through my mind is that a bicategory is of course a 2 categorical structure and there are is an appropriate notion of uniqueness to an n category. Usually an object in a bicategory satisfying a universal property is unique up to equivalence, an object in a category satisfying a universal property is unique up to isomorphism, and we could maybe say an element of a set satisfying a "universal property" is unique up to equality, the appropriate notion of equivalence in a 0 category.
So it was interesting for me to realize that there are shades of grey in between, that once I fix certain 0 objects and 1 cells in the adjunction, there is a 0-categorically unique choice of extension to a full fledged adjunction. This got me wondering if there is a larger n categorical principle here: a 0 cell satisfying an n-universal property is unique up to n-equivalence but a 0 cell is not the only data that needs to be supplied for the n-universal property, one also should fix an n-equivalence of presheaves Hom(_,c)\cong P. This got me wondering if there is some kind of principle that if you supply the k- dimensional part of an object defined by a universal property then it can always be extended to the full data of the universal property and this extension is unique up to (n-k) equivalence.

Mike Shulman (Jan 24 2024 at 16:05):

That sounds about right, but I don't know of a formal statement.

Patrick Nicodemus (Jan 24 2024 at 16:25):

If I want to define a left adjoint to a functor between bicategories

1. I have to choose as to where to send the objects and this is unique up to equivalence
2. I have to choose where to send the 1 cells and this is unique up to isomorphism
3. I have to choose where to send the 2 cells and this is unique up to equality

On some level this is a tautology because of course a cell in an n category can only be unique up to n equivalence. But this is also an oversimplification because I'm missing the lax unit and composition constraints and it's not clear that you can choose totally arbitrarily all the structure up to level k and still get an (n-k)-unique extension that fixes all the coherence problems suppressed up till that point. Maybe the initial k-structure should be k- coherent but it's not clear it makes sense to talk about k coherence in an n category when k < n.

I don't know how to analyze this rigorously. Maybe Trimble n-categories are appropriate here.

More generally I am wondering what the mathematical content is of the idea that like, some of the data of an categorical construction is inessential because it is always uniquely determined by the other data.

For example (speaking 1 categorically for simplicity) there should be an isomorphism of categories between left adjoints to P : C -> D and |Ob(C)|-indexed families of universal arrows into P. One apparently involves less data

Mike Shulman (Jan 24 2024 at 16:28):

BTW "lax" usually refers to things that are not necessarily invertible. The unit and composition constraints of a pseudofunctor are invertible, hence "pseudo" rather than "lax".

Patrick Nicodemus (Jan 24 2024 at 16:31):

Yes definitely.

Mike Shulman (Jan 24 2024 at 16:31):

(You said "lax unit and composition constraints".)

Mike Shulman (Jan 24 2024 at 16:32):

Anyway, yes, there is something to figure out how to state and prove rigorously here, and it's not as obvious as it might appear. For instance, if a given 1-cell $f$ in a bicategory is invertible, then the choice of an inverse $g$ and isomorphisms $f g \cong 1$ and $g f \cong 1$ is not unique. They become unique if the isomorphisms are required to satisfy the triangle identities, making $(f,g,\eta,\epsilon)$ an adjoint equivalence. But if $f$ and $g$ are already chosen, then the choice of $\eta$ and $\epsilon$ making an adjoint equivalence is not unique. However, if one of $\eta$ and $\epsilon$ is also chosen, then the other becomes unique.

Patrick Nicodemus (Jan 24 2024 at 16:51):

Right like in the definition of half adjoint equivalence in HoTT. Maybe something like that is relevant here, proving that there are characterizations of these notions whose type is a proposition

Patrick Nicodemus (Jan 27 2024 at 04:41):

I thought about this some more. I am sure many people have spent lots of time trying to come up with satisfying explanations for why coherence conditions somehow seem to hold automatically, or why we get naturality seemingly for free so often.

Patrick Nicodemus (Jan 27 2024 at 04:42):

I have not checked details in what follows, I am just thinking out loud here. Let $C, D$ be two bicategories. Let $F : C\to\hat{D}$ be a pseudofunctor from $C$ into the (strict, I think?) 2-category of Cat-valued pseudopresheaves on $D$. It is possible to define a Grothendieck construction for $F$, i.e., a tabulation. The objects of $\int F$ are triples $(c, d, x)$ where $x$ is an object in $F(c)(d)$. The 1-cells are pairs of $1$-cells in $C, D$ together with a 2-isomorphism filling in the square, 2-cells are evident. $\int F$ is equipped with two projections $\pi_C,\pi_D$. I think that both of these projections should actually be strict functors, not just pseudo.

Patrick Nicodemus (Jan 27 2024 at 04:42):

Claim: $x\in F(c)(d)$ is a "universal object" (i.e., the induced map $x : y(d)\to F(c)$ is a natural equivalence) iff the triple $(c, d, x) \in \int F$ has the property that for all triples $(c', d,' x')$ in $\int F$, the local hom functor $\pi_C((c, d, x), (c',d', x')): (\int F)((c, d, x), (c',d', x')) \to C(c, c')$ is an adjoint equivalence.

Patrick Nicodemus (Jan 27 2024 at 04:43):

Claim: For each $c$ in $C$, choose $(c, d, x)$ lying over $c$ in $\int F$. Assume that for all such chosen triples $(c, d, x), (c', d', x')$, the local hom functor $\pi_C((c, d, x), (c',d', x'))$ is an adjoint equivalence. Then $F$ is representable. Any family of choices of adjoint equivalences to $\pi_D((c, d, x), (c',d', x'))$ (together with units and counits) extends uniquely (up to equality) to a pseudofunctor $G: C\to \int F$, i.e., the lax unit and associativity cells are determined by the adjoint equivalences, and $\pi_D\circ G$ is a representation of $F$.

Patrick Nicodemus (Jan 27 2024 at 04:43):

I am wondering if this pattern works in general. If we replace bicategories with weak $n$ categories, in a setting where we have a notion of Grothendieck construction / tabulation, given a lift of the 0-cells of $C$ to $\int F$, and given fully coherent weak $n-1$ equivalences for the local functors $\pi_C$, I think it's plausible that these local $n-1$-equivalences (which are all chosen independently with no relationships between them) glue together into a global weak $n$-functor in a unique way (i.e., all remaining coherence isomorphisms are uniquely determined by the structure of the local equivalences)

If we sum this up as "representing n-functors for n-profunctors are determined by choosing independently a family of 0-cells with n-universal properties and then (n-1) local adjoint equivalences", then the k vs n-k idea I mentioned earlier then follows by induction on this principle, in a sense. That is, to construct an (n-1)-dimensional adjoint equivalence, it suffices to choose where to send the 0-cells, and then construct an independent family of (n-2)-dimensional local adjoint equivalences, and so on. As long as you keep choosing the lifts for cells at stage $k$ to have the desired $n-k$ universal property, you can keep going, and your remaining choices form an $(n-k)$-dimensional contractible groupoid.