Jay Williams

Stream: new members

[Jay Williams]

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.

[Mario Carneiro]

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

[Mario Carneiro]

Also hello

[Mario Carneiro]

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

[Heather Macbeth]

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.

[Mario Carneiro]

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.)

[Jay Williams]

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.

[Kenny Lau]

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

[Mario Carneiro]

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

[Jay Williams]

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!

[Heather Macbeth]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jay Williams]

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.

[Mario Carneiro]

I suppose immediacy is in the eye of the beholder

[Jay Williams]

As learning Lean is teaching me :)

[Heather Macbeth]

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 )

[Kenny Lau]

instance

[Kenny Lau]

I suppose it is obvious :P

[Heather Macbeth]

Kenny Lau said:

I suppose it is obvious :P

All the better, for a beginner!

[Kenny Lau]

oh, I just meant mathematically

[Kenny Lau]

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

[Mario Carneiro]

which is of course the hard part

[Jay Williams]

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!

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Jay Williams]

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.

[Yury G. Kudryashov]

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

[Jay Williams]

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

[Yury G. Kudryashov]

Possibly it is in the topological_space namespace

[Yury G. Kudryashov]

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

[Jay Williams]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

Try topology/metric_space/completion.

[Jay Williams]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Jay Williams]

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:

[Yury G. Kudryashov]

Let me guess docs#completion.completion

[Yury G. Kudryashov]

So, it should be open topological_space uniform_space

[Jay Williams]

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

[Jay Williams]

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

[Heather Macbeth]

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 .

[Heather Macbeth]

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 ⟩

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Or even for a dense embedding of topological spaces

[Aaron Anderson]

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

[Yury G. Kudryashov]

What exactly do you mean?

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

I guess I have two questions:

[Aaron Anderson]

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

[Aaron Anderson]

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?

[Aaron Anderson]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

Some precisions:

• I think a complete uniform space is not necessarily metrizable, even if it is separated
• We don't have this Nagata-Smirnov theorem, and I don't think anyone is interested in this up to now
• We do have https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/compact_separated.html which is somewhat in the same thread