Zulip Chat Archive

Stream: new members

Topic: Jay Williams


view this post on Zulip Jay Williams (Sep 27 2020 at 22:14):

Hi all,
I've been playing around with Lean lately, working through the natural number game and the tutorials project. I used to study descriptive set theory, and I thought I might try to prove some of the basics in Lean. There is a lot of overlap between basic point-set topology and basic descriptive set theory, so a lot of useful stuff is already in mathlib, but there are still plenty of things that aren't there yet. My hope is that I can do some of the easy stuff in my free time. :)

I realized that for all the information included in the tutorials project, I still don't know how to do something as basic as define a Polish space (a completely metrizable and separable topological space). There are at least two aspects to this:
a) I'm not sure if it's better to define a Polish space as a metric space or a topological space, i.e. I'm not sure the "correct" way to work with metrizable spaces. Some of the proofs I'd like to do definitely use the metric, though of course there may be some other way to do them.
b) Even if I just decided "okay, I'll just say it's a complete and separable space for now to get started", I'm not sure how to do that. I can find a few similar definitions in mathlib such as that of a borel_space, but I'm not really sure how the class keyword works (for example), and of course most of these files start with a lot of boilerplate that I don't yet understand the significance of.

So if anyone can point me at some relevant docs or examples, that would be excellent. I'm looking forward to getting something proved, even if it's small.

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:17):

If a Polish space is metrizable, then I guess you should say that; that is, it should not come with a metric

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:17):

Also hello

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:19):

As for examples, perhaps something like docs#topological_space.first_countable_topology can get you started? Definition making is one of the more complicated things to do in lean without prior expertise, because it shapes a lot of what comes later and there are sometimes subtle details that relate more to the way lean works than the way the mathematics works

view this post on Zulip Heather Macbeth (Sep 27 2020 at 22:20):

Welcome!

Jay Williams said:

b) Even if I just decided "okay, I'll just say it's a complete and separable space for now to get started", I'm not sure how to do that. I can find a few similar definitions in mathlib such as that of a borel_space, but I'm not really sure how the class keyword works (for example), and of course most of these files start with a lot of boilerplate that I don't yet understand the significance of.

This seems a reasonable way to start. Perhaps you could state (in words) a lemma, then someone here can give you the Lean statement and you can start playing with the proof.

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:24):

The class keyword is just a synonym for @[class] structure, so if you know how the structure keyword works then class is no different. (Of course that might not be any help.)

view this post on Zulip Jay Williams (Sep 27 2020 at 22:25):

Heather Macbeth said:

This seems a reasonable way to start. Perhaps you could state (in words) a lemma, then someone here can give you the Lean statement and you can start playing with the proof.

Ah this is a great idea, I think I was getting ahead of myself a little bit. Well let's see, the very first things in Kechris' _Descriptive Set Theory_ that are proved about Polish spaces are

  1. The completion of a separable metric space is Polish.
  2. A closed subspace of a Polish space is Polish.

view this post on Zulip Kenny Lau (Sep 27 2020 at 22:26):

Learning Lean is like picking up a new language -- you just try out things until they work

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:26):

One thing you don't need any particular lean expertise to do is unpack all the words until everything is in terms of concepts in mathlib

view this post on Zulip Jay Williams (Sep 27 2020 at 22:27):

Ah so rather than worrying about including the words "Polish space" just do the above lemmas with "complete and separable space". That's a good idea!

view this post on Zulip Heather Macbeth (Sep 27 2020 at 22:28):

Jay Williams said:

Ah so rather than worrying about including the words "Polish space" just do the above lemmas with "complete and separable space". That's a good idea!

So if we do this with your (1), is the point that the completion of a separable metric space is separable?

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:28):

you can of course define "Polish space" to mean that, and then you can use Polish space

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:28):

but the point is to define anything you need along the way

view this post on Zulip Jay Williams (Sep 27 2020 at 22:29):

Heather Macbeth said:

Jay Williams said:

Ah so rather than worrying about including the words "Polish space" just do the above lemmas with "complete and separable space". That's a good idea!

So if we do this with your (1), is the point that the completion of a separable metric space is separable?

That's right, that's why it's the very first thing, it's almost immediate.

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:29):

I suppose immediacy is in the eye of the beholder

view this post on Zulip Jay Williams (Sep 27 2020 at 22:30):

As learning Lean is teaching me :)

view this post on Zulip Heather Macbeth (Sep 27 2020 at 22:31):

So I think this would be something like

instance it_begins {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
begin
  sorry
end

(not checked in vscode) (updated, thanks @Kenny Lau )

view this post on Zulip Kenny Lau (Sep 27 2020 at 22:31):

instance

view this post on Zulip Kenny Lau (Sep 27 2020 at 22:34):

I suppose it is obvious :P

view this post on Zulip Heather Macbeth (Sep 27 2020 at 22:34):

Kenny Lau said:

I suppose it is obvious :P

All the better, for a beginner!

view this post on Zulip Kenny Lau (Sep 27 2020 at 22:34):

oh, I just meant mathematically

view this post on Zulip Kenny Lau (Sep 27 2020 at 22:35):

and that translates to easy in Lean if you prove the right lemmas

view this post on Zulip Mario Carneiro (Sep 27 2020 at 22:35):

which is of course the hard part

view this post on Zulip Jay Williams (Sep 27 2020 at 22:36):

Yes, this is definitely a great start. I'm trying it out now and discovering that I don't quite have my Lean environment set up correctly. The fun part of programming ha. But I will work on this, thanks!

view this post on Zulip Heather Macbeth (Sep 27 2020 at 22:41):

And then when you succeed you should PR it! :smiley:
https://leanprover-community.github.io/contribute/index.html

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:50):

And see if it works for a [emetric_space] instead of a [metric_space].

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:51):

BTW, do we use [separable_space] or [second_countable_topology] as a "normal form" of assumption for a [emetric_space]?

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:52):

Measure theory assumes [second_countable_topology] in many lemmas and definitions.

view this post on Zulip Jay Williams (Sep 27 2020 at 22:52):

Actually, this is a bit embarrassing, but I can't figure out the import for separable_space. I see that the definition is in topology/bases.lean, but when I try

import topology.metric_space.basic
import topology.uniform_space.completion
import topology.bases

instance it_begins {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
begin
  sorry
end

I get red squigglies underneath separable_space.

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:53):

Please add a newline after the first "```"

view this post on Zulip Jay Williams (Sep 27 2020 at 22:53):

In a metrizable space separability and second countability are equivalent, so I'm fine with either.

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:53):

Possibly it is in the topological_space namespace

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:54):

So you can either write topological_space.separable_space, or open topological_space

view this post on Zulip Jay Williams (Sep 27 2020 at 22:55):

That worked, though it turns out I have the wrong import for the completion... one thing at a time I guess :smile:

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:55):

I think that we don't have many theorems about metrizable topological spaces because we didn't have to work with metrizable spaces with no natural [emetric_space] structure.

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:56):

Try topology/metric_space/completion.

view this post on Zulip Jay Williams (Sep 27 2020 at 22:56):

Certainly the important examples in descriptive set theory all have natural metrics (Baire space, Cantor space, the reals...)

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 22:59):

It's easy to define (untested)

class metrizable (α : Type*) [h : topological_space α] :=
(metrizable :  β : emetric_space α, β.to_topological_space = h)

But every proof about [metrizable α] will start with

begin
  letI : emetric_space α := ...,
end

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 23:04):

Here ... should be a function that returns a emetric_space α instance such that emetric_space.to_topological_space = h is a definitional equality.

view this post on Zulip Jay Williams (Sep 27 2020 at 23:05):

This still doesn't like completion:

import topology.metric_space.basic
import topology.metric_space.completion

open topological_space

instance it_begins {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
begin
  sorry
end

I've tried a few variants, including with some additional stuff in open, but nothing is working... :thinking:

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 23:07):

Let me guess docs#completion.completion

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 23:09):

So, it should be open topological_space uniform_space

view this post on Zulip Jay Williams (Sep 27 2020 at 23:10):

oh geez, I thought I tried that one. Thanks!

view this post on Zulip Jay Williams (Sep 27 2020 at 23:11):

I'm going to have to read up on open, sounds like.

view this post on Zulip Heather Macbeth (Sep 27 2020 at 23:19):

You won't need to read very much. :) When you need a lemma or definition, check the docs (or scroll up in the source) to find the namespace it's in, then open that namespace in your code. Here: docs#uniform_space.completion .

view this post on Zulip Heather Macbeth (Sep 27 2020 at 23:27):

Also, @Jay Williams there's a bad omission in the stub I gave you -- should have been (note the ⟨ ... ⟩)

import topology.bases
import topology.metric_space.completion

open topological_space uniform_space

instance it_begins {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
 begin
    sorry
  end 

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 23:33):

I think that the implication should work for any uniform embedding of uniform spaces (just use the image of a fence sequence)

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 23:35):

Or even for a dense embedding of topological spaces

view this post on Zulip Aaron Anderson (Sep 28 2020 at 03:04):

Is it possible that a complete metric space is equivalent to a complete uniform space?

view this post on Zulip Yury G. Kudryashov (Sep 28 2020 at 03:48):

What exactly do you mean?

view this post on Zulip Aaron Anderson (Sep 28 2020 at 03:59):

So, one of the aspects of a Polish space is the existence of a complete metric that’s compatible with the topology

view this post on Zulip Aaron Anderson (Sep 28 2020 at 04:00):

I went looking for the definition of a complete metric in mathlib, but I only found complete space which is a uniform space definition

view this post on Zulip Aaron Anderson (Sep 28 2020 at 04:00):

I guess I have two questions:

view this post on Zulip Aaron Anderson (Sep 28 2020 at 04:01):

If you have a metric space, is completeness of that metric space equivalent to completeness of the uniform space?

view this post on Zulip Aaron Anderson (Sep 28 2020 at 04:02):

If you have a complete uniform space that doesn’t necessarily come from a metric, does there exist a (not necessarily unique) complete metric inducing the same topology?

view this post on Zulip Aaron Anderson (Sep 28 2020 at 04:03):

(I know some things about basic descriptive set theory, but have yet to study Lean’s topology and analysis libraries, and know little about uniform spaces)

view this post on Zulip Yury G. Kudryashov (Sep 28 2020 at 06:05):

We define completeness in terms of uniform_space structure. Completeness of (e)metric_spaces uses this definition. For a metric space, it is equivalent to the usual definition, see docs#metric.complete_of_cauchy_seq_tendsto and docs#metric.cauchy_seq_iff

view this post on Zulip Yury G. Kudryashov (Sep 28 2020 at 06:07):

Wiki says the following about metrizability: https://en.wikipedia.org/wiki/Nagata%E2%80%93Smirnov_metrization_theorem

view this post on Zulip Patrick Massot (Sep 28 2020 at 07:46):

Some precisions:


Last updated: May 11 2021 at 00:31 UTC