Zulip Chat Archive

Stream: maths

Topic: Hausdorff completion


view this post on Zulip Patrick Massot (Jul 11 2018 at 09:49):

@Johannes Hölzl around https://github.com/leanprover/mathlib/blob/master/analysis/topology/uniform_space.lean#L1102, is there any reason why you didn't push to the Hausdorff completion? Is the idea that users should easily combine stuff in this section with the https://github.com/leanprover/mathlib/blob/master/analysis/topology/uniform_space.lean#L928 section? Or did you intend to continue this?

view this post on Zulip Johannes Hölzl (Jul 11 2018 at 10:36):

The idea was to be compositional. So I wanted to split the separation quotient from the Cauchy construction. I'm not exactly sure what Hausdorff completion is, but I guess you can use the composition hausdorff_completion α := quotient (separation_setoid (Cauchy α)). Or do I miss something?

view this post on Zulip Patrick Massot (Jul 11 2018 at 10:41):

Yes, this is what I had in mind.

view this post on Zulip Patrick Massot (Jul 11 2018 at 10:41):

Or maybe compose in the opposite order, I would need to think whether it's the same

view this post on Zulip Patrick Massot (Jul 11 2018 at 10:45):

Bourbaki does it a bit differently. They consider the space of minimal Cauchy filters.. It seems this is always Hausdorff

view this post on Zulip Patrick Massot (Jul 11 2018 at 11:04):

I found some text claiming that your definition of hausdorff_completion α gives the same result as the minimal Cauchy filter definition. Anyway, the real test is to try to prove the universal property for this definition (every uniformly continuous map from α into a complete Hausdorff space factors through the, not necessarily injective, "inclusion" of α in hausdorff_completion α)

view this post on Zulip Johannes Hölzl (Jul 11 2018 at 16:00):

I didn't choose to use minimal Cauchy filters, as I thought the splitting into (all) Cauchy filters and quotient makes the formalization easier. And the separation quotient will be used anyway. The universal property is proved for each dense embedding from a closed set on a complete space (see section uniform_extension)

view this post on Zulip Patrick Massot (Jul 11 2018 at 16:18):

I understand. I have a stub at https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean that I'll try to complete. I think I understand what's already in mathlib and what remains to be done. Then next step would be to unsorry the end of https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/topological_structures.lean

view this post on Zulip Johannes Hölzl (Jul 11 2018 at 20:19):

All this was already done for the real numbers, if you want I can look it up in the mathlib history

view this post on Zulip Patrick Massot (Jul 11 2018 at 20:20):

Any help is welcome

view this post on Zulip Patrick Massot (Jul 11 2018 at 20:20):

But there is no separation issue in the real case

view this post on Zulip Patrick Massot (Jul 11 2018 at 20:23):

By the way, is https://github.com/leanprover/mathlib/blob/master/analysis/topology/uniform_space.lean#L18 still true?

view this post on Zulip Johannes Hölzl (Jul 11 2018 at 20:31):

No, its not true anymore.
As far as I remember, there is a separation issue for the real case: I used the separation/Cauchy construction: https://github.com/leanprover/mathlib/blob/7fd7ea8c323c5f622bda6bc8de6dd352cc2732a8/analysis/real.lean#L384

view this post on Zulip Patrick Massot (Jul 11 2018 at 20:41):

Thanks. This will probably be very useful when I'll move to completions of groups and rings. But I don't see anything that looks like the universal property of Hausdorff completions

view this post on Zulip Patrick Massot (Jul 11 2018 at 20:42):

I'm really curious to know why the separation quotient was necessary. I have no intuition about filters, but to me rationals numbers seems separated enough.

view this post on Zulip Johannes Hölzl (Jul 11 2018 at 20:59):

But the _Cauchy filters over the rationals_ are not separated. In this regard is no difference between Cauchy sequences and filters. One also needs to put a quotient over the Cauchy sequences when constructing the reals via Cauchy sequences.

view this post on Zulip Patrick Massot (Jul 11 2018 at 21:07):

Indeed

view this post on Zulip Patrick Massot (Jul 15 2018 at 10:29):

Now I know what I meant. The fundamental difference is that the map of_rat ℚ → ℝ is injective. Then you proved it's a uniform embedding, and used lemmas about uniform embeddings everywhere. This is no longer true in my context.

view this post on Zulip Johannes Hölzl (Jul 15 2018 at 12:11):

So instead of injective your function respects the separability relation?

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:29):

It's uniformly continuous, hence respects the separability relation (this is the first lemma in the other uniformity thread).

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:30):

Anyway, I now have the universal mapping property for Hausdorff completion: https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L40-L41 It also uses Chris' proof at https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/quotient.lean

view this post on Zulip Johan Commelin (Oct 15 2018 at 17:45):

Uniform spaces have Hausdorff completions https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/completion.lean#L535. More precisely, there is a completion functor which is left-adjoint to the inclusion of complete Hausdorff spaces into all uniform spaces. (Quoted from here.)

@Patrick Massot When you say "functor" and "left-adjoint" are you actually using category-theoretical machinery? Or do you mean that all the ingredients are there, and that what's left is that we just need to write the abstract nonsense boilerplate?

view this post on Zulip Patrick Massot (Oct 15 2018 at 17:47):

Adjunctions are not yet in mathlib, so I mean all the ingredients are there

view this post on Zulip Patrick Massot (Oct 15 2018 at 17:50):

There is a map from a uniform space to its completion: https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/topological_groups.lean#L27 (it's called coe because it is setup as a coercion in Lean sense). Maps into a completed Hausdorff space factor through the completion: https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/completion.lean#L651 This is used to build the action of the completion functor on arrows: https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/completion.lean#L670 this is functorial https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/completion.lean#L700 etc. etc. (I'm skipping a lot. I think everything is there)


Last updated: May 09 2021 at 09:11 UTC