[Merged by Bors] - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category #14402

manzyuk · 2022-05-26T21:54:49Z

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.

… bimodules internal to some monoidal category (#14402) We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) 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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-07-25T05:09:53Z

Build failed (retrying...):

Build mathlib

… bimodules internal to some monoidal category (#14402) We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) 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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-07-25T06:16:58Z

Build failed (retrying...):

Build mathlib

… bimodules internal to some monoidal category (#14402) We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) 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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-07-25T06:23:25Z

Build failed:

Build mathlib

manzyuk · 2022-08-13T16:01:49Z

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).

semorrison · 2022-10-16T08:00:50Z

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.

semorrison · 2022-10-16T08:01:15Z

bors d+

bors · 2022-10-16T08:01:16Z

✌️ 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.

manzyuk · 2022-10-16T08:16:34Z

Thanks you very much, Scott!

bors r+

bors · 2022-10-16T08:16:36Z

👎 Rejected by label

semorrison · 2022-10-16T08:39:15Z

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

manzyuk · 2022-10-16T11:47:18Z

bors r+

… bimodules internal to some monoidal category (#14402) We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) 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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-10-16T13:09:36Z

Pull request successfully merged into master.

Build succeeded:

semorrison and others added 30 commits April 13, 2022 21:27

this looks like a lot of work

be89dec

Fill in two sorries in the definition of act_left

03c0e77

Fill in two sorries in the definition of act_right

e65ebaf

Add sorries for the missing fields

3cbf15f

Simplify the isomorphism used in act_left

99ff1d8

Fill in a proof of one_act_left'

a5f9cf1

Prove act_right_one'

89670b7

Prove left_assoc'

b09d02a

Simplify

031eede

Prove right_assoc'

3bff40a

Prove middle_assoc'

21656c9

Cleanup

9646bb8

Define tensor product of two bimodule morphisms

5e887ab

Tensor product preserves identities and composition

280e654

Merge branch 'master' into semorrison/Bimod

3a77073

Replace simp with simp only

720ed9a

Replace simp only with explicit rewrites

a9369a8

Simplify the proofs with auxiliary lemmas

d29c7d2

Simplify tensor_hom

a250de9

Start defining the bicategory of monoids. Define left_unitor.

191a152

Define right_unitor

196d345

Define hom field of associator

0bcbe03

Extract fields into top-level bindings

29f0d0e

Finish the definition of associator_Bimod

08baa43

Simplify the definition of the left unitor

449bb42

Simplify the definition of the right unitor

cf3adf5

Simplify with helper lemmas

c7dcf14

More simplifications

0744067

Proove the pentagon axiom

52259af

Prove the triangle axiom

18cf0d8

leanprover-community-bot-assistant removed the awaiting-review The author would like community review of the PR label Jul 25, 2022

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Jul 28, 2022

Merge branch 'master' into semorrison/Bimod

6ce3c3f

Merge remote-tracking branch 'origin/master' into semorrison/Bimod

99310f7

semorrison requested a review from a team as a code owner October 16, 2022 07:26

fix universe issue

ebdc812

semorrison added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 16, 2022

github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Oct 16, 2022

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 16, 2022

bors bot changed the title ~~feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category~~ [Merged by Bors] - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category Oct 16, 2022

bors bot closed this Oct 16, 2022

bors bot deleted the semorrison/Bimod branch October 16, 2022 13:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category #14402

[Merged by Bors] - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category #14402

manzyuk commented May 26, 2022

bors bot commented Jul 25, 2022

bors bot commented Jul 25, 2022

bors bot commented Jul 25, 2022

manzyuk commented Aug 13, 2022

semorrison commented Oct 16, 2022

semorrison commented Oct 16, 2022

bors bot commented Oct 16, 2022

manzyuk commented Oct 16, 2022

bors bot commented Oct 16, 2022

semorrison commented Oct 16, 2022

manzyuk commented Oct 16, 2022

bors bot commented Oct 16, 2022

[Merged by Bors] - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category #14402

[Merged by Bors] - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category #14402

Conversation

manzyuk commented May 26, 2022

bors bot commented Jul 25, 2022

bors bot commented Jul 25, 2022

bors bot commented Jul 25, 2022

manzyuk commented Aug 13, 2022

semorrison commented Oct 16, 2022

semorrison commented Oct 16, 2022

bors bot commented Oct 16, 2022

manzyuk commented Oct 16, 2022

bors bot commented Oct 16, 2022

semorrison commented Oct 16, 2022

manzyuk commented Oct 16, 2022

bors bot commented Oct 16, 2022