adjunctions in bicategories

Stream: Is there code for X?

[Mike Shulman]

Does mathlib contain definitions and properties of internal adjunctions in a bicategory?

[Scott Morrison]

Unfortunately no. We have some basic material on rigid categories.

[Mike Shulman]

Ok, thanks. Maybe I will have some students work on it.

[Scott Morrison]

Oh, @Mike Shulman, sorry I had forgotten about this: #13418.

[Mike Shulman]

Thanks! What's the status of it? It looks like it hasn't been updated for
a year?

[Adam Topaz]

Presumably at this point it could just be redone in mathlib4. I think all the requirements have been ported.

[Adam Topaz]

Oh, maybe the coherence tactic hasn’t been ported yet?

[Matthew Ballard]

No but it is only two files away

[Sophie Morel]

I am resurrecting this thread, because I'm currently trying to prove that pseudofunctors between bicategories send adjunctions to adjunctions and getting bogged down in coherence, so I'm wondering whether someone already tried/has a PR that I have missed.

[Joël Riou]

@Yuma Mizuno has developed adjunctions in general bicategories and improved automation of the proof of coherence properties (but it is unclear this interacts well with pseudofunctors).

About adjunctions in bicategories, turns out that I have just worked on a PR #13539 which defines the bicategory of adjunctions in a given bicategory (I defined all the data, but have not even tried to prove compatibilities yet), because this should be useful when formalising certain bifibered categories.

[Sophie Morel]

I am aware of the mathlib files on adjunctions in bicategories, but they don't seem to be imported by anything else, so mathlib at least does not know that a pseudofunctor sends an adjunction to an adjunction. But @Yuma Mizuno might have a proof somewhere!
Anyway, I wrote most of a proof today. (I have the left triangle working for the image adjunction, the proof of the right triangle should be the same mutatis mutandis.)

[Sophie Morel]

By the way, the point for me is to construct limits in categories of group objects. I have formalized the fact that "group object" is a pseudofunctor from the bicategory of categories with finite products (and functors respecting finite products) to the bicategory of categories, so now I want to prove that it sends the "constant-limit" adjunction to an adjunction between categories of group objects.

[Yuma Mizuno]

Sophie Morel said:

I am aware of the mathlib files on adjunctions in bicategories, but they don't seem to be imported by anything else, so mathlib at least does not know that a pseudofunctor sends an adjunction to an adjunction. But Yuma Mizuno might have a proof somewhere!

@Sophie Morel I don't have a proof of that fact, so feel free to develop this direction!

[Adam Topaz]

It seems like we need to build a coherence-like tactic that can handle monoidal functors and pseudofunctors!

[Sophie Morel]

Yuma Mizuno said:

Sophie Morel I don't have a proof of that fact, so feel free to develop this direction!

Thanks for your answer! I guess I'll continue then. In the end I did not use the coherence tactic in the proof, I just unpacked the definition of bicategoricalComp and things did not get too complicated. So maybe there is a better proof.