Zulip Chat Archive

Stream: maths

Topic: has_* limit classes


view this post on Zulip Reid Barton (Sep 06 2019 at 15:32):

We now have a whole slew of limit-related classes beyond has_limit, has_limits_of_shape and has_limits, namely
has_terminal, has_binary_products, has_finite_products, has_products, has_equalizers, has_pullbacks, has_finite_limits.
What is the plan for making instances of all these classes?

view this post on Zulip Reid Barton (Sep 06 2019 at 15:33):

For example, here is a concrete question. In Top the binary product is given by the usual product of spaces, whose underlying type is the product of the underlying types. Should that be how has_binary_products Top is defined?

view this post on Zulip Reid Barton (Sep 06 2019 at 15:35):

Or should it agree with the product which comes from has_limits, which will be of the form a subtype of a Pi type, and will definitely not be equal (at least not provably equal) to X × Y?

view this post on Zulip Reid Barton (Sep 06 2019 at 17:13):

I tried looking at other category theory libraries, namely the Lean 2 HoTT library and UniMath, although they may have different concerns than we do.
In the Lean 2 HoTT library, has_binary_products is simply defined to be (reducibly) has_limits_of_shape for a particular shape category (just two objects and no nonidentity morphisms). That is one extreme option. However, using a class that is reducible doesn't seem to work very well in Lean 3 (based on comments in that file, it might not have worked very well in Lean 2 either).
UniMath has two (or sometimes even more) definitions of each of these special types of limits, one defined generically as a limit and one which is direct, and prove their equivalence. They're not afraid to write a lot of stuff! On the other hand they don't use type classes at all, so they don't have the question of which of these relationships to make into instances.

view this post on Zulip Reid Barton (Sep 06 2019 at 17:14):

Trying to define an instance has_binary_products Top by hand, I'm quickly led to the conclusion that one ought to define a specialized is_binary_product (like UniMath does) and then prove its equivalence to the general limit concept.

view this post on Zulip Reid Barton (Sep 06 2019 at 18:48):

Actually it's surprisingly awkward even to prove that anything has binary products

view this post on Zulip Reid Barton (Sep 06 2019 at 18:49):

That is, other than by some general limit construction. If you really want to make use of the fact that you're defining a binary product.

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:37):

So I guess two questions are:

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:38):

1) How often can you construct binary products but not general limits? What are some good examples?

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:38):

2) How often to you want to know that your "categorical" binary product is actually the "native" binary product, rather than just something satisfying the categorical binary product API?

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:39):

If either of those is "often", then yes, we need a specialized is_binary_product and all its relatives.

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:39):

This is not particularly hard or onerous to do, and I'm not too worried about the API surface area growing too large just because of this.

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:40):

I do think it will have a slightly dangerous effect --- we'll see people defining instances of has_binary_product not because they actually needed a tight connection with a "native" binary product, but just because they didn't think hard enough about constructing more general shapes.

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:41):

(I think, Reid, you saw me doing exactly this for both Type and Top during my initial experimentation. :-)

view this post on Zulip Reid Barton (Sep 07 2019 at 12:16):

1) How often can you construct binary products but not general limits? What are some good examples?

I found it difficult to come up with one which is really compelling and feasible to add to mathlib, but here are some examples:
Schemes (only finite limits, and it seems you have to build them out of pullbacks). Manifolds (but they don't care about category theory). The category of sets and relations is a simple one, it has products (which are disjoint unions) but not equalizers. Suitable subcategories of nice categories, e.g., Kan complexes. Lawvere theories (e.g., the opposite of the category of free groups) have finite products and generally not other limits.

view this post on Zulip Reid Barton (Sep 07 2019 at 12:21):

2) How often to you want to know that your "categorical" binary product is actually the "native" binary product, rather than just something satisfying the categorical binary product API?

This I think is a lot more common. For example, in lean-homotopy-theory I need the fact that the functor X×X \times - on topological spaces preserves pushouts when XX is locally compact. (In particular, when X=I=[0,1]X = I = [0, 1]; that lets me define a homotopy between maps on a pushout by gluing homotopies together.) The proof is that X×X \times - is left adjoint to C(X,)C(X, -) with the compact-open topology. The "math part" of that is here and it uses the fact that we're really talking about the product space, using is_open_prod and so on.

view this post on Zulip Reid Barton (Sep 07 2019 at 12:25):

Now technically for my purposes it doesn't matter that the cylinder functor I×I \times - is actually a categorical product, so I don't bother to formalize products. But if we're going to have notation for the categorical product on Top, it seems rather convenient for it to be the actual product defined using prod.

view this post on Zulip Reid Barton (Sep 07 2019 at 12:26):

For example, suppose we define a cartesian closed category and then we want to prove Type is one

view this post on Zulip Reid Barton (Sep 07 2019 at 12:29):

Presumably the first thing you would have to do is show that the crazy subtype-of-a-Pi-type definition of the product is isomorphic to prod

view this post on Zulip Reid Barton (Sep 07 2019 at 13:15):

Which is not specific to proving cartesian closedness, so you'd want to record that fact somewhere


Last updated: May 12 2021 at 08:14 UTC