union of complete sets

Stream: maths

[Sebastien Gouezel]

For our uniform space experts (yes, @Patrick Massot , I'm thinking of you :-). I can't find in the library the fact that the union of two complete sets is complete. I'm not even sure this is correct in full generality (i.e., without any separation assumption), but I don't have an easy counterexample either, so I'd be interested in comments in one direction or the other.

[Kevin Buzzard]

It's a great question!

[Riccardo Brasca]

For metric spaces it is easy, isn't it? If $(x_n)_n$ is a Cauchy sequence contained in $S \cup T$, then there is a subsequence contained in $S$ (or in $T$), that is convergent, and then the original sequence is convergent. Am I missing something obvious or is a more general notion of completeness?

[Patrick Massot]

It's a more general notion

[Patrick Massot]

I'm not sure whether the general statement is true.

[Kevin Buzzard]

It's docs#is_complete

[Kevin Buzzard]

(root namespace -- wow!)

[Patrick Massot]

It's a bit too late to think about exotic uniform spaces.

[Riccardo Brasca]

I am reading it, but I still have problems with uniform spaces...

[Kevin Buzzard]

If s and t are complete, and f is a Cauchy filter with s union t in f, then we can't conclude s is in f or t is in f as far as I know (Cauchy doesn't imply this, does it?), so somehow this is where Riccardo's proof breaks down.

[Adam Topaz]

If you could state completeness with ultrafilters, then you could make such a conclusion.

[Sebastien Gouezel]

Here is my current state.

lemma is_complete.union {s t : set α} (hs : is_complete s) (ht : is_complete t) :
  is_complete (s ∪ t) :=
