Why uniform_space?

Stream: new members

[Damiano Testa]

Dear All,

I am trying to prove the lemma below. I thought that is_open_ball was all I needed, but I seem to have to use that a metric_space is a uniform_space.

Does anyone know how I can finish the proof?

Thanks!

import topology.metric_space.basic

open topological_space metric

example {α : Type*} [topological_space α] [metric_space α] (x y : α) (yc : y ∈ ({x} : set α)ᶜ) :
  is_open (ball y (dist y x)) :=
begin
  convert @is_open_ball α _inst_2 y (dist y x),
  sorry,
end

[Kevin Buzzard]

Just checking -- is that really the way to set up the example? It might say "alpha is a topological space and a metric space, but these two structures are entirely unrelated"

[Damiano Testa]

Ah, let me try!

[Damiano Testa]

Sorry, you are perfectly right!

Thanks!

[Kevin Buzzard]

yeah, your way is a lot harder :-)

[Damiano Testa]

Indeed, I struggled for a little bit, not realizing what was going on!

[Damiano Testa]

Given that we are here. Is there a t1_space instance on metric_space? (Or indeed, most of the t_i_space instances?)

[Mario Carneiro]

there should be

[Damiano Testa]

(This is where the question came from: I defined a t1_space instance, thinking that it would be easy, and it is if I do not use two different topological space structures! :face_palm: )

[Kevin Buzzard]

import topology.metric_space.basic

open topological_space metric

example {α : Type*} [metric_space α] : t1_space α := by apply_instance

Yes.

[Kevin Buzzard]

This had to be there, otherwise Patrick's proof the other day wouldn't have worked.

[Mario Carneiro]

I'm trying to answer this question the hard way, by reading the sources

[Kevin Buzzard]

example {α : Type*} [metric_space α] : t1_space α := by show_term {apply_instance} is the easy way now

[Damiano Testa]

Ok, I think all my confusion started with the two separate assumption topological_space and metric_space.

Thanks for clearing this up for me!

[Kevin Buzzard]

I didn't really get typeclasses until I actually made something which used them (schemes)

[Mario Carneiro]

I see that uniform_space.basic imports topology.separation but it doesn't actually use anything in the file

[Kevin Buzzard]

write a linter!

[Kevin Buzzard]

isn't that what you kids do?

[Mario Carneiro]

Hm, we don't have that metric spaces are normal though

[Adam Topaz]

Even better:

import topology.metric_space.basic
example {X : Type*} [metric_space X] : regular_space X := by apply_instance

[Adam Topaz]

What comes after t3?

[Mario Carneiro]

regular, then normal

[Adam Topaz]

regular = t3 right?

[Mario Carneiro]

yeah

[Mario Carneiro]

I think there is another one in between

[Kevin Buzzard]

Are regular and normal really words for topological spaces? They're also predicates on commutative rings. Regular implies normal for commutative rings

[Reid Barton]

they are

[Kevin Buzzard]

maths is so messed up

[Adam Topaz]

normal implies regular for spaces :sad:

[Kevin Buzzard]

that's because spec is contravariant

[Adam Topaz]

Wikipedia says there's TX for X in {0,1,2,2.5,3,3.5,4,5,6}

[Mario Carneiro]

