completion of uniform spaces

Stream: maths

[Patrick Massot]

The perfectoid projects crucially needs completions of topological rings. I can see mathlib already has a lot about completion of uniform spaces but I also remember the definition of real numbers was changed by @Mario Carneiro. Is there anything we should know before doing completions of topological rings?

[Mario Carneiro]

All the material for completion of topological rings via uniform completion is still there. It simply isn't being used to construct the reals anymore, since the direct construction is better in a number of other ways. If you have need for a generic completion operator in a more abstract context, feel free to use it

[Filippo A. E. Nuccio]

In this message @Patrick Massot observes that the way we define completion in mathlib is slightly different from Bourbaki, Topologie Générale, Chap. II, § 3, No. 7. We define the completion as the quotient of Cauchy (the sub-type of the filter defined by being cauchy) by the equivalence relation of being "inseparable"; on the other hand, Bourbaki uses minimal Cauchy filters (that we call ultrafilters, IIUC). Moreover, the embedding $\iota : X \to\hat{X}$ that we use is $x\mapsto \mathcal{P}(x)$, the pure/principal filter, while Bourbaki sends $x$ to the neighborhood filter $\mathcal{N}(x)$. This is also observed in the comments to docs#Cauchy. By universal property, it is clear that the two constructions are isomorphic.

My first two questions are:

1. Why have we chosen this path instead of Bourbaki's (in both cases $\iota$ is injective if and only if $X$ is separated, of course)?
2. What happens if we modify our definition by also using $\mathcal{N}(x)$ instead of $\mathcal{P}(x)$?

My final question is more mathematical. I would like to prove the following: suppose $X$ is separated, $Y$ is separated complete and $f\colon X\to Y$ is uniformly continuous. Let $\mathscr{F}$ be a Cauchy filter in $X$. Then I can produce two elements in $Y$, namely:

1. The limit of $f (\mathscr{F})$: since $f$ is uniformly continuous, it is a Cauchy filter of the complete space $Y$, and it converges to something, say $y_1$.
2. I can first extend $f$ to $\hat{f}\colon \hat{X}\to Y$: concretely, this is defined by taking a Cauchy filter $\mathscr{G}$, taking the inverse image $\iota^{-1}\mathscr{N}(\mathscr{G})$ (which is a filter in $X$) and then taking the limit of this filter along $f$, using that it is uniformly continuous.Applying this to my starting filter, I get $y_2=\hat{f}(\mathscr{F})$.
   I would like to show $y_1=y_2$: I am not 100% sure it is true, but in a nice world it should be, I guess. This would clearly follow if $\iota^{-1}\mathcal{N}(\mathscr{G})=\mathscr{G}$ for all $\mathscr{G}$; is this true? The reason why I asked the second question above is that if I can replace $\mathcal{P}$ by $\mathcal{N}$ in the definition of $\iota$, the proof would seem easier.

[Yaël Dillies]

For 1., I think it's the general fact that quotient are nicer to work with than representatives.

[Filippo A. E. Nuccio]

Well, but this contrasts with the general fact that Bourbaki always makes the best choice :smirk:

[Yaël Dillies]

They certainly didn't make the best choice by not letting ⊥ be a filter!

[Filippo A. E. Nuccio]

That's true...

[Patrick Massot]

This construction is very old, it was done by Johannes at the very beginning. I think the honest answer is he was following the book by James rather than Bourbaki. But one can claim this construction is more general because it does not impose completeness and separatedness in one step, and more natural because looking at all Cauchy filters is the most natural thing to do before noticing you don't get a separated result.

[Patrick Massot]

I'll answer the other questions later, I'm late for a talk.

[Filippo A. E. Nuccio]

I see your point, thanks! And will be waiting for your answer when you have time... :clock:

[Patrick Massot]

@Filippo A. E. Nuccio Sorry I forgot to come back to your question yesterday night. The main answer is you should un-#xy your problem by telling me what you actually want to do. You shouldn't need to think about details of this construction.

