quotient homeomorphisms

Stream: Is there code for X?

[Adam Topaz]

Do we have something similar to the following?

import topology.homeomorph

variables {α β : Type*} [topological_space α] [topological_space β]

example {f : α → β} (hf : quotient_map f) : β ≃ₜ quot (λ a b : α, f a = f b) := sorry

[Adam Topaz]

In case anyone wants a golfing challenge...

import topology.homeomorph

variables {α β : Type*} [topological_space α] [topological_space β]

noncomputable theory

example {f : α → β} (hf : quotient_map f) : quot (λ a b : α, f a = f b) ≃ₜ β :=
homeomorph.homeomorph_of_continuous_open
(equiv.of_bijective (quot.lift f $ by tauto) begin
  split,
  { rintro ⟨a⟩ ⟨b⟩ h, exact quot.sound h },
  { intro a, obtain ⟨a,rfl⟩ := hf.surjective a, use quot.mk _ a }
end) begin
  rw quotient_map_quot_mk.continuous_iff,
  have : ((equiv.of_bijective (quot.lift f _) _) ∘ quot.mk (λ (a b : α), f a = f b)) = f,
  { ext, refl },
  rw this,
  exact hf.continuous
end begin
  intros U hU,
  rw ← quotient_map_quot_mk.is_open_preimage at hU,
  rw ← hf.is_open_preimage,
  convert hU,
  ext t,
  split,
  { intro h,
    simp only [set.mem_preimage, set.mem_image, equiv.of_bijective_apply] at h ⊢,
    rcases h with ⟨⟨x⟩,hx,h : f x = f t⟩,
    convert hx using 1,
    exact quot.sound h.symm },
  { rintro (h : quot.mk _ t ∈ U),
    simp only [set.mem_preimage, set.mem_image, equiv.of_bijective_apply],
    exact ⟨quot.mk _ t, h, rfl⟩ }
end

[Ruben Van de Velde]

In line 14:

  rw quotient_map_quot_mk.continuous_iff,
  convert hf.continuous using 1,

[Adam Topaz]

Even exact hf.continuous works ;)

[Adam Topaz]

(after the rewrite)

[Eric Wieser]

That quotient condition is docs#setoid.ker

[Eric Wieser]

Which may have some lemmas that help

[Adam Topaz]

A bit better:

import data.setoid.basic
import topology.homeomorph

variables {α β : Type*} [topological_space α] [topological_space β]

noncomputable theory

example {f : α → β} (hf : quotient_map f) : quotient (setoid.ker f) ≃ₜ β :=
{ continuous_to_fun := quotient_map_quot_mk.continuous_iff.mpr hf.continuous,
  continuous_inv_fun := begin
    rw hf.continuous_iff,
    convert continuous_quotient_mk,
    ext,
    simpa [(setoid.quotient_ker_equiv_of_surjective f (quotient_map.surjective hf)).symm_apply_eq],
  end,
  ..(setoid.quotient_ker_equiv_of_surjective _ hf.surjective) }

[Eric Wieser]

That strikes me as quite a lot better :)