monoid object

Stream: Is there code for X?

[Jack J Garzella]

Do we have a way to express a monoid object in a (monoidal) category?

Similarly, do we have a concise way to express commutative diagrams as one would want to define a monoid/group/coalgebra/etc object?

[Johan Commelin]

Q1: Maybe? I think not yet...
Q2: Nope. And if you figure out how to solve this, that would be awesome. It seems quite nontrivial to me.

[Bhavik Mehta]

1. Yeah - as Johan says, it's not yet in mathlib but it's entirely doable

[Markus Himmel]

1. was actually an exercise at LFTCM: https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/thursday/afternoon/category_theory/exercise7.lean

[Jalex Stark]

Scott should give a lecture course, and then the next 2000 lines of the category theory library can be students PRing exercises

[Kevin Buzzard]

While we're giving category theory some love, I should tell people about the experience Bhavik, Chris and me had at Xena on the Discord last night (we have regular Thursday evening meetings there btw). I'd just refactored abelianization.lean, which claims in its docstring to construct the adjoint functor to the forgetful functor from Ab to Gp but of course it's just an API for abelianisation and doesn't mention categories at all. I saw that Scott had made adjoint functors so suggested we should prove that they really were adjoint. Then it turned out Ab is + and Gp is * (as it should be!) so there were going to be additives and multiplicatives everywhere (and the API for this stuff is not even complete, for example there's no construction of additive G ->+ A from G ->* multiplicative A unless you abuse the type alias additive (multiplicative A) = A, something which might cause problems later? Anyway when Chris saw this mess his first reaction was "there are layers upon layers here, proving adjointness might not be easy". But I'd been refactoring subgroups and had been dealing with additive/multiplicative stuff so knew some tricks, and the functors were defined without too much problem. And when it came to adjointness I just started ploughing through the fields but then Bhavik said that he knew a couple of constructors which would make our life easier. Chris was really surprised when I told him that the condition for functors to be adjoint was that there was some bijection between hom sets and it had to be natural in a sense I couldn't make precise. We looked at the constructor and it involved whiskering and I said I didn't know what that was either (fortunately Bhavik did). But I freely confessed to using adjoint functors in my work. Bhavik told us the constructor which just needed the bijection, I formalised the data and then with baited breath we tried tidy and it did every single goal. Chris was delighted, Bhavik said tidy was OP :-)

[Kevin Buzzard]

One important thing we learnt @Scott Morrison was that I would have wasted a bunch of time if Bhavik hadn't told me about the constructor for adjoints which just asks for the equiv, and so maybe these important constructors should be mentioned in the docstring for adjoint?

[Johan Commelin]

The code was written before we start doccing definitions

[Johan Commelin]

I'm a big fan of mentioning alternative constructors in docstrings

[Jalex Stark]

my ~only strategy right now for discovering alternative constructors is to ask suggest; i'd love to sometimes learn about them from docstrings :)

[Bryan Gin-ge Chen]

The docs still need a lot of love... contributions very, very welcome!

[Jalex Stark]

maybe we can organize a docs hackathon day

[Matt Earnshaw]

I did this "exercise" for commutative comonoids recently, without realising this it had been posed. It's a bit rough so will try to mould it into PR shape when I can (with the additional theorems).

Anyway, it raised a question for me, even if it is somewhat idle. In principle there is a distinction between the abstract universal "monoid object" and concrete universal "monoid object in a category", the latter being a functor from a sketch. For now it is probably needless abstraction but I am curious if anyone has thought about how switching between parametric typeclasses and functors in this way might be carried out

[Patrick Massot]

Bryan Gin-ge Chen said:

The docs still need a lot of love... contributions very, very welcome!

Reminder for everyone (not targetting any specific part of mathlib): when the days of the great switch to Lean4 will come, everything which is undocumented will much harder to port. Some stuff may disappear completely from mathlib if nobody understands it.

[Scott Morrison]

The other thing to say about Kevin + Bhavik + Chris's experience is that pair/group proving is fun. :-)

[Scott Morrison]

@Matt Earnshaw, I haven't thought about that distinction yet.

[Scott Morrison]

I think exploring monoid objects in monoidal categories further would be valuable. Can we obtain all the basic results on (C)DGAs by observing they are (commutative) monoid objects in chain complexes?

[Bhavik Mehta]

By the way I've got some messy code which does internal category objects, and I made the functors internal_category (Type u) ⥤ Cat and Cat.{u} ⥤ internal_category (Type u) (where internal_category A is the category of categories internal to A), I don't know that this is useful for anyone but I have it at least