ContinuousAlgEquiv.toContinuousAddEquiv

Stream: mathlib4

[Kevin Buzzard]

I found this error surprising:

import Mathlib

variable {R A B : Type*} [CommSemiring R] [Semiring A] [TopologicalSpace A]
    [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B)

/--
error: Type mismatch
  e.toAddEquiv.toContinuousAddEquiv
has type
  (∀ (s : Set B), IsOpen (⇑e.toAddEquiv ⁻¹' s) ↔ IsOpen s) → A ≃ₜ+ B
but is expected to have type
  A ≃ₜ+ B
-/
#guard_msgs in
example : A ≃ₜ+ B := e.toContinuousAddEquiv -- surprising error
-- because it goes through `AddEquiv` which forgets the continuity!

-- Do we want this?
def ContinuousAlgEquiv.toContinuousAddEquiv (e : A ≃A[R] B) : A ≃ₜ+ B := {
  __ := e
}

example : A ≃ₜ+ B := e.toContinuousAddEquiv -- now works

Should mathlib have ContinuousAlgEquiv.toContinuousAddEquiv or is the correct fix something more subtle?

[Edward van de Meent]

(docs#ContinuousAlgEquiv, docs#ContinuousAddEquiv )

[Edward van de Meent]

i think this would be fixed if it extended ContinuousAddEquiv instead of Homeomorph?

[Edward van de Meent]

it's possible the reason that's not currently the case is because it could bring with it some bad import chains

[Kevin Buzzard]

Rather than changing the definition should I just add the declaration? It fits perfectly in Mathlib.Topology.Algebra.Algebra.Equiv. I think that changing the definition will cause far more disruption and we don't have any particular need to change the definition?

[Edward van de Meent]

i think adding the declaration should be fine too.

note that we also should get API explaining how the coercions interact (so things like e.toContinuousAddEquiv.toAddEquiv = e.toAddEquiv, e.toContinuousAddEquiv.toHomeomorph = e.toHomeomorph, FunLike.coe e.toContinousAddEquiv = FunLike.coe e etc.), as well as how it interacts with operations like symm and trans

[Aaron Liu]

Should docs#AddEquiv.toContinuousAddEquiv be called instead something like ContinuousAddEquiv.ofAddEquiv to avoid such a collision