Reconstructing a filter from its points

Stream: maths

[Kyle Miller]

I was wondering whether it's possible to reconstruct a filter from the neighborhood filters it contains, at least when the filter has a basis of open sets, and allowing the space to be compact Hausdorff?

import topology.separation

open_locale topological_space

lemma rebuild_le {α : Type*} [topological_space α]
  (f : filter α) :
  Sup (𝓝 '' {a : α | 𝓝 a ≤ f}) ≤ f :=
begin
  intros s hs,
  simp,
  intros a ha,
  exact ha hs,
end

lemma le_rebuild {α : Type*} [topological_space α]
  [t2_space α] [compact_space α] -- a guess at sufficient assumptions
  (f : filter α)
  (h : ∀ s ∈ f, ∃ (u : set α), is_open u ∧ u ⊆ s) :
  f ≤ Sup (𝓝 '' {a : α | 𝓝 a ≤ f}) :=
begin
  sorry
end

[Kevin Buzzard]

Would you expect this to be true for a principal filter associated to a non-open set?

[Kevin Buzzard]

I think your h doesn't say anything because u can be empty?

[Kyle Miller]

That was a mistake -- I want it to be a filter generated by open sets. No guarantees that this is correctly formulated yet.

[Kyle Miller]

I had imagined that if you have the filter generated by the open sets containing $A$ that this would be true.

What I'd like is for every filter generated by open sets to be generated by all the open sets containing some set $A$, and I'd like for A = {a : α | 𝓝 a ≤ f}. This might be too much to hope for.

[Kyle Miller]

The thought here is that in a compact hausdorff space, the neighborhood filters are the only minimal filters among all nonempty filters that are generated by open sets, so these are the only possible points of a filter generated by open sets.

[Kyle Miller]

It looks like it's true, though I still have a few sorries. https://gist.github.com/kmill/ec673e254e2950d11da1d39785405647

The main theorem is

lemma filter_eq_nhds_principal_pts
  [t2_space α] [compact_space α]
  (f : filter α) (hf : f.is_open) :
  f = 𝓝' {a : α | 𝓝 a ≤ f}

where 𝓝' s is the filter generated by all the open sets containing s, and the filter.is_open predicate is whether a filter is generated by open sets. In a T1 space you get 𝓝' s ≤ 𝓝' s' ↔ s ⊆ s' among other nice relations.

The biggest sorry is that maximal open filters in a compact Hausdorff space are exactly neighborhood filters (I've proved it on paper, but it would be nice to put it into Lean to be sure, however I need some sleep!). The other sorries have to be true by abstract nonsense.

[Junyan Xu]

@Kyle Miller By "maximal" open filters, you actually meant the minimal (ne_bot) ones right? It turns out the nhds filters usually aren't even minimal, because there are nhds_within open filters that are smaller. For example, in the (closed) unit interval [0,1], nhds 0 is strictly larger than nhds_within 0 {0}ᶜ, which is in turn strictly larger than nhds_within 0 s, where s = {0, 1, 1/2, 1/3, 1/4, ...}ᶜ. The latter two are examples of filters that "contains no points" but are still not ⊥. Here's a formalization:

import topology.separation
import topology.unit_interval

open_locale filter topological_space

variables {α : Type*} [topological_space α]

def filter.is_open (f : filter α) : Prop := ∀ s ∈ f, ∃ u ∈ f, is_open u ∧ u ⊆ s

lemma nhds_is_open (a : α) : (𝓝 a).is_open :=
λ s hs, begin
  obtain ⟨u, hus, ho, hau⟩ := mem_nhds_iff.1 hs,
  exact ⟨u, ho.mem_nhds hau, ho, hus⟩,
end

lemma is_open.principal {s : set α} (hs : is_open s) : (𝓟 s).is_open :=
λ t ht, ⟨s, subset_rfl, hs, ht⟩

lemma filter.is_open.inf {f g : filter α} (hf : f.is_open) (hg : g.is_open) : (f ⊓ g).is_open :=
begin
  rintro s ⟨t₁, h₁, t₂, h₂, rfl⟩,
  obtain ⟨u₁, hu₁, o₁, hut₁⟩ := hf t₁ h₁,
  obtain ⟨u₂, hu₂, o₂, hut₂⟩ := hg t₂ h₂,
  exact ⟨u₁ ∩ u₂, filter.inter_mem_inf hu₁ hu₂, o₁.inter o₂, set.inter_subset_inter hut₁ hut₂⟩,
end

lemma nhds_within_is_open (a : α) (s : set α) (hs : is_open s) : (𝓝[s] a).is_open :=
(nhds_is_open a).inf hs.principal

lemma nhds_within_compl_zero_lt : 𝓝[{0}ᶜ] (0 : unit_interval) < 𝓝 0 :=
lt_of_le_not_le inf_le_left $ λ h, begin
  obtain ⟨t, ht, _, h0⟩ := mem_nhds_iff.1 (h self_mem_nhds_within),
  exact ht h0 rfl,
end

noncomputable def reciprocal_seq (n : ℕ) : unit_interval :=
⟨1/n, begin
  cases n, norm_num,
  { apply unit_interval.div_mem; norm_cast, swap 3, apply nat.succ_le_succ, all_goals {norm_num} },
end⟩

lemma nhds_within_compl_reciprocal_seq_lt :
  𝓝[(set.range reciprocal_seq)ᶜ] (0 : unit_interval) < 𝓝[{0}ᶜ] 0 :=
lt_of_le_not_le (nhds_within_mono _ $ set.compl_subset_compl.2 $
  by { rintro _ h, use 0, cases h, rw reciprocal_seq, norm_num }) $ λ h,
begin
  obtain ⟨s, hs, t, ht, he⟩ := h self_mem_nhds_within,
  obtain ⟨ε, hε, hεs⟩ := metric.mem_nhds_iff.1 hs,
  obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε,
  have : reciprocal_seq (n+1) ∈ s ∩ t,
  { split,
    { apply hεs, rw metric.ball, change abs _ < _, convert hn,
      rw reciprocal_seq, norm_num, exact_mod_cast (reciprocal_seq (n+1)).2.1 },
    { apply ht, rw reciprocal_seq, intro h, replace h := subtype.ext_iff.1 h,
      refine one_div_ne_zero _ h, rw nat.cast_ne_zero, norm_num } },
  rw ← he at this, apply this, exact ⟨n+1, rfl⟩,
end