transferring topological properties along homeomorphisms

Stream: Is there code for X?

[Kevin Buzzard]

The 2nd year analysis lecturer at Imperial asked students to prove that if X and Y were homeomorphic topological spaces then X was Hausdorff iff Y was. A student in my course formalised the result as part of a project.

import topology.homeomorph

variables (X Y : Type) [topological_space X] [topological_space Y]

example (e : homeomorph X Y) : t2_space X ↔ t2_space Y :=
sorry

It took many lines. Do we have some kind of tactic which can produce these proofs for free yet?

[Scott Morrison]

Still no. :-(

[Scott Morrison]

It is a bit strange how infrequently we actually need to do this, on the other hand.

[Kevin Buzzard]

I absolutely agree with you about how strange it is. When I opened #408 several years ago I was convinced it would be really important. The situation here is pathological -- for their second projects I asked the students to engage with the material they learnt in Y2 and this was a random question on a problem sheet (rather than anything being used to build more theory, or part of a more complex proof).

[Kevin Buzzard]

At that time I was also convinced that building a classical mathematics library covering an undergraduate curriculum was also important, and I suspect you agreed with me -- at least we were right on that one ;-)

[Kevin Buzzard]

Another thing I found strange was that we don't ever seem to use the bijection between equivalence relations and partitions (which I got Amelia to make, convinced that it would be important). My model of mathematics was that this was used absolutely everywhere; more recently I have become slightly embarrassed to even teach it to the 1st years! Someone suggested to me that it was perhaps because Lean uses type theory and has inbuilt quotients.

[Johan Commelin]

@Kevin Buzzard I'm not sure that matters. We could have built an identical quotient API without axioms. At that point we would need to use a little bit about equivalence relations and partitions. But once the API is in place, I don't think you would ever need to look under the hood.
The only downside would be less defeqs.

[Patrick Massot]

import topology.homeomorph

variables (X Y : Type) [topological_space X] [topological_space Y]

example (e : homeomorph X Y) : t2_space X ↔ t2_space Y :=
by { split ; introI h, exacts [e.t2_space, e.symm.t2_space] }

Do I win something?

[Johan Commelin]

For this particular problem, it is again the case that it "generalises" to a non-trivial problem: If f : X → Y is continuous and injective, and Y is a t2_space, then so is X.

[Patrick Massot]

I guess that using the result from mathlib is cheating so I reproved it from scratch (only one implication since the other one is completely symmetric):

example (e : homeomorph X Y) (h : t2_space X) : t2_space Y :=
begin
  rw t2_iff_nhds at *,
  refine λ y y' hyy', e.symm.injective (h ⟨λ H, _⟩),
  rw [e.symm.inducing.nhds_eq_comap, e.symm.inducing.nhds_eq_comap, ← comap_inf, H, comap_bot] at hyy',
  exact hyy'.ne rfl,
end

[Patrick Massot]

From this proof you see immediately that asking for a homeomorphism is too strong if you only care about one implication. The proof clearly only uses that e.symm is an embedding. So you write

example {f : Y → X} (hf : embedding f) (h : t2_space X) : t2_space Y :=
begin
  rw t2_iff_nhds at *,
  refine λ y y' hyy', hf.inj (h ⟨λ H, _⟩),
  rw [hf.to_inducing.nhds_eq_comap, hf.to_inducing.nhds_eq_comap, ← comap_inf, H, comap_bot] at hyy',
  exact hyy'.ne rfl,
end

[Patrick Massot]

But then you think more and see asking for an embedding it too strong, and a continuous injective function is good enough:

open function
open_locale topological_space

example {f : Y → X} (hf : injective f) (hf' : continuous f) (h : t2_space X) : t2_space Y :=
begin
  rw t2_iff_nhds at *,
  refine λ y y' hyy', hf (h ⟨λ H, hyy'.ne $ le_bot_iff.mp _⟩),
  calc 𝓝 y ⊓ 𝓝 y' ≤ comap f (𝓝 $ f y) ⊓ (comap f (𝓝 $ f y')) :
    inf_le_inf (map_le_iff_le_comap.mp hf'.continuous_at) (map_le_iff_le_comap.mp hf'.continuous_at)
  ... = comap f ((𝓝 $ f y) ⊓ (𝓝 $ f y')) : comap_inf.symm
  ... = ⊥ : by rw [H, comap_bot],
end

[Patrick Massot]

At that point things are so clear you start fearing someone could understand what's going on, so you go for full term mode:

example {f : Y → X} (hf : injective f) (hf' : continuous f) (h : t2_space X) : t2_space Y :=
t2_iff_nhds.mpr $ λ y y' hyy', hf $ t2_iff_nhds.mp h
⟨λ H, hyy'.ne $ le_bot_iff.mp $ calc 𝓝 y ⊓ 𝓝 y' ≤ comap f (𝓝 $ f y) ⊓ (comap f (𝓝 $ f y')) :
    inf_le_inf (map_le_iff_le_comap.mp hf'.continuous_at) (map_le_iff_le_comap.mp hf'.continuous_at)
  ... = comap f ((𝓝 $ f y) ⊓ (𝓝 $ f y')) : comap_inf.symm
  ... = ⊥ : by rw [H, comap_bot]⟩

[Kevin Buzzard]

Ok you get an A

[Kevin Buzzard]

Yes it's again this weird observation that the math-trivial "you can transfer P along equivs" can often be deduced from the more contentful statement "you can transfer P along either injections or surjections" which we'll often have in the library anyway.

[Damiano Testa]

Also, thinking about the actual maths use, knowing that a subspace of a separated space is separated is an actually useful fact.

I don't remember if I ever found it easier to show that something was homeomorphic to something separated to deduce separatedness.