embedding into completion

Stream: new members

[Jay Williams]

I'm trying to start proving something simple, and I've settled on showing that the completion of a separable space is separable. So far I have this (which was mostly given to me in my introduction thread, thanks!):

import topology.bases
import topology.metric_space.completion

open topological_space uniform_space

instance completion_of_separable_is_separable {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
⟨ begin
    let a := _inst_1.to_uniform_space,

    let f := Cauchy.pure_cauchy X,
  end ⟩

and at this point I get

failed to synthesize type class instance for
X : Type ?,
_inst_1 : metric_space X,
_inst_2 : separable_space X,
a : uniform_space X := metric_space.to_uniform_space
⊢ uniform_space (Type ?)
state:
X : Type ?,
_inst_1 : metric_space X,
_inst_2 : separable_space X,
a : uniform_space X := metric_space.to_uniform_space
⊢ ∃ (s : set (completion X)), s.countable ∧ closure s = set.univ

Basically, I'm trying to get a hold of the embedding from X into completion X and I'm getting an error. I'm a bit confused why it's having trouble synthesizing uniform_space (Type ?) when it has X : Type ? and uniform_space X, which seems to me like it should be enough. Does anyone know what is going on here? Is there some other better way for me to work with the embedding from X into completion X?

[Kevin Buzzard]

I don't know if what you're doing is the right way to do it, but I can tell you why you're getting the error: let puts your valuable into the local context (so you can use it) but it doesn't tell it to the type class inference system (the system which is handling all the square bracket stuff). Changing let to letI should put the uniform space instance into the system and then things will work. But I'm not sure that this is what you want to do. Is there more than one completion? Do you really want to use uniform space completion?

[Jay Williams]

Those are great questions! I find the completion stuff a bit confusing honestly. I'd prefer to use the metric space completion, but I couldn't figure out how to get at the embedding with the stuff in metric_space/completion.lean. I also think I'm going to want to use the dense_embedding_coe lemma in uniform_space/completion.lean. So it seemed to me like I was going to need to treat X like a uniform space at some point, since the existence of that embedding and that lemma are both formulated for uniform spaces.

Here's how the proof I want to write goes:
X is separable, so it has a countable dense subset S.
There is an (isometric) embedding of X into completion X, and the image of X is dense in completion X.
It follows that the image of S under the embedding is dense in completion X.

So I really would like to use the embedding. I'm very open to learning a better way to get at it.

[Jay Williams]

I mean, writing it out it seems like I could probably just formulate this _for_ uniform spaces...

[Jay Williams]

But I'm still curious about the "right" way to do this for metric spaces. :)

[Reid Barton]

⊢ uniform_space (Type ?) means Lean is looking for a uniform_space instance on Type itself, which in turn means you probably passed the wrong argument to something.

[Jay Williams]

I think I understand now that Kevin was getting at there being a difference between Cauchy X and completion X, so Cauchy.pure_cauchy isn't really appropriate to use when dealing with completion X. That said, I still don't know how to get at the embedding when restricting to looking at completion-related lemmas. Several of them make reference to coe, but this is very mysterious to me, as coe appears to be something in the core of mathlib, as opposed to something that is specifically relating a space to its completion.

[Jay Williams]

Maybe put a little differently, Cauchy.pure_cauchy has as its documentation "Embedding of α into its completion", but there is nothing else that says that among all the things for completions, so I'm at a bit more of a loss there.

[Heather Macbeth]

@Jay Williams Indeed this coe is something general, but what you probably need is the definition of how coe works from a metric space to its completion. Start reading at
docs#uniform_space.completion.has_coe_t
If it's still puzzling, let me know and I'll take a more careful look.

[Jay Williams]

I'm getting there, but that specific pointer is helpful, thanks. Now I have

import topology.bases
import topology.metric_space.completion

open topological_space uniform_space

instance completion_of_separable_is_separable {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
⟨ begin
    let φ := completion.coe_eq (completion X),

    rcases _inst_2.exists_countable_closure_eq_univ with ⟨ S, hc, hd ⟩,
  end ⟩

and realize that I don't know how to talk about the image of a set under φ. But that's probably something for a different question... :smile:

[Heather Macbeth]

Letting s denote the set, the image is denoted by φ '' s! And if you ever need the preimage, that's φ ⁻¹' s.

[Jay Williams]

Ah I'm still doing something wrong because φ as I have it up there has type Prop (it's a proof of an equality), not a function from X to completion X. So I'll take a closer look at has_coe_t.

[Heather Macbeth]

You can probably do let φ : X → completion X := coe.

(In fact later it will probably be possible to rewrite so this map is nearly silent, but I think it's sensible to make it explicit, as you have done, for now.)

[Jay Williams]

Hmm yes, that works. I find this whole coe business very mysterious! But I think I'll set that aside for now and focus on trying to finish up the proof. Thanks!

[Patrick Massot]

Jay, you are having a lot of difficulties here, both from the maths side and the Lean side. The main issue is math, you are concentrating on completely irrelevant points. I need to run but I'll add details later. Here is the Lean code:

import topology.bases
import topology.metric_space.completion

open topological_space uniform_space set

lemma exists_countable_closure_eq_univ (X : Type*) [topological_space X] [separable_space X] :
  ∃ s : set X, countable s ∧ closure s = univ :=
separable_space.exists_countable_closure_eq_univ

lemma separable_of_dense_range {X Y : Type*} [topological_space X] [separable_space X] [topological_space Y] {f :X → Y}
  (h : dense_range f) (h' : continuous f) : separable_space Y :=
let ⟨s, s_count, s_clos⟩ := exists_countable_closure_eq_univ X in
⟨⟨f '' s, countable.image s_count f, begin
  have : f '' (closure s) ⊆ closure (f '' s) := image_closure_subset_closure_image h',
  have := closure_mono this,
  rw [s_clos, image_univ, h.closure_range, closure_closure] at this,
  exact eq_univ_of_univ_subset this,
end⟩⟩

lemma dense_embedding.separable {X Y : Type*} [topological_space X] [separable_space X] [topological_space Y] {f :X → Y}
  (h : dense_embedding f) : separable_space Y :=
separable_of_dense_range h.dense h.to_dense_inducing.continuous

instance completion_of_separable_is_separable {X : Type*} [metric_space X] [separable_space X] :
  separable_space (completion X) :=
completion.dense_embedding_coe.separable

Only the last declaration involves metric spaces (and it can of course be replaced with uniform spaces if you add the relevant assumptions that are automatic for metric spaces).

[Patrick Massot]

I'm back with a bit more time. The main issue is mathematical. The key is to focus on the heart of the result, dismissing irrelevant bits. This is true in the real world of course, but it's much more important in formalized mathematics since every irrelevant bit of context has to be carried around in fully detailed form. So you need to first forget about metric spaces and realize that the key fact is separable_of_dense_range above.

Then comes the first technological issue. We haven't done much with separable spaces except in the integration theory folder and the API is still bad. In particular the binders in separable_space.exists_countable_closure_eq_univ are stupid, the space should be explicit. That's why I wrote exists_countable_closure_eq_univ. Then the lemma is easy to prove, but one should probably extract one more lemma, I'm pretty sure I'm duplicating an existing proof.

[Patrick Massot]

Here is a better version

import topology.bases
import topology.metric_space.completion

open topological_space uniform_space set

section

lemma exists_countable_closure_eq_univ (X : Type*) [topological_space X] [separable_space X] :
  ∃ s : set X, countable s ∧ closure s = univ :=
separable_space.exists_countable_closure_eq_univ

variables {X Y : Type*} [topological_space X] [topological_space Y] {f :X → Y}

lemma continuous.closure_image_eq_univ_of_dense_range
  (hf : continuous f) (hf' : dense_range f) {s : set X} (hs : closure s = univ) :
  closure (f '' s) = univ :=
begin
  have : f '' (closure s) ⊆ closure (f '' s) := image_closure_subset_closure_image hf,
  have := closure_mono this,
  rw [hs, image_univ, hf'.closure_range, closure_closure] at this,
  exact eq_univ_of_univ_subset this
end

variables [separable_space X]

lemma separable_of_dense_range (h : dense_range f) (h' : continuous f) : separable_space Y :=
let ⟨s, s_count, s_clos⟩ := exists_countable_closure_eq_univ X in
⟨⟨f '' s, countable.image s_count f, h'.closure_image_eq_univ_of_dense_range h s_clos⟩⟩

lemma dense_inducing.separable (h : dense_inducing f) : separable_space Y :=
separable_of_dense_range h.dense h.continuous

lemma dense_embedding.separable (h : dense_embedding f) : separable_space Y :=
h.to_dense_inducing.separable

end

instance separable_space_completion {X : Type*} [uniform_space X] [separable_space X] :
  separable_space (completion X) :=
completion.dense_inducing_coe.separable

[Patrick Massot]

Note how focusing of the key content completely bypasses the question of how to speak about the map from X to its completion.

[Patrick Massot]

You should still learn about coercions, by reading the relevant section of TPIL (you may need need to backtrack at least to the beginning of Chapter 10).

[Patrick Massot]

Ouch, the module docstring of uniform_space.completion has several annoying typos.

[Yury G. Kudryashov]

We have docs#topological_space.dense_seq

[Patrick Massot]

I know, I wrote it pretty recently. But this assumes a non-empty space.

[Patrick Massot]

I opened #4399

[Yury G. Kudryashov]

I always forget about empty types.

[Patrick Massot]

But Lean doesn't forget.

[Patrick Massot]

I just commented on the PR.

[Patrick Massot]

OMG, someone put dense in the root namespace to mean something else than dense.

[Patrick Massot]

And then he ran away to Apple.

[Patrick Massot]

Is there anyone who doesn't want docs#dense to be renamed to exists_between?

[Jay Williams]

Patrick Massot said:

Jay, you are having a lot of difficulties here, both from the maths side and the Lean side. The main issue is math, you are concentrating on completely irrelevant points. I need to run but I'll add details later. Here is the Lean code:

I just want to say that frankly I did not find this comment very helpful at all. I know I'm having difficulties, it's why I came to the "new members" stream and said multiple times that I was having difficulties.

I gave a three sentence proof of the result that uses the embedding, so no, I don't think I'm particularly confused on the math side, though honestly I don't work as a mathematician anymore, so I expect to be rusty about a lot of things. I am not surprised that one can think about things in a different way that avoids explicitly relying on the embedding. I feel certain I would have gotten there eventually, but I'm trying to first figure out how to do the things I want to do in Lean, and then learn (probably in a PR review) better ways of doing things. A month or so ago I didn't know anything about using Lean at all!

You should still learn about coercions, by reading the relevant section of TPIL (you may need need to backtrack at least to the beginning of Chapter 10).

Thank you, this is actually helpful.

I think you should really reconsider how you interact with new members, because this was incredibly discouraging to come back to, and makes me not want to contribute. I was asking for help, not asking for someone to do this for me. And I felt talked down to not just on a Lean level, but on a mathematical level.

[Patrick Massot]

I'm really sorry, I wrote that very quickly because I wanted to help and had only ten minutes.

[Patrick Massot]

Then I returned and tried to add a lot of details.

[Patrick Massot]

And I can see it wasn't clear enough.

[Patrick Massot]

Of course the proof uses the embedding (which is not an embedding in general, but it certainly is in the metric space case). What I wanted to explain was that you don't need so much information on either the spaces or the map (in particular injectivity plays no role at all).

[Patrick Massot]

And, on the Lean side, you don't need to know that this map is a setup as a coercion.

[Patrick Massot]

But again I'm really sorry. I wanted to paste only the statements of the lemmas with a couple of Lean hints but I was already late, so I pasted the whole code.

[Jay Williams]

I appreciate the apology.

That said, what was upsetting was less that the proof was done for me, but the way it was presented. I know to look for ways to weaken hypotheses, I just wanted to do that after I had a working proof of the result I was looking at. Of course injectivity is not necessary, since all I need is that the dense subset in the completion is countable. I take your point that by focusing on the canonical embedding I perhaps was not looking for more general lemmas that would help, but what you actually said was that I was "concentrating on completely irrelevant points". You said "The main issue is mathematical." as though the short pen-and-paper proof I gave was somehow wrong. It made me feel pretty bad.

[Patrick Massot]

I can see this was potentially upsetting, and I'm sorry. But one important piece was the sentence about what is specific to formalized mathematics. We are very good at pretending to speak about a specific situation but actually focusing on some abstract feature. Proof assistant are less good here, so you need to help them by going abstract as early as possible.

[Jay Williams]

Thank you, that is good advice.

[Patrick Massot]

We can still try to write the proof in the special case if you want.

[Jay Williams]

No thanks, this is fine. I am going to study this one a bit, see how it works, and then think of the next thing I want to try to prove. I'll let you know if I have more questions. :smile: