mathlib

mathlib copied to clipboard

We generalise the well-known construction of the 2-category of rings, bimodules, and intertwiners. Given a monoidal category C that has coequalizers and in which left and right tensor products preserve colimits, we define a bicategory whose

• objects are monoids in C;
• 1-morphisms are bimodules;
• 2-morphisms are bimodule homomorphisms.

The composition of 1-morphisms is given by the tensor product of bimodules over the middle monoid.

---

@yuma-mizuno I believe I have satisfied the linter. Will try to golf some of the definitions later.

Ping.

There are many dunfold in the proofs. Is it possible to reduce them? I guess one might add simp attributes or use abbreviation instead of def.

I've had some mixed experiences with abbreviations and prefer defs and predictability of dunfold, but I can try. I'm trying not to rely on simplification in this proof but rather on explicit rewrites, so not sure if simp attributes would help?

I've had some mixed experiences with abbreviations and prefer defs and predictability of dunfold, but I can try. I'm trying not to rely on simplification in this proof but rather on explicit rewrites, so not sure if simp attributes would help?

I see. Let me just add one more comment: dunfold foo bar, dsimp can be replaced with dsimp [foo, bar], which makes the proofs a little cleaner.

Build failed (retrying...):

• Build mathlib

Build failed (retrying...):

• Build mathlib

Build failed:

• Build mathlib

I didn't have time to look into this in detail (and patience, as VS Code takes ages to check the file) but apparently there has been a recent refactoring of preserves_colimits class, so that Lean is no longer able to derive an instance of preserves_colimit (parallel_pair f g) (tensor_left Z) from ∀ X : C, preserves_colimits (tensor_left X).

I didn't have time to look into this in detail (and patience, as VS Code takes ages to check the file) but apparently there has been a recent refactoring of preserves_colimits class, so that Lean is no longer able to derive an instance of preserves_colimit (parallel_pair f g) (tensor_left Z) from ∀ X : C, preserves_colimits (tensor_left X).

This was a universe issue, which I've just fixed, and will bump this back onto the queue.

bors d+

:v: manzyuk can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Thanks you very much, Scott!

bors r+

:-1: Rejected by label

@manzyuk, it needs to finish CI first (so that the awaiting-CI label gets removed) before you can ask bors to merge.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests