homeomorphisms

Stream: maths

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

thanks! I like this extends equiv idea

[Patrick Massot]

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

[Kenny Lau]

just do it in a category man

[Kevin Buzzard]

won't there be universe issues?

[Kenny Lau]

just build a category theory without universe issue, man

[Kevin Buzzard]

I think Russell had something to say about that

[Kenny Lau]

the category itself as an object has universe issues

[Kenny Lau]

if you use the things within, you should be fine

[Kevin Buzzard]

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

[Kenny Lau]

(there's a different category for each universe)

[Kenny Lau]

(but it doesn't matter)

[Kevin Buzzard]

my understanding is that sometimes it does matter

[Kevin Buzzard]

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

[Scott Morrison]

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.

[Scott Morrison]

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. :-)

[Scott Morrison]

(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.)

[Scott Morrison]

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.

[Scott Morrison]

The two options I considered were:

[Scott Morrison]

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.

[Scott Morrison]

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).

[Scott Morrison]

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.

[Scott Morrison]

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.