begin
  assume f f_cauchy hf,
  let fs := f ⊓ 𝓟 s,
  let ft := f ⊓ 𝓟 t,
  have fst : fs ⊔ ft = f, by simpa [fs, ft, ← inf_sup_left, sup_principal] using hf,
  rcases eq_or_ne fs ⊥ with h|h,
  { rw [h, bot_sup_eq] at fst,
    rw ← fst at f_cauchy,
    obtain ⟨x, xt, hx⟩ : ∃ (x : α) (H : x ∈ t), ft ≤ 𝓝 x := ht ft f_cauchy inf_le_right,
    exact ⟨x, mem_union_right _ xt, by rwa fst at hx⟩ },
  rcases eq_or_ne ft ⊥ with h'|h',
  { rw [h', sup_bot_eq] at fst,
    rw ← fst at f_cauchy,
    obtain ⟨x, xs, hx⟩ : ∃ (x : α) (H : x ∈ s), fs ≤ 𝓝 x := hs fs f_cauchy inf_le_right,
    exact ⟨x, mem_union_left _ xs, by rwa fst at hx⟩ },
  obtain ⟨x, xs, hx⟩ : ∃ (x : α) (H : x ∈ s), fs ≤ 𝓝 x :=
    hs fs (f_cauchy.mono' ⟨h⟩ inf_le_left) inf_le_right,
  obtain ⟨y, yt, hy⟩ : ∃ (y : α) (H : y ∈ t), ft ≤ 𝓝 y :=
    ht ft (f_cauchy.mono' ⟨h'⟩ inf_le_left) inf_le_right,
  suffices H : 𝓝 x = 𝓝 y,
  { rw ← H at hy,
    refine ⟨x, mem_union_left _ xs, _⟩,
    rw ← fst,
    exact sup_le hx hy },
  sorry
end

(Since I don't know anything about this stuff, having Lean double-check everything helps a lot). I start from a Cauchy filter on s ∪ t, and then I restrict it to s and to t. If one of the restrictions is trivial, then the original filter lives on the other set, and I'm done. Otherwise, each restricted filter is Cauchy, so it has a limit (called x and y above). If I can prove that the neighborhoods of x and of y are the same, then I can conclude the proof. (Of course, x and y don't need to be the same, as limits are typically not unique). And hopefully this should be true, as these two points are approximated by a Cauchy filter, so they should be infinitely close...

[Yury G. Kudryashov]

Probably you can reformulate the definition using ultrafilters. Then the proof is trivial

[Patrick Massot]

lemma is_complete.union {s t : set α} (hs : is_complete s) (ht : is_complete t) :
  is_complete (s ∪ t) :=
begin
  assume f f_cauchy hf,
  let fs := f ⊓ 𝓟 s,
  let ft := f ⊓ 𝓟 t,
  have fst : fs ⊔ ft = f, by simpa [fs, ft, ← inf_sup_left, sup_principal] using hf,
  rcases eq_or_ne fs ⊥ with h|h,
  { rw [h, bot_sup_eq] at fst,
    rw ← fst at f_cauchy,
    obtain ⟨x, xt, hx⟩ : ∃ (x : α) (H : x ∈ t), ft ≤ 𝓝 x := ht ft f_cauchy inf_le_right,
    exact ⟨x, mem_union_right _ xt, by rwa fst at hx⟩ },
  obtain ⟨x, xs, hx⟩ : ∃ (x : α) (H : x ∈ s), fs ≤ 𝓝 x :=
    hs fs (f_cauchy.mono' ⟨h⟩ inf_le_left) inf_le_right,
  use [x, or.inl xs],
  apply le_nhds_of_cauchy_adhp f_cauchy,
  rw [← fst, cluster_pt, inf_sup_left, sup_ne_bot],
  left,
  rw inf_of_le_right hx,
  exact ⟨h⟩
end

I can go to bed knowing my reputation is safe.

[Yury G. Kudryashov]

Il try to write a proof with ultrafilters tonight

[Yury G. Kudryashov]

Probably I'm wrong.

[Yury G. Kudryashov]

No, I'm not.

lemma cauchy.to_ultrafilter {l : filter α} (h : cauchy l) :
  cauchy (@ultrafilter.of _ l h.1 : filter α) :=
begin
  haveI := h.1,
  have := ultrafilter.of_le l,
  exact ⟨ultrafilter.ne_bot _, (filter.prod_mono this this).trans h.2⟩
end

lemma is_complete_iff_cluster_pt {s : set α} :
  is_complete s ↔ ∀ l, cauchy l → l ≤ 𝓟 s → ∃ x ∈ s, cluster_pt x l :=
forall₃_congr $ λ l hl hls, exists₂_congr $ λ x hx, le_nhds_iff_adhp_of_cauchy hl

lemma is_complete_iff_ultrafilter {s : set α} :
  is_complete s ↔ ∀ l : ultrafilter α, cauchy (l : filter α) → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x :=
begin
  refine ⟨λ h l, h l, λ H, is_complete_iff_cluster_pt.2 $ λ l hl hls, _⟩,
  haveI := hl.1,
  rcases H (ultrafilter.of l) hl.to_ultrafilter ((ultrafilter.of_le l).trans hls)
    with ⟨x, hxs, hxl⟩,
  exact ⟨x, hxs, (cluster_pt.of_le_nhds hxl).mono (ultrafilter.of_le l)⟩
end

lemma is_complete_iff_ultrafilter' {s : set α} :
  is_complete s ↔ ∀ l : ultrafilter α, cauchy (l : filter α) → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x :=
is_complete_iff_ultrafilter.trans $ by simp only [le_principal_iff, ultrafilter.mem_coe]

protected lemma is_complete.union {s t : set α} (hs : is_complete s) (ht : is_complete t) :
  is_complete (s ∪ t) :=
begin
  simp only [is_complete_iff_ultrafilter', ultrafilter.union_mem_iff, or_imp_distrib] at *,
  exact λ l hl, ⟨λ hsl, (hs l hl hsl).imp $ λ x hx, ⟨or.inl hx.fst, hx.snd⟩,
    λ htl, (ht l hl htl).imp $ λ x hx, ⟨or.inr hx.fst, hx.snd⟩⟩
end

[Yury G. Kudryashov]

#11912

[Yury G. Kudryashov]

I used my proof because IMHO we should have is_complete_iff_ultrafilter, and with this lemma my proof is much shorter.

[Sebastien Gouezel]

Thanks to both of you!