About question 2, the answer is we would get the same map after composition by the projection $\pi : C_X \to \hat X$ where $C_X$ is the space of Cauchy filters on $X$.

About the final question, note your notations are a bit confusing because you use an invisible symbol for $\pi$. The answer is still that $y_1 = y_2$ but I don't have a very efficient proof right now, and I suspect we should rather fix your #xy issue than think about an efficient answer.

[Patrick Massot]

And I keep forgetting to say

Bourbaki uses minimal Cauchy filters (that we call ultrafilters, IIUC)

This isn't correct. There is no Cauchy in the ultrafilter story. The set of ultrafilters on $X$ depends on no additional structure on $X$, no uniform structure, not even a topology. Ultrafilters are generalized singletons in the same way filters are generalized sets.

[Oliver Nash]

I never think about ultrafilters but I guess this is true. Is it in Mathlib in some form?

import order.filter.ultrafilter

open_locale filter

instance foo {α : Type*} {s : set α} [nonempty s] : (𝓟 s).ne_bot :=
by rwa [filter.principal_ne_bot_iff, ← set.nonempty_coe_sort]

lemma bar {α : Type*} {s : set α} [nonempty s] :
  ↑(ultrafilter.of $ 𝓟 s) = 𝓟 s ↔ ∃ x, s = {x} :=
sorry

[Filippo A. E. Nuccio]

@Patrick Massot Thanks, it is perhaps true that there is an xy-problem here, but I find the question mathematically interesting per se. At any rate, I will come back and detail you what I am trying to do (Long story short : proving that the Laurent series are isomorphic to the/a completion of rational functions wrt the X-adic topology, I am 85% done but still some bits are left). I really have no time now. Concerning ultrafilters, I meant that "ultrafilters" seem to me to correspond to what Bourbaki calls a "minimal" filter (this definition has nothing to do with topology or Cauchy neither), no?

[Patrick Massot]

They go in opposite directions anyway.

[Anatole Dedecker]

This message by @Junyan Xu feels very related to this discussion (in particular he proves that any cauchy filter tendsto itself in Cauchy \a

[Anatole Dedecker]

Indeed what Bourbaki calls "minimal" is "maximal" for our order. Besides, I think "minimal Cauchy filter" really means "minimal among Cauchy filters", not merely a minimal filter which is Cauchy.

[Jireh Loreaux]

@Oliver Nash What you are looking for is closely related to docs#filter.ne_bot.le_pure_iff and docs#ultrafilter.of_coe, but it doesn't seem like we have the precise statement you mentioned (unless I'm missing it).

[Oliver Nash]

Thanks. On reflection I guess docs#ultrafilter.of is more of an implementation tool rather than something around which we need a substantial API so I’m not surprised we don’t have this.

[Patrick Massot]

Anatole is right that my previous message was probably a bit too allusive. It doesn't help that Bourbaki uses the wrong order relation on filters in this discussion. As usual, understanding the intuition is easier than tracking ordering conventions.

An ultrafilter is meant to be a generalized singleton. So, using the ordering ensuring that the "inclusion" of set X into filter X is order preserving, an ultrafilter is minimal among "non-empty" filters, where non-empty means not the image of the empty set under this inclusion, just as ordinary singletons are minimal among non-empty elements of set X.

Now assume X has a uniform structure, aka equipped with a generalized set 𝓤 X : filter (X × X) of pairs of points that are close to each other. A filter F is Cauchy if it is non-empty and F × F ≤ 𝓤 X, that is every two points "in" F are close to each other. That notion is obviously monotone, ie if G is non-empty and "contained" in F which is Cauchy then G is Cauchy. So certainly the only meaningful maximality or minimality condition to consider on Cauchy filter is being maximal among Cauchy filters.

This intuition makes it obvious that {x} is Cauchy (it isn't empty and any two points in {x} are close to each other). And 𝓝 x is also Cauchy since it isn't empty and any two points that are close to x are close to each other (of course checking this intuition is correct requires the complete definition of uniform_space and the associated topology). And certainly {x} is not maximal unless x is isolated since {x} ≤ 𝓝 x because x is close to itself.