Filter on (set X)

Stream: Is there code for X?

[Damien Thomine]

I have a function defined on set (X) (or rather, on a filter F of neighborhoods on X), and want to take its limit when taking smaller and smaller neighborhoods. I think the filter along which I want to take its limit is something like

$$\{T : set (set X) | T \subset F \and \exists U \in F, \forall V \in T, T \subset U\}.$$

The motivation is as follows: I am formalizing the notion(s) of topological entropy. Classically, you take some $\epsilon >0$, define a quantity $h(\epsilon)$, and take the limit $\epsilon \to 0$. I want to get a non-metric version of topological entropy; I thus take some uniformity set $U$, define a quantity $h(U)$, and now I want to take its limit when $U \to \Delta$, where $\Delta$ is the diagonal.

Is it implemented in some way? I have found order.filter.small_sets, but it is much to large (it includes all subsets of a given $U \in F$, not only those which are in the initial filter).

[Junyan Xu]

@Damien Thomine I don't think what you wrote makes sense:
$$\{T : set (set X) | T \subset F \and \exists U \in F, \forall V \in T, T \subset U\}.$$
First it's not obvious it defines a filter (I think it usually doen't). Second, it's weird that T \subset U doesn't depend on V. Third, no matter what you replace T \subset U with, the condition is vacuously true when T is empty, so the empty set is in the filter and the filter must be trivial.

I suppose you want to formalize what Wikipedia calls the definition of Bowen and Dinaburg. I think what you want is the following:

import order.filter.at_top_bot
variables {X : Type*} (F : filter X)
#check (filter.at_bot : filter F.sets) -- defeq to `(filter.at_bot : filter {T // T ∈ F})`

Could you simply use it? And I guess you intend to take F to be some docs#uniform_space.core.uniformity, right?

I also thought a little about the more general definition that doesn't require a uniform structure, only a topology. It's a supremum over all open covers, and can be calculated as a limit over finer and finer open covers. To formalize the latter definition we need to order the open covers by refinement, which doesn't seem to exist in mathlib, but once we have that, I think we can simply use docs#filter.at_top or docs#filter.at_bot. docs#finpartition.has_le is the refinement relation for finite partitions, but covers are more general than partitions (which requires disjointness), not to mention the finiteness restriction. We have docs#category_theory.grothendieck_topology.cover for Grothendieck topology (which is essentially ordered by refinement and used to construct docs#category_theory.grothendieck_topology.sheafify) but not a more straightforward version for topological spaces. We also want the meet of finitely many open covers, which is given by docs#finpartition.has_inf for finpartitions.

[Damien Thomine]

@Junyan Xu Thank you very much for your answer. You are right, my attempt at a definition is nonsensical. I am not used to working with filters, so I may not always make sense; my excuses.

Your proposition (filter.at_bot on (uniformity X).sets) looks good. If I understand well, it is a filter on {U : set(X x X) | U \in uniformity X}. In order to avoid annoying coercions, I would have liked a filter on set (X x X) (I think the image of the former under the inclusion (uniformity X) -> set (X x X) ), but maybe this is enough. I'll try this tomorrow and confirm if it works.

I choose the Bowen-Dinaburg version because it is convenient for applications, and I had in mind to actually compute the topologial entropy of a subshift of finite type.

The uniform structure is not a problem as long as one works with compact spaces, because then the uniform structure is canonical. However, I wanted to define the topological entropy for invariant compact subsets of larger spaces, and these larger spaces have no reason to be compact, so their uniform structure is not determined by their topology. Of course the end result will depend only on the topology of the space rather than its uniform structure, but I have not yet found a good fix for that.

[Junyan Xu]

@Damien Thomine

I choose the Bowen-Dinaburg version because it is convenient for applications, and I had in mind to actually compute the topologial entropy of a subshift of finite type.

Your project sounds fun!

However, I wanted to define the topological entropy for invariant compact subsets of larger spaces, and these larger spaces have no reason to be compact, so their uniform structure is not determined by their topology.

I don't quite see what the problem is. Can't you just view these compact subsets as compact topological spaces, and use the topological entropy on these compact spaces, which has unique uniform structure? Or maybe you want to connect them somehow to the topological entropy on the larger spaces?

Now, some update on the original question: after some more thoughts, I think I figured out the right definition for the filter on set X : it's simply {T : set (set X)) | ∃ U ∈ F, ∀ V ⊆ U, V ∈ T}, which I call filter_of_directed. This filter is larger than filter.map coe filter.at_bot (which I abbreviate as map_at_bot), so once you show your function has limit on filter_of_directed, then it also has limit on map_at_bot.

In the code below I did it in maximal generality, generalizing set X to an arbitrary preorder and the filter on X to an arbitrary nonempty downward-directed subset.

import order.filter.at_top_bot
import order.pfilter

variable {X : Type*}

def filter.pfilter (F : filter X) : order.pfilter (set X) :=
⟨ { carrier := F.sets,
    lower' := λ a b h ha, F.sets_of_superset ha h,
    nonempty' := ⟨set.univ, F.univ_sets⟩,
    directed' := λ a ha b hb, ⟨order_dual.to_dual (a.of_dual ∩ b.of_dual),
      F.inter_sets ha hb, set.inter_subset_left a b, set.inter_subset_right a b⟩ } ⟩

