Continuous bijective from compact to T1 implies homeomorphis

Stream: Is there code for X?

[Riccardo Brasca]

I guess that we have somewhere in mathlib the fact that a continuous bijection from a compact space to a separated space is an homeomorphism, but I am not able to find it... does someone know where is it?

[Sebastien Gouezel]

You have docs#continuous.closed_embedding

[Riccardo Brasca]

Thank's! It seems a little strange to me that we don't have the literal statement, but may I am missing some subtleties about this part of the library.

[Johan Commelin]

I think there was a PR recently with a constructor for homeo that did just that. But maybe I misremember.

[Kevin Buzzard]

I just wanted this and was about to ask here but Zulip pointed me to this thread when I was composing the title. I have the same question except I'm only smart enough to prove it for t2 spaces. Do we really not have either of these?

import topology.homeomorph

theorem foo {X Y : Type*} [topological_space X] [topological_space Y]
[compact_space X] [t2_space Y]
  {f : X ≃ Y} (hf : continuous f) : continuous f.symm :=
begin
  refine continuous_iff_is_closed.mpr _,
  intros C hC,
  have hC2 : is_compact C := by library_search,
  have hC3 : is_compact (f '' C) := by library_search,
  have hC4 : is_closed (f '' C) := by library_search,
  convert hC4 using 1,
  tidy,
end

def bar (X Y : Type*) [topological_space X] [topological_space Y]
[compact_space X] [t2_space Y]
  (f : X ≃ Y) (hf : continuous f) : X ≃ₜ Y :=
{
  continuous_to_fun := hf,
  continuous_inv_fun := foo hf,
  ..f }

What I like about the proof of foo is that it's essentially the proof I'd write on the board.

[Reid Barton]

It's apparently not actually true for T1 spaces.

[Kyle Miller]

If both $X$ and $Y$ have $\mathbb{N}\cup\{\infty\}$ as their points where $X$ is the one-point compactification of $\mathbb{N}$ and $Y$ has the cofinite topology, then $X$ is compact, $Y$ is T1, the identity function is a continuous bijection, but it's not a homeomorphism.

[Adam Topaz]

docs#CompHaus.is_iso_of_bijective should be a thing (I think)

[Kevin Buzzard]

Oh perfect, that will do for me. Adam I'm still wrestling with that binary product thing ;-)

[Adam Topaz]

I think we have a wrapper for Profinite too... Let's check docs#Profinite.is_iso_of_bijective

[Patrick Massot]

Adam Topaz said:

docs#CompHaus.is_iso_of_bijective should be a thing (I think)

I think it's a bad idea to add mathematical content to the category theory part of mathlib. It should only wrap mathematical content. If the concrete lemma is missing I think you should add it first and then wrap it.

[Patrick Massot]

Kyle Miller said:

If both $X$ and $Y$ have $\mathbb{N}\cup\{\infty\}$ as their points where $X$ is the one-point compactification of $\mathbb{N}$ and $Y$ has the cofinite topology, then $X$ is compact, $Y$ is T1, the identity function is a continuous bijection, but it's not a homeomorphism.

Don't hesitate to add this example right after proving the lemma. I think we should have more of those in mathlib.

[Adam Topaz]

import topology.category.Compactum

open category_theory

local attribute [instance] Compactum_to_CompHaus.is_equivalence

instance : reflects_isomorphisms Compactum.forget :=
(of_type_monad ultrafilter).forget_reflects_iso

lemma category_theory.reflects_isomorphisms_comp {C D E : Type*} [category C] [category D]
  [category E] (F : C ⥤ D) (G : D ⥤ E) [reflects_isomorphisms F] [reflects_isomorphisms G] :
  reflects_isomorphisms (F ⋙ G) :=
begin
  constructor,
  intros A B f hf,
  dsimp at hf,
  resetI,
  suffices : is_iso (F.map f),
  { resetI, apply is_iso_of_reflects_iso f F },
  apply is_iso_of_reflects_iso (F.map f) G,
end

instance : reflects_isomorphisms Compactum_to_CompHaus.inv :=
category_theory.of_full_and_faithful Compactum_to_CompHaus.inv

instance : reflects_isomorphisms (Compactum_to_CompHaus.inv ⋙ forget _) :=
category_theory.reflects_isomorphisms_comp _ _

lemma category_theory.reflects_isomorphisms_of_iso {C D : Type*} [category C] [category D]
  {F G : C ⥤ D} (η : F ≅ G) [reflects_isomorphisms G] : reflects_isomorphisms F :=
begin
  constructor,
  rintros A B f ⟨g,h1,h2⟩,
  haveI : is_iso (G.map f) := begin
    constructor,
    use η.inv.app B ≫ g ≫ η.hom.app A,
    split,
    { simp [reassoc_of h1] },
    { simp only [category.assoc, ← η.hom.naturality, reassoc_of h2], simp }
  end,
  apply is_iso_of_reflects_iso f G,
