mathlib
mathlib copied to clipboard
leanprover-community
feat(category_theory/category/Pointed): `Pointed` is a monoidal category
Provide the monoidal_category and symmetric_category instances for Pointed.
This is mostly an exercise for me to see whether I understand monoidal categories. Please suggest missing API. I tried to do the same for PartialFun over at branch PartialFun_monoidal but obviously timed out. ~~Can I somehow use that PartialFun ≌ Pointed to transfer the monoidal structure?~~ No, because that doesn't give the right monoidal structure.
We discussed this offline, but for the sake of a record, the equivalence PartialFun ≌ Pointed isn't useful to transfer the monoidal structure, as the equivalence doesn't give you the nice monoidal structure unfortunately (in other words the correct monoidal structure on both sides means that the equivalence isn't a monoidal one)
Seems to have been a spurious CI failure, and I couldn't re-run failed jobs, so I've merge master to restart CI.
:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.
![bors[bot] avatar](https://avatars.githubusercontent.com/in/1847?v=4 "Published by a pub.dev verified publisher"){kind=small}
Let me just say that since Bhavik's last review we figured out that this isn't the usual literature tensor operation on Pointed. Rather, it should be the "smash sum", the wedge from algebraic topology. I have it on a branch, so I can update this PR to use this instead, but then what should I do with the material in this PR?
Options:
- Just drop this PR, if it isn't needed for something else you're doing, and this can be revisited in Mathlib when needed.
- Merge as is, adding a note that this is the Cartesian monoidal structure, rather than the smash monoidal structure.
I'm inclined to drop: this construction would probably be better done as defining PointedObject for an arbitrary category with a terminal object, in any case.