lemma filter.generate_singleton (s : set X) :
  filter.generate {s} = filter.principal s :=
begin
  apply le_antisymm,
  { intros t h, apply filter.generate_sets.superset _ h, exact filter.generate_sets.basic rfl },
  { rw filter.sets_iff_generate, rintro _ ⟨rfl⟩, exact subset_rfl },
end

variables [preorder X] {F : set X} (hn : F.nonempty) (hd : directed_on (≥) F)
-- hn and hd together are weaker than pfilter (two of three conditions)

def filter_of_directed : filter X :=
{ sets := {T : set X | ∃ U ∈ F, ∀ V ≤ U, V ∈ T},
  univ_sets := ⟨hn.some, hn.some_mem, λ _ _, trivial⟩,
  sets_of_superset := λ s t ⟨U, hU, hs⟩ hl, ⟨U, hU, λ V hV, hl (hs V hV)⟩,
  inter_sets := λ s t ⟨U₁, hU₁, hs₁⟩ ⟨U₂, hU₂, hs₂⟩,
    let ⟨U, hU, hl₁, hl₂⟩ := hd U₁ hU₁ U₂ hU₂ in
    ⟨U, hU, λ V hV, ⟨hs₁ V (hV.trans hl₁), hs₂ V (hV.trans hl₂)⟩⟩ }

lemma mem_filter_of_directed (T : set X) :
  T ∈ filter_of_directed hn hd ↔ ∃ U ∈ F, set.Iic U ⊆ T := iff.rfl

lemma filter_of_directed_eq :
  filter_of_directed hn hd = ⨅ U ∈ F, filter.principal (set.Iic U) :=
begin
  simp_rw [← filter.generate_singleton, ← filter.generate_Union],
  apply le_antisymm,
  { rw filter.sets_iff_generate, rintro T hT,
    obtain ⟨x, hx, he⟩ := set.mem_Union₂.1 hT,
    refine (mem_filter_of_directed hn hd T).2 ⟨x, hx, he.superset⟩ },
  { rintro T hT, obtain ⟨U, hU, hl⟩ := (mem_filter_of_directed hn hd T).1 hT,
    apply filter.generate_sets.superset (filter.generate_sets.basic _) hl,
    exact set.mem_Union₂.2 ⟨U, hU, rfl⟩ },
end

lemma directed_on_univ' : directed_on (≥) F ↔ directed_on (≥) (set.univ : set F) :=
begin
  rw directed_on_univ_iff, refine ⟨λ hd, ⟨_⟩, _⟩,
  { rintro ⟨a, ha⟩ ⟨b, hb⟩,
    obtain ⟨c, hc, h⟩ := hd a ha b hb,
    exact ⟨⟨c, hc⟩, h⟩ },
  { rintro ⟨hd⟩ a ha b hb,
    obtain ⟨⟨c, hc⟩, h⟩ := hd ⟨a, ha⟩ ⟨b, hb⟩,
    exact ⟨c, hc, h⟩ },
end

lemma filter_of_directed_eq_at_bot :
  filter_of_directed (@set.univ_nonempty _ hn.to_subtype) (directed_on_univ'.1 hd) =
  filter.at_bot :=
by rw [filter_of_directed_eq, filter.at_bot, infi_univ]


def map_at_bot (F : set X) : filter X := filter.map coe (filter.at_bot : filter F)

include hn hd
lemma mem_map_at_bot (T : set X) :
  T ∈ map_at_bot F ↔ ∃ U ∈ F, set.Iic U ∩ F ⊆ T :=
begin
  dsimp [map_at_bot], rw [← filter_of_directed_eq_at_bot hn hd, mem_filter_of_directed],
  exact ⟨λ ⟨⟨U, hU⟩, _, h⟩, ⟨U, hU, λ V ⟨hVU, hVF⟩, @h ⟨V, hVF⟩ hVU⟩,
    λ ⟨U, hU, h⟩, ⟨⟨U, hU⟩, trivial, λ ⟨V, hVF⟩ hVU, h ⟨hVU, hVF⟩⟩⟩,
end

lemma map_at_bot_eq (T : set X) : map_at_bot F = filter_of_directed hn hd ⊓ filter.principal F :=
begin
  ext, rw [filter.mem_inf_principal, mem_map_at_bot hn hd, mem_filter_of_directed],
  exact exists₂_congr (λ _ _, forall_congr $ λ _, and_imp),
end

Let me tag @Patrick Massot @Yaël Dillies to see if any of these are already in mathlib.

[Junyan Xu]

Oh wait, I think filter_of_directed doesn't actually work, and we should stick to map_at_bot, which I proved is equal to {T | ∃ U ∈ F, set.Iic U ∩ F ⊆ T}, i.e. {T : set (set X)) | ∃ U ∈ F, ∀ V ⊆ U, V ∈ F → V ∈ T}.