Elements of completion as limits

Stream: Is there code for X?

[Adam Topaz]

Do we know that elements of the completion of a uniform space $X$ can be represented as limits of Cauchy filters on $X$?

[Junyan Xu]

This is my formalization and proof of the result:

import topology.uniform_space.completion

variables {α : Type*} [uniform_space α]

lemma Cauchy_tendsto_nhds_self (F : Cauchy α) : F.1.tendsto Cauchy.pure_cauchy (nhds F) :=
begin
  rw uniform.tendsto_nhds_left,
  intros s hs,
  obtain ⟨t, ht, hts⟩ := Cauchy.mem_uniformity'.1 hs,
  obtain ⟨r, hr, hrt⟩ := (cauchy_iff'.1 F.2).2 t ht,
  rw filter.mem_map_iff_exists_image,
  use [r, hr],
  rw set.image_subset_iff,
  intros x hx, apply hts,
  rw filter.mem_prod_iff,
  use [r, hx, r, hr],
  rintro ⟨x, y⟩ ⟨hx, hy⟩,
  exact hrt x hx y hy,
end

lemma exists_cauchy (x : uniform_space.completion α) :
  ∃ F : filter α, cauchy F ∧ F.tendsto coe (nhds x) :=
begin
  rcases x, use [x.1, x.2],
  rw uniform_space.completion.coe_eq,
  erw ← inducing.tendsto_nhds_iff,
  { apply Cauchy_tendsto_nhds_self },
  { exact uniform_inducing.inducing ⟨uniform_space.comap_quotient_eq_uniformity⟩ },
end

I feel I don't really understand it, but I was able to complete the proofs!

[Adam Topaz]

Nice! That's roughly the proof I had, but I would be surprised if there wasn't a lemma in mathlib that makes this a one-liner.

[Anatole Dedecker]

I'm not sure at all I can do better, but I feel like there has to be a nicer proof involving docs#dense_inducing or things like that

[Anatole Dedecker]

Let me give it a try

[Anatole Dedecker]

Indeed

[Anatole Dedecker]

import topology.uniform_space.completion

open filter uniform_space
open_locale topological_space

variables {α : Type*} [uniform_space α]

lemma exists_cauchy (x : completion α) :
  ∃ F : filter α, cauchy F ∧ tendsto coe F (𝓝 x) :=
begin
  refine ⟨comap coe (𝓝 x), cauchy_nhds.comap' _
    (completion.dense_inducing_coe.comap_nhds_ne_bot x), tendsto_comap⟩,
  rw (completion.uniform_inducing_coe α).comap_uniformity,
  exact le_rfl
end

[Anatole Dedecker]

Junyan Xu said:

This is my formalization and proof of the result:

import topology.uniform_space.completion

variables {α : Type*} [uniform_space α]

lemma Cauchy_tendsto_nhds_self (F : Cauchy α) : F.1.tendsto Cauchy.pure_cauchy (nhds F) :=
begin
  rw uniform.tendsto_nhds_left,
  intros s hs,
  obtain ⟨t, ht, hts⟩ := Cauchy.mem_uniformity'.1 hs,
  obtain ⟨r, hr, hrt⟩ := (cauchy_iff'.1 F.2).2 t ht,
  rw filter.mem_map_iff_exists_image,
  use [r, hr],
  rw set.image_subset_iff,
  intros x hx, apply hts,
  rw filter.mem_prod_iff,
  use [r, hx, r, hr],
  rintro ⟨x, y⟩ ⟨hx, hy⟩,
  exact hrt x hx y hy,
end

lemma exists_cauchy (x : uniform_space.completion α) :
  ∃ F : filter α, cauchy F ∧ F.tendsto coe (nhds x) :=
begin
  rcases x, use [x.1, x.2],
  rw uniform_space.completion.coe_eq,
  erw ← inducing.tendsto_nhds_iff,
  { apply Cauchy_tendsto_nhds_self },
  { exact uniform_inducing.inducing ⟨uniform_space.comap_quotient_eq_uniformity⟩ },
end

I feel I don't really understand it, but I was able to complete the proofs!

Sorry, I could have saved you a lot of trouble :sweat_smile:

[Anatole Dedecker]

This is really a lemma about docs#uniform_inducing s with dense range

[Anatole Dedecker]

I don't even use the fact that the completion is complete x)

[Junyan Xu]

Very nice proof! Can be compactified to

lemma exists_cauchy (x : completion α) :
  ∃ F : filter α, cauchy F ∧ tendsto coe F (𝓝 x) :=
⟨comap coe (𝓝 x), cauchy_nhds.comap'
  (completion.uniform_inducing_coe α).comap_uniformity.le
  (completion.dense_inducing_coe.comap_nhds_ne_bot x), tendsto_comap⟩

[Anatole Dedecker]

Nice, I feel better now that you golfed me back :stuck_out_tongue_wink:

[Junyan Xu]

Your proof shows every point x in the completion is the limit at the preferred Cauchy filter comap coe (𝓝 x), which is interesting, as my proof shows that any Cauchy filter in the class of x has x as the limit.

[Anatole Dedecker]

I think the philosophy for such constructions which have a nice universal property is to forbid yourself to unfold the constructions, so somehow we don't want to make sense of "filters in the class of x"

[Anatole Dedecker]

But I agree that your approach feels natural

[Junyan Xu]

I wonder if this result also has a short proof ...

lemma forall_cauchy (x : uniform_space.completion α) :
  ∀ F : Cauchy α, x = quotient.mk' F → F.1.tendsto coe (nhds x) :=
begin
  rintro F rfl,
  rw uniform_space.completion.coe_eq,
  erw ← inducing.tendsto_nhds_iff,
  { apply Cauchy_tendsto_nhds_self },
  { exact uniform_inducing.inducing ⟨uniform_space.comap_quotient_eq_uniformity⟩ },
end

[Junyan Xu]

of course this only makes sense for completion not docs#abstract_completion ...

[Anatole Dedecker]

I don't see a more clever way than proving first

lemma Cauchy.tendsto_nhds_self {α : Type*} [uniform_space α] (F : Cauchy α) :
  tendsto (λ (x : α), Cauchy.pure_cauchy x) F.val (𝓝 F) :=
begin
  sorry,
end

and then

lemma forall_cauchy (x : uniform_space.completion α) :
  ∀ F : Cauchy α, x = quotient.mk' F → F.1.tendsto coe (nhds x) :=
begin
  rintro F rfl,
  exact (continuous_quotient_mk.tendsto _).comp F.tendsto_nhds_self
end

[Anatole Dedecker]

And I don't think the first sorry can be solved without using filter bases and so on

[Junyan Xu]

I also can't find the following lemma in mathlib; is there a simpler proof?

lemma separation_setoid_eq_inseparable_setoid {α} [uniform_space α] :
  uniform_space.separation_setoid α = inseparable_setoid α :=
begin
  ext, change (a,b) ∈ separation_rel α ↔ inseparable a b,
  rw inseparable_iff_forall_open,
  split; intro h,
  { intros s hs, suffices : _,
    { split, revert a b h,
      exacts [this, this _ _ $ (uniform_space.separation_setoid α).symm' h] },
    { clear h a b, exact λ a b h ha, h _ (is_open_uniformity.1 hs a ha) rfl } },
  { rw uniformity_has_basis_open.mem_separation_rel,
    intros s hs,
    refine (h {x | (a, x) ∈ s} _).1 (refl_mem_uniformity hs.1),
    exact (continuous.prod.mk a).is_open_preimage _ hs.2 },
end

[Patrick Massot]

It's nice that you can train student and then send them do internship across the Atlantic so that they can answer questions for you when you sleep. I still tried to get to the bottom of this and found a couple of surprising holes (as usual). I suggest adding:

import topology.uniform_space.completion

open filter set
open_locale topological_space

lemma function.surjective.comap_ne_bot_iff_ne_bot {α β : Type*} {f : α → β}
  (hf : function.surjective f) (F : filter β) : (comap f F).ne_bot ↔ F.ne_bot :=
⟨λ h, ⟨λ H, (H ▸ h : (comap f ⊥).ne_bot).ne comap_bot⟩, λ h, h.comap_of_surj hf⟩

open filter set

lemma mem_closure_range_iff_comap {α : Type*} {β : Type*} [topological_space β]
  {f : α → β} {b : β} : b ∈ closure (range f) ↔ (comap f (𝓝 b)).ne_bot :=
begin
  rw [mem_closure_iff_comap_ne_bot],
  conv_rhs { rw [← coe_comp_range_factorization f, ← filter.comap_comap,
                 surjective_onto_range.comap_ne_bot_iff_ne_bot] }
end

-- Not used below but nice to have.
lemma dense_range.comap_nhds_ne_bot {α : Type*} {β : Type*} [topological_space β]
  {f : α → β} (h : dense_range f) (b : β) : (comap f (𝓝 b)).ne_bot :=
mem_closure_range_iff_comap.mp (h b)

variables {α : Type*} [uniform_space α]

open uniform_space
open_locale uniformity

lemma exists_cauchy_tendsto {β : Type*} [uniform_space β]
  {f : α → β} (hf : comap (prod.map f f) (𝓤 β) ≤ 𝓤 α) {x} (hx : x ∈ closure (range f)) :
∃ F : filter α, cauchy F ∧ tendsto f F (𝓝 x) :=
⟨comap f (𝓝 x), cauchy_nhds.comap' hf (mem_closure_range_iff_comap.mp hx), tendsto_comap⟩

open uniform_space.completion

lemma uniform_space.completion.exists_cauchy_tendsto (x : completion α) :
  ∃ F : filter α, cauchy F ∧ tendsto coe F (𝓝 x) :=
exists_cauchy_tendsto (uniform_inducing_coe α).comap_uniformity.le (dense_range_coe x)

[Junyan Xu]

(deleted)

[Junyan Xu]

So I was able to prove a characterization of the backward map from completion α to Cauchy α constructed by Anatole. The code is at https://gist.github.com/alreadydone/9fcfb78af6cd48bdedf3220a598b8321, where the map is called preferred_cauchy. It turns out it's a right inverse to the "separation quotient" map that produces completion α from Cauchy α. Moreover, it sends a point x in the completion to the unique maximal Cauchy filter F that tends to x under α → completion α; as it turns out, F tends to x iff it maps to x under the quotient map. This was rather mysterious to me, as points in Cauchy α that maps to the same point in completion α are by definition topologically indistinguishable, but it makes sense when you think about Cauchy α as filters on the original space α instead of a space by itself, so everything still makes sense when considering abstract_completion, which doesn't mention an intermediate space.

To understand this better I worked out an example: consider the uniformity ⊤ = {univ} on the two point set α = {0, 1}, which induces the trivial topology; every ne_bot filter on this space is Cauchy, and there are three of them: ⊤={univ}, 𝓟 {0}, and 𝓟 {1}. Of course the map α → completion α sends x to 𝓟 {x}, while ⊤ is not in the image. The separation quotient consists of exactly one point, and preferred_cauchy maps it to ⊤.