The bicategory of algebras and bimodules

Stream: maths

[Scott Morrison]

@Yuma Mizuno and/or @Oleksandr Manzyuk may be interested in the branch#semorrison/Bimod I just started with the aspiration of constructing the 2-category of (algebras)/(bimodules)/(intertwiners), (all internal to some monoidal category, e.g. R-mod). This is related e.g. to the Brauer group of a commutative ring R. The new content is in category_theory/monoidal/Bimod.lean.

My summary so far is that it still looks hard! I got as far as constructing the data for the tensor product of two bimodules, but have many scary looking proof obligations. There's constant interplay between the colimits API and the monoidal API in the proofs.

I'm about to disappear for a week or two, but if anyone wants to play with it please go ahead. :-)

[Kevin Buzzard]

Johan always said he wanted Brauer groups but I don't think he was thinking of this! Perhaps for fields the story is far simpler.

[Adam Topaz]

I would have imagined a cohomological description of the Brauer group would come first!

[Kevin Buzzard]

I was imagining that we proved that H^2(k,G_m)=Br(k) by an explicit computation with 2-cocycles (this is continuous group cohomology, which we're slowly working towards at Imperial)

[Adam Topaz]

cocycles? oof. What's the status of Hilbert 90? How close are you to that? (I mean the general statement with $GL_n$)

[Kevin Buzzard]

last I heard we were still struggling to get any definition of group cohomology into mathlib :-/

[Kevin Buzzard]

Amelia is busy with something else right now but I hope to get back to working on this in the near future

[Reid Barton]

I realize you've not quite gotten to the point where this becomes pertinent yet but I would start from the other end--write constant tensor_Bimod and enough of the related structure in order to build the bicategory first, before trying to make an actual definition of tensor_Bimod.

[Reid Barton]

Oh--I see you've made this more difficult with the weak assumptions on the original category

[Scott Morrison]

Yes, the weak assumptions are probably not helping. I've only ever had reason to care about the case of symmetric frobenius algebras in rigid categories, where you can define the tensor product of bimodules as the image of an idempotent rather than as a coequalizer, and that is probably easier (and equivalent to the more general definition I started on).

[Reid Barton]

The main assumption I was thinking would help is that the category is closed monoidal

[Scott Morrison]

The main reason I didn't go there is that we currently on have closed-on-one-side, not biclosed monoidal categories, and in this context I wouldn't want to assume a braiding or symmetry. Thus I just assumed that tensor-on-left and tensor-on-right preserved colimits, which is the immediate consequence of biclosed that seems relevant. I'll think some more to how being biclosed could help.

[Oleksandr Manzyuk]

@Scott Morrison I've started playing with your code (filled in two sorries so far), and I've noticed a small problem with the implementation of pure_coherence: it's not hygienic. When used in a context that has shadowed the definition of id, pure_coherence will fail (as will, of course, coherence). Fortunately, the error message (type mismatch for the type of id) was helpful to quickly pinpoint the issue, but it'd be nice to make the tactic more robust.

[Oleksandr Manzyuk]

I also had to replace the uses of monoidal composition ⊗≫ with plain composition with explicitly constructed isomorphisms inserted because we have no tools to reason about monoidal composition at the moment.

[Scott Morrison]

#13507

[Oleksandr Manzyuk]

FWIW, I've finished the definition of tensor_Bimod (pushed to branch#semorrison/Bimod). I haven't had much time recently, so the progress has been slow, but I intend to continue.

[Oleksandr Manzyuk]

I wanted to start defining a bicategory structure on Mon_ C but it seems just importing category_theory.bicategory.basic causes pesky deterministic timeouts, and I'm not sure how to resolve them. I already had to extract the fields of tensor_Bimod to top-level definitions and lemmas because of deterministic timeouts, and importing category_theory.bicategory.basic causes a deterministic timeout in one of the lemmas, middle_assoc'.

The proofs seem to share a lot of structure, so perhaps there are some useful lemmas that could be extracted to simplify the proofs, but I haven't looked into this yet.

[Scott Morrison]

This does sound unfortunate.

[Scott Morrison]

An obvious workaround is to prove these lemmas, and only import bicategory.basic in a new file.

[Scott Morrison]

Oh -- the obvious explanation for the deterministic timeouts is just all the non-terminal simps. Replacing these with simp only will make your lemmas much more robust to additional imports.

[Oleksandr Manzyuk]

Ah, good suggestion, thank you, I'll try that.

[Oleksandr Manzyuk]

@Scott Morrison I'm hoping you're still interested in this. I've finished the definition of the bicategory and can open a PR now.

[Scott Morrison]

Awesome, yes, I'd love to have a look.

[Scott Morrison]

Remind me what branch it is on?

[Oleksandr Manzyuk]

https://github.com/leanprover-community/mathlib/tree/semorrison/Bimod

[Scott Morrison]

Epic!

[Scott Morrison]

wisker should be whisker

[Scott Morrison]

I'll look more later. I'm impressed, I would not have had the fortitude for that. :-)

