Monoids in a braided monoidal category

Stream: general

[Oleksandr Manzyuk]

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]

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]

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

[Patrick Massot]

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.

$A_\infty$-categories are still everywhere in symplectic topology.

[Scott Morrison]

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

[Scott Morrison]

@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]

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

[Scott Morrison]

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

[Adam Topaz]

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

[Oleksandr Manzyuk]

Thanks for the nice feedback! Getting back to $A_\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]

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]

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]

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

[Oleksandr Manzyuk]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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]

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

[Scott Morrison]

src#category_theory.monoidal_closed