Zulip Chat Archive

Stream: maths

Topic: homeos


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

@Scott Morrison For the perfectoid project I had to get back to my old https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/homeos.lean defining homeomorphisms. But now we have the category Top in mathlib, and isomorphisms. Can I throw away my file and use the category theory stuff? How would that work?

view this post on Zulip Reid Barton (Sep 20 2018 at 20:06):

That's what I did in lean-homotopy-theory. My internet is acting up and I can't provide a direct link, but the filename is src/homotopy_theory/topological_spaces/homeomorphism.lean

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

great

view this post on Zulip Patrick Massot (Sep 20 2018 at 20:12):

It looks nice, but I'd like to be able to plug this into the story we have in the separation thread

view this post on Zulip Patrick Massot (Sep 20 2018 at 20:12):

Do you think it's possible, or does it mean everything must be rewritten in terms of Top instead of topological_space?


Last updated: May 14 2021 at 19:21 UTC