Continuous linear equivs

Stream: Is there code for X?

[Kevin Buzzard]

I want bicontinuous isomorphisms between e.g. topological vector spaces (and more generally topological R-modules). Do we have these and if not, would a PR be welcome?

[Eric Wieser]

docs#ContinuousLinearEquiv ?

[Kevin Buzzard]

Oh perfect! Thanks!

[Kevin Buzzard]

Wait, I need the inverse map to be continuous too... aah, no, the axiom is there, it's just that somehow the name is not quite right maybe :-)

[Eric Wieser]

It's e.symm.continuous

[Kevin Buzzard]

Sure, I'm just noting that a ContinuousLinearEquiv is not a linear equiv which is continuous

[Jireh Loreaux]

What would you propose to call it instead Kevin?

[Jireh Loreaux]

HomeomorphLinearEquiv?

[Jireh Loreaux]

I think we allow this naming because there is no reason for ContinuousLinearEquiv to mean a LinearEquiv that is continuous since (a) this doesn't have many nice properties as a type unto itself, and (b) e : E →ₗ[𝕜] F and he : Continous e is a perfectly fine spelling for the latter.

[Heather Macbeth]

And also because of the Banach open mapping theorem: in Banach spaces, the two are equivalent. docs#LinearEquiv.continuous_symm

[Eric Wieser]

One strong argument for the current ContinuousLinearEquiv naming is that it matches the title you chose when you were looking for it :)

[Kevin Buzzard]

Yes but ironically when I actually searched, I searched for HomeomorphLinearEquiv :-)