end

instance : reflects_isomorphisms (forget CompHaus) :=
let E : forget CompHaus ≅ Compactum_to_CompHaus.inv ⋙ Compactum.forget :=
  iso_whisker_right Compactum_to_CompHaus.as_equivalence.counit_iso.symm (forget _) in
category_theory.reflects_isomorphisms_of_iso E

lemma CompHaus.is_iso_of_bijective' {X Y : CompHaus} (f : X ⟶ Y) (hf : function.bijective f) :
  is_iso f :=
begin
  rw ← is_iso_iff_bijective at hf,
  change is_iso ((forget _).map f) at hf,
  resetI,
  apply is_iso_of_reflects_iso f (forget _),
end

[Kyle Miller]

Patrick Massot said:

Don't hesitate to add this example right after proving the lemma. I think we should have more of those in mathlib.

I wasn't sure whether what @Kevin Buzzard wrote made it into mathlib (at least I couldn't find the theorem statement), so I created #11072 just in case.

It also has a counterexample for the T1 generalization, written as

lemma homeo_of_equiv_compact_to_t2.t1_counterexample :
  ∃ (α β : Type) (Iα : topological_space α) (Iβ : topological_space β), by exactI
  ∃ (hα : compact_space α) (hβ : t1_space β) (f : α ≃ β) (hf : continuous f),
  ¬ continuous f.symm

though I probably should refactor the proof -- I basically reimplemented the one-point compactification, and I wasn't sure whether the cofinite topology already existed in some way so I implemented that for nat with the discrete topology, too.

[Patrick Massot]

@Kyle Miller I just opened #11076

[Patrick Massot]

Sorry about all those missing pieces.

[Patrick Massot]

I haven't included your counter-example, this is your reward.

[Patrick Massot]

After that PR you'll be able to modify yours to use:

lemma homeo_of_equiv_compact_to_t2.t1_counterexample :
  ∃ (α β : Type) (Iα : topological_space α) (Iβ : topological_space β), by exactI
  compact_space α ∧ t1_space β ∧ ∃ f : α ≃ β, continuous f ∧ ¬ continuous f.symm :=
begin
  let topα : topological_space ℕ := nhds_adjoint 0 filter.cofinite,
  let topβ : topological_space ℕ := topological_space.cofinite ℕ,
  refine ⟨ℕ , ℕ, topα, topβ, _, t1_space_cofinite, equiv.refl ℕ, _, _⟩,
  { constructor,
    rw is_compact_iff_ultrafilter_le_nhds,
    intros f,
    suffices : ∃ a, ↑f ≤ @nhds _ topα a, by simpa,
    by_cases hf : ↑f ≤ @nhds _ topα 0,
    { exact ⟨0, hf⟩ },
    { obtain ⟨U, h0U, hU_fin, hUf⟩ : ∃ U : set ℕ, 0 ∈ U ∧ Uᶜ.finite ∧ U ∉ f,
      { rw [nhds_adjoint_nhds, filter.le_def] at hf,
        push_neg at hf,
        simpa [and_assoc] using hf },
      rw ← ultrafilter.compl_mem_iff_not_mem at hUf,
      obtain ⟨n, hn', hn⟩ := ultrafilter.eq_principal_of_finite_mem hU_fin hUf,
      use n,
      intros s' hns',
      rw hn,
      exact @mem_of_mem_nhds _ topα n _ hns' } },
  { rw continuous_iff_coinduced_le,
    change topα ≤ topβ,
    rw gc_nhds,
    simp [nhds_cofinite] },
  { intros h,
    replace h : topβ ≤ topα, by simpa [continuous_iff_coinduced_le, coinduced_id] using h,
    rw le_nhds_adjoint_iff at h,
    exact  (finite_singleton 1).infinite_compl (h.2 1 one_ne_zero ⟨1, mem_singleton 1⟩) }
end

[Patrick Massot]

Note this proof isn't much shorter if you take into account that the topology definitions have been removed, but it minimizes messing around with sets.

[Kyle Miller]

Patrick Massot said:

Sorry about all those missing pieces.

No need to apologize! I was happy doing this as an exercise, and it's nice that it helped drive more library development. (Thanks for implementing eq_principal_of_finite_mem, too.)

[Patrick Massot]

Indeed counter-examples also have this library development role.

[Patrick Massot]

The cofinite topology was a really unexpected hole.

[Kyle Miller]

Is there a construction like docs#topological_space.nhds_adjoint that could specialize to docs#alexandroff.topological_space?

[Patrick Massot]

I guess we could cook up a definition giving both cases, but I'm not sure we would gain much.