Zulip Chat Archive

Stream: maths

Topic: homeomorphisms


view this post on Zulip Reid Barton (Jun 01 2018 at 18:50):

@Patrick Massot, did you have a definition of homeomorphisms somewhere?

view this post on Zulip Patrick Massot (Jun 01 2018 at 18:51):

https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/homeos.lean

view this post on Zulip Reid Barton (Jun 01 2018 at 19:03):

thanks! I like this extends equiv idea

view this post on Zulip Patrick Massot (Jun 01 2018 at 20:11):

This was Mario's idea. At that time I had no idea equiv existed

view this post on Zulip Kenny Lau (Jun 01 2018 at 20:12):

just do it in a category man

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 20:46):

won't there be universe issues?

view this post on Zulip Kenny Lau (Jun 01 2018 at 20:46):

just build a category theory without universe issue, man

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 20:49):

I think Russell had something to say about that

view this post on Zulip Kenny Lau (Jun 01 2018 at 20:50):

the category itself as an object has universe issues

view this post on Zulip Kenny Lau (Jun 01 2018 at 20:50):

if you use the things within, you should be fine

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 20:50):

I never really understood the issues that Scott had with universes but my impression is that things are harder than you might think

view this post on Zulip Kenny Lau (Jun 01 2018 at 20:50):

(there's a different category for each universe)

view this post on Zulip Kenny Lau (Jun 01 2018 at 20:50):

(but it doesn't matter)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 21:01):

my understanding is that sometimes it does matter

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 21:01):

because maybe you end up with the right object but in the wrong universe

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:17):

The problem with universes (which is the sole reason I didn't have a PR ready months ago) is that there are genuinely two different sorts of categories one needs in mathematics: "small categories", in which objects and morphisms live in the same fixed universe, and "large categories", in which objects get to live in one higher universe than the morphisms.

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:18):

For a very long time in my pre-Lean mathematical career, I thought this wasn't such a big deal, but I've learnt better. :-)

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:21):

(Briefly: we need large categories because all the basic algebra examples like Types, Groups, PL, etc are large. We need small categories because if you try thinking about any of the basic machinery in category theory, particularly taking limits, when you index over objects in a large category you find yourself having to move up the universe hierarchy over and over again, while when you index over objects in a small category you can stay at one level. Happily, one can get away with doing most of mathematics only having to index over a small category --- but not quite all, so eventually you need to admit that the universe parameter can vary across a development.)

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:22):

So, how to implement this? We don't want to have parallel developments of small and large categories, because then we'd have at least 3 different types of functors (small to small, small to large, large to large -- large to small is just silly, of course :-), and lifts between these, and then more mess at the level of transformations, and it will all end badly.

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:23):

The two options I considered were:

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:23):

1) "categories" by default have objects in Type (u+1) and morphisms in Type u, and a small category is a category along with the additional evidence that the objects are equivalent in something in Type u after all.

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:24):

2) We define "categories" to have two universe parameters, so objects live in Type u and morphisms in Type v, and define "small_category" and "large_category" as subclasses (with u=v and u=v+1 respectively).

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:25):

In the end, it seems that 1) just doesn't work; I found that I was having to implement multiple sorts of functors and natural transformations anyway.

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:27):

2) mostly works. You develop as much as you need at the level of "independent universe" categories, but then when it makes sense restrict to either small_category or large_category. Working entirely with independent universe categories becomes problematic, because Lean usually can't infer the morphism universe level. Mostly you can get around this just by specifying that level explicitly, but it also starts to break typeclass inference and so eventually becomes a serious problem.


Last updated: May 19 2021 at 02:10 UTC