homeo of induced by equiv

Stream: Is there code for X?

[Adam Topaz]

I'm working with the following minimal example:

import topology.constructions
import topology.homeomorph

namespace scratch

variables {α β : Type*} [topological_space β] (f : α ≃ β)
instance : topological_space α := topological_space.induced f $ by apply_instance

example : α ≃ₜ β := sorry

end scratch

I have two questions here:

1. There is a maximum class-instance resolution depth error in the example. It seems lean is having trouble finding the topological space instances which I find strange. Why?
2. Does mathlib have the definition needed to fill in the sorry?

[Sebastien Gouezel]

The instance is a bad instance: it means that, whenever Lean is looking for a topological space structure on some type α, it will explore all types β and all equivs between the two types. There is no way to determine which one it should use.

[Adam Topaz]

Oh yes of course.

[Adam Topaz]

I should add fto a synonym for \a, for example.

[Sebastien Gouezel]

Yes, using a type synonym with the information on f would be enough to make things reasonable.

[Adam Topaz]

Okay, so here's an updated code:

import topology.constructions
import topology.homeomorph

namespace scratch

variables {α β : Type*} [topological_space β] (f : α ≃ β)

include f
def γ := α
instance : topological_space (γ f) := topological_space.induced f $ by apply_instance
example : (γ f) ≃ₜ β := sorry

end scratch

Does mathlib have a quick way to fill in the sorry?

[Yury G. Kudryashov]

variables [topological_space β] (f : α ≃ β)

def induced_space (f : α → β) := α

instance : topological_space (induced_space f) := topological_space.induced f $ by apply_instance

example : (induced_space f) ≃ₜ β :=
{ to_equiv := f,
  continuous_to_fun := continuous_induced_dom,
  continuous_inv_fun := continuous_induced_rng (by simp [continuous_id]) }