Zulip Chat Archive

Stream: Is there code for X?

Topic: homeo of induced by equiv


view this post on Zulip Adam Topaz (Dec 15 2020 at 21:14):

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?

view this post on Zulip Sebastien Gouezel (Dec 15 2020 at 21:20):

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.

view this post on Zulip Adam Topaz (Dec 15 2020 at 21:20):

Oh yes of course.

view this post on Zulip Adam Topaz (Dec 15 2020 at 21:21):

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

view this post on Zulip Sebastien Gouezel (Dec 15 2020 at 21:21):

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

view this post on Zulip Adam Topaz (Dec 15 2020 at 21:27):

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?

view this post on Zulip Yury G. Kudryashov (Dec 18 2020 at 23:25):

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]) }

Last updated: May 19 2021 at 00:40 UTC