Zulip Chat Archive

Stream: maths

Topic: Reconstructing a filter from its points


Kyle Miller (Jul 27 2022 at 16:12):

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 (Jul 27 2022 at 17:30):

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

Kevin Buzzard (Jul 27 2022 at 17:31):

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

Kyle Miller (Jul 27 2022 at 17:34):

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 (Jul 27 2022 at 17:37):

I had imagined that if you have the filter generated by the open sets containing AA 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 AA, and I'd like for A = {a : α | 𝓝 a ≤ f}. This might be too much to hope for.

Kyle Miller (Jul 27 2022 at 17:41):

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 (Jul 28 2022 at 09:23):

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 (Jul 30 2022 at 02:50):

@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εs := metric.mem_nhds_iff.1 hs,
  obtain n, hn := exists_nat_one_div_lt ,
  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

Last updated: Dec 20 2023 at 11:08 UTC