RFC: bicontinuous maps shouldn't be called `ContinuousEquiv`

Stream: mathlib4

[Kevin Buzzard]

We are taught as mathematics undergraduates that a continuous bijection between topological spaces might not have a continuous inverse, and the special word "homeomorphism" is used for a continuous bijection which does happen to have a continuous inverse. Mathlib has translated this to docs#Homeomorph , a reasonable choice given that this is (at least most of the letters of) what the word is in English. But docs#ContinuousLinearEquiv has always bothered me a little, because (for the same reasons) it's not a linear isomorphism which is also continuous, it's an isomorphism in the category of topological algebraic objects, i.e. a continuous linear bijection with continuous linear inverse. It has just occurred to me that we could change the name of this declaration to BicontinuousLinearEquiv and all of a sudden the ambiguity is resolved, because "bicontinuous map" is another word for "homeomorphism". Mathlib has just added docs#ContinuousMulEquiv and docs#ContinuousAddEquiv a few days ago and my comments also apply to these declarations; I think there's a reasonable argument that they should be called BicontinuousMulEquiv etc. I started thinking about this because we have ContinuousAlgEquiv in FLT and it irked me when merging it that it wasn't a continuous algebra equivalence. ContinuousAffineEquiv also suffers from the same problem. Do you think we should change all of them or am I fussing about nothing?

[Kevin Buzzard]

/poll Should Continuous{Add, Mul, Linear, Affine}Equiv be renamed Bicontinuous{...}Equiv?
Yes
No

[Patrick Massot]

The current name is in line with the fact that an Equiv is not a single map but a pair of map, together with some proof. So it’s less inconsistent that it sounds at first. It doesn’t really answer your question however since we still mostly think of Equiv in the normal way.

[Chris Hughes]

Why not LinearHomeomorphism. Bicontintuous is too much like bilinear for my taste

[Eric Wieser]

I think part of the issue here is that the docstring (for the linear version) doesn't resolve the ambiguity; if we fix that is that sufficient?

[Eric Wieser]

Chris Hughes said:

Why not LinearHomeomorphism. Bicontintuous is too much like bilinear for my taste

I guess to be maximally consistent, we should either do this or rename Homeomorph to ContinuousEquiv

[Kevin Buzzard]

I would be open to MulHomeomorph, LinearHomeomorph etc. I'd also be very open to changing *Homeomorph to *Homeomorphism

[Sébastien Gouëzel]

ContinuousLinearEquiv means that both maps in the equiv are continuous linear, so I don't see why there is an issue here.

[Kevin Buzzard]

Because it reads as "a continuous linear equivalence" which in my mind (but less so, after Patrick's comment) sounds like "we're not assuming the inverse is continuous", i.e. "a continuous (linear equivalence)".

[Kevin Buzzard]

I guess the issue is whether you think of an equivalence (or an isomorphism) as one map with some nice properties, or two maps with some nice properties.

[Yaël Dillies]

I've always found Homeomorph to be a mouthful. What about Homeo?

[Yaël Dillies]

It's short, standard and unambiguous

[Yaël Dillies]

Incidentally, it's the same length as Equiv

[Kevin Buzzard]

Why are you pro making things shorter and less easy to understand, when bytes are free?

[Kevin Buzzard]

Are you voting for Doset? ;-)

[Kevin Buzzard]

We never write Homeomorph anyway, we have notation for it.

[Patrick Massot]

To me Homeo is slightly easier to understand than Homeomorph. I would never write homeomorph on paper while I write homeo very often.

[Patrick Massot]

Of course Homeomorphism is even clearer.

[Patrick Massot]

Kevin Buzzard said:

We never write Homeomorph anyway, we have notation for it.

It appears in lemma names.

[Yaël Dillies]

My point is that if we're to shorten the name we might as well shorten it to something recognisable

[Jireh Loreaux]

Anything that is an XEquiv should be an isomorphism in the concrete category with X as the morphisms. The fact that in a bunch of algebraic categories this is equivalent to a morphism in the category which, as a function, has an inverse, should not have any effect.

And @Kevin Buzzard, if you worked in better categories :laughing: (e.g., Banach spaces) then a continuous (linear equiv) is a docs#ContinuousLinearEquiv (obviously tongue-in-cheek).

[Jireh Loreaux]

In other words, I think the canonical way to refer to a linear equivalence which is also continuous in the forward direction should be either (f : E →L[𝕜] F) (hf : Function.Bijective f) or (f : E ≃ₗ[𝕜] F) (hf : Continuous f) depending on whether it is the continuity or the computability of the inverse which is more important.