design of products/equalizers/kernels/pullbacks

Stream: general

[Scott Morrison]

I'm looking for some advice/opinions on a design issue for category theory. In particular this is about categorical products (or equalizers, or kernels, or pullbacks). I think there ought to be at least two descriptions of these, along with appropriate lemmas to move back on forth. One description will be as a special case of limits, and the other description will be more "concrete".

[Scott Morrison]

Writing them as special cases of limits is of course useful so we can save effort on proving things like "products are unique, up to unique isomorphism" and "equalizers are unique, up to unique isomorphism" without duplication.

[Scott Morrison]

But I'm pretty sure it will be too cumbersome to actually use them when presented like this.

[Scott Morrison]

My question is just how concrete to make the concrete version. (One possible answer here is to have several versions.)

[Scott Morrison]

My first inclination is to make them extremely explicit: for example for a product it would be a structure containing separate fields for the data:

1. an object P of the category
2. maps \pi_i to each factor X_i
3. if you have an object Q equipped with maps g_i to each of the X_i, then you get a map f : Q \to P
4. moreover, this means that g_i factors as f then \pi_i
5. finally, if you have two maps from Q to P making the g_i's factor in this way, then the two maps are equal.

[Scott Morrison]

Slightly less explicit would be

1. an object P of the category
2. maps \pi_i to each factor X_i
3. given Q and maps g_i : Q \to X_i, the fact that the set of maps Q \to P giving those factorisations is a singleton set

[Scott Morrison]

Maybe there's not much difference between the two. In any case, if someone cares let me know, as this is easy to change now. :-)

[Scott Morrison]

The advantage of the first approach is that if you just want the map Q \to P, you can ask for it directly without having to unpack a witness that a certain type is a singleton to actually get the element.

[Scott Morrison]

The disadvantage is that it's a bit grosser to write everything out.

[Scott Morrison]

I'm curious to know which choice feels more usable to people.

[Johan Commelin]

Hi Scott! Those are the difficult questions that we will have to tackle!

[Johan Commelin]

Did you see Reid's approach in his homotopy lib?

[Johan Commelin]

He basically provides both. Your (1,2,3) would be a wrapper around (1,2,3,4,5)

[Scott Morrison]

Great, thanks for the pointer! (And my apologies to @Reid Barton, for not having yet read his work, although he told me about it a few days ago.)

[Scott Morrison]

Seeing that Reid went for two versions, I'm further inclined to go for lots of versions: the gory one, the "singleton" based one, and the "this is just a limit" one.

[Patrick Massot]

I'm almost sure we need several versions, with "constructors" to get the most explicit ones out of implicit information.

[Scott Morrison]

Yes. Having just looked at @Reid Barton's design for this, I like it. (Well... I might try rewriting it myself before I really like it, but the overall approach looks right.)

[Scott Morrison]

Although I think/hope all his lemmas about various types of colimits interacting can be simplified! I'd hope you can just prove a Fubini theorem for colimits, and then specialise to get many of the lemmas there. Haven't thought about this very hard, however!

[Patrick Massot]

What would be really really useful is a convenient way to be able to use all this as an external tool. For instance, we have uniform spaces in mathlib, and all lemmas required to make a category of those, but we don't have that category. Same for complete Hausdorff uniform spaces. Then we have https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/completion.lean#L8-L15. And I'd like https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/completion.lean#L20-L24 to be done by invoking a function defined in category_theory with minimal effort, without necessarily being tied to use the content of category_theory everywhere else.

[Patrick Massot]

same for the uniqueness up to unique iso of the completion