Why no `IsHomeomorph` property?

Stream: mathlib4

[Ben Eltschig]

For simple functions between types, there is both Function.Bijective, a property encoding that a function is invertible, and Equiv, a structure carrying both the function and its inverse. This makes it possible to have theorems like bijective_iff : Bijective f ↔ ... when a function is only bijective under certain conditions, and still allows you to refer to the corresponding equiv as Equiv.ofBijective (bijective_iff.mpr ...). For homeomorphisms though, it seems to me that there is only the Homeomorph structure extending Equiv and no corresponding IsHomeomorph property. Why is that the case?

[Ben Eltschig]

I get that equivs are easier to work with because they directly bundle all the relevant maps and properties, and that properties like IsHomeomorph would thus get used less often in comparison, but it still seems like a bit of an oversight to me that currently the easiest ways to write "f is a homeomorphism" (at least that I know of) are Continuous f ∧ IsOpenMap f ∧ Bijective fand ∃ h : Homeomorph X Y, h = f

[Floris van Doorn]

One potential issue is that if we define IsHomeomorph, we are then tempted to state each lemma that mentions homeomorphisms twice, once using Homeomorph and once using IsHomeomorph.

You are correct that in the current situation it is indeed a bit cumbersome to state that a given function is a homeomorphism. We could add an IsHomeomorph predicate, and have a bit of API to conveniently transform between Homeomorph and IsHomeomorph.

[Jireh Loreaux]

I think the API for homeomorphisms in general is underdeveloped. I would be in favor of an IsHomeomorph predicate.

[Antoine Chambert-Loir]

Shouldn't this kind of predicate be defined more or less automatically, together with some basic API ? As suggested by floris, this is painful to have to do this by hand for every such structure.

[Jireh Loreaux]

I would argue that we don't want to do it for every such structure (unless we do a wider refactor to separate data from properties every, including in bundled structures). Homeomorphisms are a bit of a special case, especially because we unbundle large portions of topology.

[Antoine Chambert-Loir]

Probably not for all, but the basic math vocabulary is built on the (noncategorical) point of view of structures for which isomorphisms are bijections that preserve everything , hence play an important rôle.

[Antoine Chambert-Loir]

(From the univalent type theoretic point of view, isomorphisms would just be type equalities! https://www.sciencedirect.com/science/article/pii/S0019357713000694)

[Jireh Loreaux]

Antoine, what I mean is that we don't have this unbundling for most kinds of morphisms. For example, docs#IsMonoidHom technically exists, but it has been deprecated for ages now.

[Antoine Chambert-Loir]

My (meager) point is that IsHomeomorph is of a different nature than docs#IsMonoidHom. The former is about isomorphisms, and is basically intrinsic, the second one is about morphisms and requires the choice of an adequate definition.

[Ben Eltschig]

I think what Jireh means is that it makes sense to talk about homeomorphisms in an unbundled way because we already do the same with continuous maps a lot, but that that isn't true for monoid morphisms?

[Ben Eltschig]

also, a monoid isomorphism is just a monoid morphism that's bijective, right? so there's no need for an extra predicate for that, Bijective already is one

[Ben Eltschig]

I've gone ahead and opened a PR (#12533) adding such a predicate together with a few properties and characterisations that I think would be useful - does that look about right? I'm not very experienced with designing API like this so I imagine there's probably still lots of things to improve, but I hope this should be a good start

[Andrew Yang]

@Ben Eltschig What’s the status of this? This is useful for me somewhere else and I could try and finish the PR process if you have decided not to continue with it.

[Ben Eltschig]

@Andrew Yang Oh, sorry for leaving the PR hanging like that - by the time it was first reviewed I was already quite busy with my thesis and other coursework again, so I somewhat forgot about it and also didn't check Zulip for a while. I probably won't have time for it in the next few weeks either, so if you want to get it merged earlier, feel free to take over the PR.