[Oleksandr Manzyuk]

Scott Morrison said:

wisker should be whisker

:face_palm:

[Oleksandr Manzyuk]

Scott Morrison said:

I'll look more later. I'm impressed, I would not have had the fortitude for that. :-)

Thanks! It wasn't too bad. I think map_π_epi stating that the image of coequalizer.π under a colimit-preserving functor is an epi really helped to structure the proofs. When we need to prove equality of two morphisms from a coequalizer, we can use ext, which precomposes both morphisms with coequalizer.π, and map_π_epi together with cancel_epi allows us to apply the same idea when the source of the morphisms is a coequalizer tensored with other objects. Once we have compositions starting with coequalizer.π, proofs almost write themselves. Initially I relied on simp a lot, but it was slow, so following your advice I replaced it with simp only, which taught me quite a bit of the relevant API, and at some point I felt more comfortable using the API and performing rewrites directly, which also helped with the perf.

[Oleksandr Manzyuk]

#14402

[Scott Morrison]

I'll be away from the #queue for a few days, but hopefully others can look at this too. You've got ahead of the old world, so we can't even compare this to the bicategory of vanilla algebras/bimodules/intertwiners when C = Type. :-)

[Scott Morrison]

Not at all for now, but later I'd love to see how this construction works out in special cases. When you restrict to (symmetric??) Frobenius algebras and the category is idempotent complete there are nicer formulas for the tensor product of bimodules (the image of the "ladder" idempotent), and I'm hopeful that we can prove an equivalence.

[Scott Morrison]

(In some settings, e.g. in a fusion category, restricting to Frobenius algebras is not much of a restriction.)

[Yuma Mizuno]

It's so nice! I'm happy to see that the bicategory structure on the algebras and bimodules is defined in this generality.

[Yuma Mizuno]

I would like to make a comment that are not intended to interfere with the current PR.

The proofs in the PR #14402 contain several rewriting of the form (𝟙 _ ⊗ f) ≫ (g ⊗ 𝟙 _) = (g ⊗ 𝟙 _) ≫ (𝟙 _ ⊗ f). In fact, these are equal to tensor_hom, g ⊗ f.

In my experience, tensor_hom seems to be incompatible with simp. I think this can be improved by introducing whisker_right and whisker_left as the primitive objects in the definition of the monoidal category rather than tensor_hom, as I did in the definition of bicategory, which uses whisker_right and whisker_left instead of the horizontal compositions. I would like to do this kind of a refactoring if I can find the time.

[Oleksandr Manzyuk]

@Scott Morrison @Yuma Mizuno This is a gentle reminder that I would appreciate your review of #14402.

[Oleksandr Manzyuk]

Hi everyone (particularly @Scott Morrison and @Yuma Mizuno ), #14402 was last reviewed over 2 weeks ago, and since then I've made quite a few changes and would appreciate another pass over the PR.

[Yuma Mizuno]

@Oleksandr Manzyuk Sorry for delay. I left some comments.

[Yuma Mizuno]

By the way, you can add the awaiting-review label, then maintainers can find your PR.

[Oleksandr Manzyuk]

I think I've addressed all comments from @Yuma Mizuno on #14402. Are there any other change you'd like me to make?

[Yuma Mizuno]

Now #14402 looks good to me.

[Yuma Mizuno]

I put approved on github just to make sure.