• X is T0, or Kolmogorov, if any two distinct points in X are topologically distinguishable. (It will be a common theme among the separation axioms to have one version of an axiom that requires T0 and one version that doesn't.)
• X is R0, or symmetric, if any two topologically distinguishable points in X are separated.
• X is T1, or accessible or Fréchet or Tikhonov, if any two distinct points in X are separated. Thus, X is T1 if and only if it is both T0 and R0. (Although you may say such things as "T1 space", "Fréchet topology", and "suppose that the topological space X is Fréchet"; avoid saying "Fréchet space" in this context, since there is another entirely different notion of Fréchet space in functional analysis.)
• X is R1, or preregular, if any two topologically distinguishable points in X are separated by neighbourhoods. Every R1 space is also R0.
• X is Hausdorff, or T2 or separated, if any two distinct points in X are separated by neighbourhoods. Thus, X is Hausdorff if and only if it is both T0 and R1. Every Hausdorff space is also T1.
• X is T2½, or Urysohn, if any two distinct points in X are separated by closed neighbourhoods. Every T2½ space is also Hausdorff.
• X is completely Hausdorff, or completely T2, if any two distinct points in X are separated by a continuous function. Every completely Hausdorff space is also T2½.
• X is regular if, given any point x and closed set F in X such that x does not belong to F, they are separated by neighbourhoods. (In fact, in a regular space, any such x and F will also be separated by closed neighbourhoods.) Every regular space is also R1.
• X is regular Hausdorff, or T3, if it is both T0 and regular.[1] Every regular Hausdorff space is also T2½.
• X is completely regular if, given any point x and closed set F in X such that x does not belong to F, they are separated by a continuous function. Every completely regular space is also regular.
• X is Tychonoff, or T3½, completely T3, or completely regular Hausdorff, if it is both T0 and completely regular.[2] Every Tychonoff space is both regular Hausdorff and completely Hausdorff.
• X is normal if any two disjoint closed subsets of X are separated by neighbourhoods. (In fact, a space is normal if and only if any two disjoint closed sets can be separated by a continuous function; this is Urysohn's lemma.)
• X is normal regular if it is both R0 and normal. Every normal regular space is regular.
• X is normal Hausdorff, or T4, if it is both T1 and normal. Every normal Hausdorff space is both Tychonoff and normal regular.
• X is completely normal if any two separated sets are separated by neighbourhoods. Every completely normal space is also normal.
• X is completely normal Hausdorff, or T5 or completely T4, if it is both completely normal and T1. Every completely normal Hausdorff space is also normal Hausdorff.
• X is perfectly normal if any two disjoint closed sets are precisely separated by a continuous function. Every perfectly normal space is also completely normal.
• X is perfectly normal Hausdorff, or T6 or perfectly T4, if it is both perfectly normal and T1. Every perfectly normal Hausdorff space is also completely normal Hausdorff.

I feel like the list gets longer every time I look at it

[Adam Topaz]

Right. Time to switch to condensed sets then.

[Kevin Buzzard]

@Damiano Testa if you're still around, then here's something you might want to think about. In #4301 there is the following proof:

lemma non_root_interval_of_polynomial (α : ℝ) (f : polynomial ℝ) (h_f_nonzero : f ≠ 0) :
  ∃ B : ℝ, 0 < B ∧ ∀ x (hr : abs (α - x) < B) (hn : x ≠ α), f.eval x ≠ 0 :=
begin
  set f_roots := f.roots.to_finset.erase α,
  set distances := insert (1 : ℝ) (f_roots.image (λ x, abs (α - x))),
  have h_nonempty : distances.nonempty := ⟨1, finset.mem_insert_self _ _⟩,
  set B := distances.min' h_nonempty with hB,
  have h_allpos : ∀ x : ℝ, x ∈ distances → 0 < x,
  { intros x hx, rw [finset.mem_insert, finset.mem_image] at hx,
    rcases hx with rfl | ⟨α₀, ⟨h, rfl⟩⟩,
    { exact zero_lt_one },
    { rw [finset.mem_erase] at h,
      rw [abs_pos, sub_ne_zero], exact h.1.symm }},
  use [B, (h_allpos B (distances.min'_mem h_nonempty))],
  intros x hx hxα,
  have hab₂ : x ∉ f.roots.to_finset,
  { intro h,
    have h₁ : x ∈ f_roots, { rw [finset.mem_erase], exact ⟨hxα, h⟩ },
    have h₂ : abs (α - x) ∈ distances,
    { rw [finset.mem_insert, finset.mem_image], right, exact ⟨x, ⟨h₁, rfl⟩⟩ },
    have h₃ := finset.min'_le distances (abs (α - x)) h₂,
    erw ←hB at h₃, linarith only [lt_of_lt_of_le hx h₃] },
  rwa [multiset.mem_to_finset, mem_roots h_f_nonzero, is_root.def] at hab₂
end

(to make it run you need to go to a local copy of mathlib, checkout liouville_theoerm/lemmas, type leanproject get-cache and then open analysis/real/polynomial.lean). This PR is making the same mistake you were making earlier. Can you make that proof about 1/4 the length?

[Mario Carneiro]

Hm, so I started trying to prove this and got stuck on the very first step:

import topology.uniform_space.separation

open topological_space
open_locale classical topological_space uniformity filter

instance separated_normal {α} [uniform_space α] [separated_space α] : normal_space α :=
⟨λs t hs ht d, begin
  have : {p : α × α | p.1 ∈ s → p.2 ∉ t} ∈ 𝓤 α,
  { sorry },
end⟩

why should this be true?

[Mario Carneiro]

it seems like you might need some kind of compactness property to be able to get all the neighborhoods together

[Mario Carneiro]

ah, it's false

[Damiano Testa]

@Kevin Buzzard it was looking at liouville that I decided to prove the lemma about discreteness of roots of polynomials: I am indeed planning to apply this to make the arguments quicker! Though, tonight I should rest: assuming two topologies on the same space was my cue!