topology on filters?

Stream: maths

[Yury G. Kudryashov]

Is there any reasonable topology on filter X such that, e.g., in case of a topological space, the nhds map is continuous (or even inducing)?

[Kevin Buzzard]

Nice question!

[Kevin Buzzard]

Naive idea: a basis of open sets is indexed by the opens U in X, with the set B(U) being the filters that contain U as an element. Only works for topological spaces though so not exactly what you want

[David Wärn]

The topology on ultrafilters given by docs#ultrafilter_basis actually defines a natural topology on filter X. This is the same as Kevin's suggestion except it uses all U instead of only the opens. Either way, nhds should be inducing since the preimage of B(U) is the interior of U (I think?), which is an arbitrary open subset of X

[Yury G. Kudryashov]

/me is going to reread this in the morning

[Yury G. Kudryashov]

Indeed,

import topology.maps

open set filter topological_space
open_locale filter topological_space

variables {X : Type*}

namespace filter

instance : topological_space (filter X) :=
generate_from $ range $ λ s : set X, {l : filter X | s ∈ l}

lemma nhds_eq (l : filter X) : 𝓝 l = ⨅ s ∈ l, 𝓟 {l' | s ∈ l'} :=
begin
  refine nhds_generate_from.trans _,
  simp only [mem_set_of_eq, and_comm (l ∈ _), infi_and, infi_range]
end

lemma inducing_nhds [topological_space X] : inducing (𝓝 : X → filter X) :=
begin
  refine ⟨eq_of_nhds_eq_nhds $ λ x, _⟩,
  simp only [nhds_induced, nhds_eq, comap_infi, comap_principal],
  refine le_antisymm (le_infi₂ $ λ s hs, le_principal_iff.2 _) (λ s hs, _),
  { filter_upwards [interior_mem_nhds.mpr hs] with y using mem_interior_iff_mem_nhds.mp },
  { exact mem_infi_of_mem s (mem_infi_of_mem hs $ λ y, mem_of_mem_nhds) }
end

end filter

[Yaël Dillies]

Is that somehow related to the topology on set α that I wanted? For reference, I need to prove

example (f : ℝ → ℝ) (hf : continuous f) : continuous (λ ab : α × α, ⨆ x ∈ Icc a b, f x) := sorry

for Sharkovskii's theorem, and I feel like it would naturally decompose into

example : continuous (uncurry Icc : ℝ × ℝ → set ℝ) := sorry

example {α : Type*} [topological_space α] (f : ℝ → ℝ) (hf : continuous f) (s : α → set ℝ)
  (hs : continuous s) :
  continuous (λ a, ⨆ x ∈ s a, f x) := sorry

had we topological_space (set ℝ).

[Yury G. Kudryashov]

Which topology on set X are you talking about? Some specific topology? I can imagine different topologies.

[Yury G. Kudryashov]

E.g., you can introduce a topology based on docs#emetric.Hausdorff_edist

[Reid Barton]

Yes, but this should be for nonempty compact sets (like Icc a b)

[Yury G. Kudryashov]

Another equivalent approach to topology on filter α:

import order.filter.lift
import topology.maps

open set filter topological_space
open_locale filter topological_space

variables {ι : Sort*} {α X : Type*}

def Iic_topology {α β : Type*} [semilattice_inf α] [semilattice_inf β] (f : α → β)
  (hf_inf : ∀ x y, f (x ⊓ y) = f x ⊓ f y) (hf : ∀ y, ∃ x, y ≤ f x) : topological_space β :=
{ is_open := λ s, ∃ t : set α, (⋃ x ∈ t, Iic (f x)) = s,
  is_open_univ := ⟨univ, Union₂_eq_univ_iff.2 $ λ y, (hf y).imp (λ x hx, ⟨mem_univ _, hx⟩)⟩,
  is_open_inter :=
    begin
      rintro _ _ ⟨s, rfl⟩ ⟨t, rfl⟩,
      refine ⟨image2 (⊓) s t, _⟩,
      simp only [image2_eq_Union, bUnion_Union, bUnion_singleton, inter_Union, Union_inter,
        Iic_inter_Iic, hf_inf]
    end,
  is_open_sUnion := λ s hs,
    begin
      choose! T hT using hs,
      use ⋃ t ∈ s, T t,
      simp only [bUnion_Union, hT, sUnion_eq_bUnion] { contextual := tt },
    end }

namespace filter

instance : topological_space (filter α) :=
generate_from $ range $ λ s : set α, {l : filter α | s ∈ l}

lemma topology_eq :
  filter.topological_space = Iic_topology (𝓟 : set α → filter α) (λ _ _, inf_principal.symm)
    (λ l, ⟨univ, le_principal_iff.2 univ_mem⟩) :=
begin
  have : ∀ s : set α, Iic (𝓟 s) = {l | s ∈ l}, by simp [Iic],
  refine le_antisymm (λ s hs, _) (le_generate_from_iff_subset_is_open.2 $ range_subset_iff.2 _),
  { rcases hs with ⟨t, rfl⟩,
    exact is_open_bUnion (λ s hs, generate_open.basic _ ⟨s, (this s).symm⟩) },
  { refine λ s, ⟨{s}, _⟩,
    rw [bUnion_singleton, this] }
end

lemma is_open_iff {s : set (filter α)} :
  is_open s ↔ ∃ T : set (set α), (⋃ t ∈ T, Iic (𝓟 t)) = s :=
by { rw [topology_eq], refl }