[Merged by Bors] - feat(category_theory/limits/shapes/multiequalizer): Multi(co)equalizers

[adamtopaz]

This PR adds another special shape to the limits library, which directly generalizes shapes for many other special limits (like pullbacks, equalizers, etc.). A multiequalizer can be thought of an an equalizer of two maps between two products. This will be used later on in the context of sheafification.

I don't know if there is a standard name for the gadgets this PR introduces. I would be happy to change the names if needed.

---

[jcommelin]

These names are not very mnemonic. Also, should α and β be bundled?

[adamtopaz]

I think I'll switch them to L resp. R (for left resp. right). Is there a particular reason you think they should not be bundled?

In the (hopefully near?) future where we have pseudofunctors, I can imagine wanting to talk about the category of multicospan_indexs and to a morphism in this category, obtain a functor between walking_multicospans which fit together into a pseudofunctor. This might be an argument for bundling.

[adamtopaz]

I renamed \alpha -> L and \beta -> R, also f -> fst_to/fst_from and s -> snd_to/snd_from.

[erdOne]

Could there / should there be isomorphisms from the multiequalizer to the equalizer of the products, and simp lemmas showing that the projections on both sides are the same?

[adamtopaz]

Could there / should there be isomorphisms from the multiequalizer to the equalizer of the products, and simp lemmas showing that the projections on both sides are the same?

Good idea. I'll try to add that soon.

[adamtopaz]

Could there / should there be isomorphisms from the multiequalizer to the equalizer of the products, and simp lemmas showing that the projections on both sides are the same?

Good idea. I'll try to add that soon.

On second thought, I think it would be too much additional work to do this properly, so I think it would be better to leave this for a future PR. I added a comment under the Projects section in the module docstring regarding this.

[erdOne]

Did you run into any obstacle when trying to do so?

If not, and that it is merely time-consuming, I could try do it since I would probably need these results when gluing.

An alternative would be to develop API about multicoequalizers in Top, but I doubt that this would be easier.

[adamtopaz]

Did you run into any obstacle when trying to do so?

If not, and that it is merely time-consuming, I could try do it since I would probably need these results when gluing.

An alternative would be to develop API about multicoequalizers in Top, but I doubt that this would be easier.

There is no real difficulty, what to do it properly would require the following:

1. Given a multifork, construct a fork for the two maps between the products, and vice versa.
2. Prove that a multifork is a limit if and only if the associated fork is a limit (and vice versa).
3. Construct the isomorphism between the multiequalizer and equalizer.
4. And, of course, dualize everything...

So the main obstacle is time, and that all of this would probably be too much for a single PR :)

[jcommelin]

Thanks 🎉

bors merge

[adamtopaz]

bors r-

[bors]

Canceled.

[jcommelin]

bors d+

[bors]

✌️ adamtopaz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[adamtopaz]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests