Tobias Schmude

Stream: new members

[Tobias Schmude]

Hey everyone! My name is Tobias, I'm a PhD student, and I'm currently working on various generalizations of the Grothendieck construction. I'm thinking about contributing to mathlib by formalizing my work in Lean. Upon skimming the category theory part of mathlib I couldn't find anything in that direction yet, but if there are already some plans for that, I'd love to hear about them and collaborate!

[Tobias Schmude]

The contribute file mentions I should include my GitHub username for write access, so here it is: Tobias-Schmude.

[Junyan Xu]

Hi welcome! If you are talking about docs#category_theory.grothendieck, I have generalized it to take an (op)lax functor at branch#lax_grothendieck and proved a bunch of stuff about it (most importantly existence of (co)limits), but have not migrated it to use the docs#category_theory.bicategory framework. I haven't had time to work on it since February, and your help would be very welcome. (Partial progress of the migration/adaptation is at branch#lax_grothendieck_bicat.)

[Tobias Schmude]

Ah, yes, that's part of what I was looking for! As a first step, I'd like to formalize the generalized Grothendieck equivalence of Bénabou , i.e. the equivalence $\mathrm{Cat}/\mathcal{B} \cong \mathrm{Lax}_\mathrm{norm}(\mathcal{B}^\mathrm{op}, \mathrm{Prof})$, where the action on objects of the pseudofunctor from right to left is given by your construction.

[Tobias Schmude]

*almost, we'd have to generalize to $\mathrm{Prof}$ first.

[Tobias Schmude]

I've written "first step", but depending on how much of the preliminaries has to be formalized first, this might be a lot of work. I can't judge that yet.

[Tobias Schmude]

If I see correctly, you're defining lax functors into $\mathrm{Cat}$ directly, since neither the bicategory $\mathrm{Cat}$ nor lax functors of bicategories are available (correct me if I'm wrong!).
It might be a good start for me to formalize these concepts first to get familiar with Lean. I have some experience with Coq-UniMath, so let's see how well this transfers :grinning_face_with_smiling_eyes:

[Junyan Xu]

docs#category_theory.Cat.bicategory and docs#category_theory.oplax_functor have been added to mathlib since I did that work! I want to adapt my code to use them but lost the momentum.

[Junyan Xu]

Unfortuantely I'm not a category theory expert and my motivation mainly comes from algebraic geometry; I'm not sure what Prof stands for?

[Tobias Schmude]

Junyan Xu said:

docs#category_theory.Cat.bicategory and docs#category_theory.oplax_functor have been added to mathlib since I did that work! I want to adapt my code to use them but lost the momentum.

Hm, for some reason I didn't see them :neutral:

[Tobias Schmude]

Junyan Xu said:

Unfortuantely I'm not a category theory expert and my motivation mainly comes from algebraic geometry; I'm not sure what Prof stands for?

By $\mathrm{Prof}$ I mean the bicategory of profunctors: 0-cells are small categories, 1-cells $\mathcal{C} \to \mathcal{C}'$ are profunctors, i.e. functors $\mathcal{C}'^\mathrm{op} \times \mathcal{C} \to \mathrm{Set}$, and 2-cells are natural transformations.

An arbitrary functor $\mathcal{C} \to \mathcal{B}$ does not induce functors between its fibers, only profunctors. That's why they are relevant here.

[Tobias Schmude]

You might also have heard of profunctors under the names "distributors" or "bimodules".

[Anne Baanen]

Tobias Schmude said:

The contribute file mentions I should include my GitHub username for write access, so here it is: Tobias-Schmude.

Invite sent: https://github.com/leanprover-community/mathlib/invitations

[Junyan Xu]

You might also have heard of profunctors under the names "distributors" or "bimodules".

Incidentally there's an open PR #14402 "define the bicategory of algebras and bimodules internal to some monoidal category". I guess it's directly related to this paragraph in nLab?
image.png

[Tobias Schmude]

Yep, they seem to be defining a special case of a generalization of what I'd like to define. The common generalization would be enriched profunctors(/distributors/(bi)modules/correspondences), which I think will be way more of a hassle than the $\mathrm{Set}$-enriched case.