Zulip Chat Archive

Stream: general

Topic: Monoids in a braided monoidal category


Oleksandr Manzyuk (Mar 29 2022 at 10:26):

Hello, I'm new to Lean and this chat. I've started picking up Lean a few months ago, and it's been a lot of fun. I've gone through several tutorials (including LFTCM2020 and @Kevin Buzzard's formalising mathematics course), and I think I'm now sufficiently competent to work on "real stuff", so most recently I've picked up and been working on one of the projects mentioned at the bottom of category_theory/monoidal/Mon_.lean file, namely the construction of monoidal structure on the category of monoids in a braided monoidal category. I'm not done yet but I thought I'd start contributing some self-contained pieces of work. "How to contribute to mathlib" page suggests that I introduce myself here first and ask for write access to non-master branches of the mathlib repository. My GitHub username is "manzyuk".

The original plan was to show that the category of lax monoidal functors admits a monoidal structure if the target monoidal category is braided, and then translate this structure to the category of monoids along the equivalence between the latter category and the category of lax monoidal functors from the unit category into the given braided monoidal category. I started with some straightforward stuff like monoidal category structure on C × D and lax monoidal functor structure on the product of two lax monoidal functors, and then proved that the tensor functor from C × C to C is lax monoidal if C is braided, which I thought was the key lemma (and one that was hardest to prove). However, today I realised that I also needed the lemma that the associator is a monoidal isomorphism of triple tensor product functors, which will require a similar lemma.

In the end, I decided to work directly with the category of monoids rather than the equivalent category of lax monoidal functors from the unit category, but use the tensorator of the tensor product functor and the lemmas I proved for it directly to give the construction of tensor product of monoids and structural isomorphisms and provide necessary proofs.

Anyway, it's probably easier to share the code and move the discussion to PRs. I'm looking forward to your further instructions.

(A very quick bio: I did a PhD in maths, for which I studied so called A-infinity categories, which seem to have gone out of fashion now, but were a pretty hot topic 15 years ago. I switched careers and started working as a software developer full time about 10 years ago, and have done very little mathematics, mostly recreational stuff, since then. This is changing now that I've discovered Lean.)

Anne Baanen (Mar 29 2022 at 10:39):

Oleksandr Manzyuk said:

I introduce myself here first and ask for write access to non-master branches of the mathlib repository. My GitHub username is "manzyuk".

Invitation sent!

Oleksandr Manzyuk (Mar 29 2022 at 10:45):

Accepted, thank you! I'll create some PRs later today.

Patrick Massot (Mar 29 2022 at 11:01):

Oleksandr Manzyuk said:

A very quick bio: I did a PhD in maths, for which I studied so called A-infinity categories, which seem to have gone out of fashion now, but were a pretty hot topic 15 years ago.

AA_\infty-categories are still everywhere in symplectic topology.

Scott Morrison (Mar 30 2022 at 00:39):

I also like A_\infty categories, for their uses in link homology, and higher category theory. Let's have some in mathlib. :-)

Scott Morrison (Mar 30 2022 at 00:40):

@Oleksandr Manzyuk, you may be interested in checking out my (failed) attempt at the monoidal structure on monoids in a braided category, at branch#Mon_braided. (diff from master at https://github.com/leanprover-community/mathlib/compare/Mon_braided?expand=1)

Scott Morrison (Mar 30 2022 at 00:40):

I think this is a place we really need tactic help with associators. There has been some recent discussion on this.

Scott Morrison (Mar 30 2022 at 00:41):

e.g. at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/associator-free.20proof.20in.20bicategories

Adam Topaz (Mar 30 2022 at 00:42):

Kadeishvili's theorem (for A_infty algebras) would be an excellent formalization goal!

Oleksandr Manzyuk (Mar 30 2022 at 10:27):

Thanks for the nice feedback! Getting back to AA_\infty-categories will require time because I haven't touched them since 2008-2009. Somehow other things, like multicategories, have sunk in deeper. For this reason, I've been thinking of a more realistic (yet still ambitious) goal to try and formalise my paper "Closed categories vs. closed multicategories". I think closed (not-necessarily monoidal) categories haven't been formalised in mathlib yet, and I haven't seen multicategories either?

Oleksandr Manzyuk (Mar 30 2022 at 10:36):

Scott Morrison said:

I think this is a place we really need tactic help with associators. There has been some recent discussion on this.

Interesting! Yes, my proof of associativity of the strength for the tensor product functor relies in several places on rewriting a composition of morphisms built out of associators, unitors and identities with another such composition. Filling in the proofs manually would be extremely tedious (and would require some creativity / ingenuity), but I've found a cheap (if somewhat boilerplate-y) way to apply the coherence theorem and derive the necessary equations pretty mindlessly. I've left a comment on PR.

IMG_5196.HEIC

Yuma Mizuno (Mar 30 2022 at 15:12):

Oleksandr Manzyuk said:

Filling in the proofs manually would be extremely tedious (and would require some creativity / ingenuity), but I've found a cheap (if somewhat boilerplate-y) way to apply the coherence theorem and derive the necessary equations pretty mindlessly. I've left a comment on PR.

Recently I wrote a coherence tactic that you just mentioned at this comment. See mathlib#12697. I feel that the scope of coherence tactic is still limited as I stated at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312697.20coherence.20tactic.20for.20monoidal.20categories, but it is already useful enough to remove boilerplate.

Scott Morrison (Mar 30 2022 at 20:44):

@Oleksandr Manzyuk, search for closed_category. We have the basics.

Oleksandr Manzyuk (Mar 30 2022 at 21:41):

Yuma Mizuno said:

Recently I wrote a coherence tactic that you just mentioned at this comment. See mathlib#12697. I feel that the scope of coherence tactic is still limited as I stated at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312697.20coherence.20tactic.20for.20monoidal.20categories, but it is already useful enough to remove boilerplate.

This is awesome! I'm looking forward to being able to use this tactic.

Oleksandr Manzyuk (Apr 01 2022 at 23:28):

A small status update: I'm done with the proof and have sliced it up as a stack of 4 PRs: #13033, #13034, #13121, #13122, with the last PR containing the main result. I'm looking forward to your reviews and suggestions for improvements!

Scott Morrison (Apr 02 2022 at 03:15):

I've started a new thread over at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313122.3A.20monoids.20in.20a.20braided.20category now that there are PRs on this.

Scott Morrison (Apr 02 2022 at 03:21):

I implemented a coherence tactic, and pushed this in #13034 for others to look at. @Oleksandr Manzyuk and @Yuma Mizuno, could we compare the approach there and Yuma's approach described at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312697.20coherence.20tactic.20for.20monoidal.20categories? There's not much difference between them: it's either some typeclass boilerplate or some meta boilerplate. We'll merge one soon!

Scott Morrison (Apr 02 2022 at 06:25):

I've extracted out my coherence tactic, and put it up at #13125. It is an alternative to @Yuma Mizuno's #12697.

Scott Morrison (Apr 02 2022 at 06:25):

It doesn't contain a coherence tactic for bicategories, however.

Scott Morrison (Apr 02 2022 at 06:26):

It additionally provides a "composition up to unitors+associators" operation, so you can write

example {U V W X Y : C} (f : U  V  (W  X)) (g : (V  W)  X  Y) : U  Y := f ⊗≫ g

Scott Morrison (Apr 02 2022 at 06:26):

Finally, I've left a comment about a better coherence tactic:

To prove an equality f = g in a monoidal category,
parse each of f and g as the composition of some lift of morphisms.
Identify the morphisms for which we can not construct a lift_hom.
Make sure the lists of such morphisms in f and g are identical; fail if not.
Now split the lists at these points,
and for each corresponding pair of lists of morphisms for which we have a lift_hom
(one list from f, one list from g),
try to prove these are equal using the coherence tactic above.

We should try and implement this soon!

Scott Morrison (Apr 02 2022 at 07:57):

Oooh, that may have been easier than I feared:

example (f) : (λ_ (𝟙_ C)).hom  f  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom  f  (ρ_ (𝟙_ C)).hom :=
by coherence2

Oleksandr Manzyuk (Apr 12 2022 at 10:42):

Scott Morrison said:

Oleksandr Manzyuk, search for closed_category. We have the basics.

I've tried grepping closed_category but it turned up nothing?

Scott Morrison (Apr 12 2022 at 11:27):

I'm sorry, it's src/category_theory/closed/monoidal.lean

Scott Morrison (Apr 12 2022 at 11:27):

src#category_theory.monoidal_closed


Last updated: Dec 20 2023 at 11:08 UTC