Zulip Chat Archive

Stream: new members

Topic: Why uniform_space?


view this post on Zulip Damiano Testa (Dec 09 2020 at 20:13):

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

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:14):

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"

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:14):

Ah, let me try!

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:15):

Sorry, you are perfectly right!

Thanks!

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:15):

yeah, your way is a lot harder :-)

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:16):

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

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:18):

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

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:18):

there should be

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:19):

(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: )

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:21):

import topology.metric_space.basic

open topological_space metric

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

Yes.

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:21):

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

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:22):

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

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:22):

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

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:22):

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

Thanks for clearing this up for me!

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:23):

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

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:25):

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

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:25):

write a linter!

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:26):

isn't that what you kids do?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:28):

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

view this post on Zulip Adam Topaz (Dec 09 2020 at 20:36):

Even better:

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

view this post on Zulip Adam Topaz (Dec 09 2020 at 20:38):

What comes after t3?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:38):

regular, then normal

view this post on Zulip Adam Topaz (Dec 09 2020 at 20:39):

regular = t3 right?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:39):

yeah

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:39):

I think there is another one in between

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:39):

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

view this post on Zulip Reid Barton (Dec 09 2020 at 20:39):

they are

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:39):

maths is so messed up

view this post on Zulip Adam Topaz (Dec 09 2020 at 20:39):

normal implies regular for spaces :sad:

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:40):

that's because spec is contravariant

view this post on Zulip Adam Topaz (Dec 09 2020 at 20:40):

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

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:41):

  • 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

view this post on Zulip Adam Topaz (Dec 09 2020 at 20:42):

Right. Time to switch to condensed sets then.

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 20:47):

@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?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:47):

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?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:49):

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

view this post on Zulip Mario Carneiro (Dec 09 2020 at 20:52):

ah, it's false

view this post on Zulip Damiano Testa (Dec 09 2020 at 20:57):

@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!


Last updated: May 13 2021 at 00:41 UTC