Zulip Chat Archive

Stream: maths

Topic: Ultrafilter map continuous


view this post on Zulip Adam Topaz (Sep 24 2020 at 22:28):

I have a 20 line proof of the following example:

import order.filter.ultrafilter
import topology.stone_cech

open filter
open topological_space

example {α β : Type*} (f : α  β) : continuous (ultrafilter.map f) := sorry

Is there a simpler proof for this? e.g. using docs#continuous_ultrafilter_extend ? I'm not as familiar with the topology parts of mathlib as I should be...

view this post on Zulip Reid Barton (Sep 24 2020 at 22:37):

I was under the impression that I built the adjunction involving the Stone-Cech compactification at some point... but where...

view this post on Zulip Reid Barton (Sep 24 2020 at 22:39):

lol

-- TODO: These proofs seem too long!
noncomputable def hom_iso (S : Type u) (X : CompHaus) :
  (free_obj S  X)  (S  X) :=
{ to_fun := λ g, g  ultrafilter.pure,
  inv_fun := λ f, ultrafilter.extend f, continuous_ultrafilter_extend f⟩,
  left_inv := λ g, begin
    apply subtype.eq,
    apply dense_inducing_pure.dense.equalizer,
    { apply continuous_ultrafilter_extend },
    { apply g.2 },
    { ext x,
      exact congr_fun (ultrafilter_extend_extends (g  ultrafilter.pure)) x },
    { apply_instance }
  end,
  right_inv := λ f, ultrafilter_extend_extends f }

view this post on Zulip Adam Topaz (Sep 24 2020 at 22:40):

Nice. I didn't know the adjunction existed in mathlib

view this post on Zulip Reid Barton (Sep 24 2020 at 22:40):

Maybe this will help (mathlib commit d12db89ac21bdcf5d33fd1dc7262ebbd3a7dcf54)

import category_theory.monad.adjunction
import topology.category.Top.basic
import topology.stone_cech

noncomputable theory

universe u

structure CompHaus :=
(to_Top : Top.{u})
[is_compact : compact_space to_Top]
[is_hausdorff : t2_space to_Top]

namespace CompHaus

open category_theory filter

instance : has_coe CompHaus.{u} Top.{u} :=
λ X, X.1

-- TODO: Fix this mess
instance {X : CompHaus.{u}} : compact_space X.to_Top := X.is_compact
instance {X : CompHaus.{u}} : t2_space X.to_Top := X.is_hausdorff
instance i {X : CompHaus.{u}} : compact_space X := X.is_compact
instance ij {X : CompHaus.{u}} : t2_space X := X.is_hausdorff

def of (X : Type u) [topological_space X] [compact_space X] [t2_space X] : CompHaus :=
⟨⟨X⟩⟩

instance category : large_category CompHaus :=
induced_category.category to_Top

instance concrete_category : concrete_category CompHaus.{u} :=
induced_category.concrete_category to_Top

instance has_forget_to_CompHaus : has_forget₂ CompHaus Top :=
induced_category.has_forget₂ to_Top

section adj
/- The space of ultrafilters β : Set → CompHaus
is left adjoint to the forgetful functor CompHaus → Set. -/

def free_obj (S : Type u) : CompHaus.{u} :=
of (ultrafilter S)

-- TODO: These proofs seem too long!
noncomputable def hom_iso (S : Type u) (X : CompHaus) :
  (free_obj S  X)  (S  X) :=
{ to_fun := λ g, g  ultrafilter.pure,
  inv_fun := λ f, ultrafilter.extend f, continuous_ultrafilter_extend f⟩,
  left_inv := λ g, begin
    apply subtype.eq,
    apply dense_inducing_pure.dense.equalizer,
    { apply continuous_ultrafilter_extend },
    { apply g.2 },
    { ext x,
      exact congr_fun (ultrafilter_extend_extends (g  ultrafilter.pure)) x },
    { apply_instance }
  end,
  right_inv := λ f, ultrafilter_extend_extends f }

instance : is_right_adjoint (forget CompHaus.{u}) :=
{ left := _,
  adj := adjunction.adjunction_of_equiv_left hom_iso (by { intros, refl }) }

end adj

end CompHaus

view this post on Zulip Reid Barton (Sep 24 2020 at 22:42):

I mean, your statement definitely follows somehow from this but it might be longer than your proof.

view this post on Zulip Adam Topaz (Sep 24 2020 at 22:43):

Is this in mathlib? API search came up empty with CompHaus

view this post on Zulip Reid Barton (Sep 24 2020 at 22:43):

No just a file I had lying around

view this post on Zulip Adam Topaz (Sep 24 2020 at 22:45):

Ah ok. Thanks.

view this post on Zulip Adam Topaz (Sep 24 2020 at 22:46):

I was hoping to be able to just quote a lemma from mathlib :smile:

view this post on Zulip Reid Barton (Sep 24 2020 at 22:48):

I agree it seems to be missing

view this post on Zulip Adam Topaz (Sep 24 2020 at 22:49):

There must be a way to do it with ultrafilter.extend, but I couldn't come up with a nice proof.

view this post on Zulip Adam Topaz (Sep 24 2020 at 22:52):

Here's my original proof FWIW

import order.filter.ultrafilter
import topology.stone_cech

open filter
open topological_space

example {α β : Type*} (f : α  β) : continuous (ultrafilter.map f) :=
begin
  intros U hU,
  induction hU,
  { rcases hU_H with V,rfl⟩,
    apply is_open_of_is_topological_basis ultrafilter_basis_is_basis,
    use f ⁻¹' V,
    refl },
  { apply is_open_of_is_topological_basis ultrafilter_basis_is_basis,
    use set.univ,
    ext,
    refine λ cond, _, by tauto⟩,
    apply univ_sets },
  { apply is_open_inter,
    assumption' },
  { rw set.preimage_sUnion,
    apply is_open_sUnion,
    rintros T T,rfl⟩,
    apply is_open_sUnion,
    rintros S S,rfl⟩,
    apply hU_ih,
    assumption }
end

view this post on Zulip Reid Barton (Sep 24 2020 at 23:01):

Now I'm not even sure you can do it easily with ultrafilter.extend. Because you need to somehow identify the extension with ultrafilter.map, and the obvious way to do that (it's the unique continuous map that fits in a square) presupposes that you already know ultrafilter.map is continuous.

view this post on Zulip Adam Topaz (Sep 24 2020 at 23:07):

Right. I was also hoping mathlib had some lemma saying that ultrafilter.extend agrees with pure composed with the map f.

view this post on Zulip Adam Topaz (Sep 24 2020 at 23:07):

I guess it's not there :oh_no:

view this post on Zulip Reid Barton (Sep 24 2020 at 23:16):

This seems to be frustratingly close

lemma continuous_ultrafilter.map {α β : Type*} (f : α  β) : continuous (ultrafilter.map f) :=
begin
  rw continuous_iff_ultrafilter,
  intros u g hg,
  let G : ultrafilter (ultrafilter α) := g, hg⟩,
  change G.val  𝓝 u  (G.map _).val  𝓝 _,
  rw [ultrafilter_converges_iff, ultrafilter_converges_iff],
  rintro rfl,
  -- ⊢ ultrafilter.map f (mjoin G) = mjoin (ultrafilter.map (ultrafilter.map f) G)
end

view this post on Zulip Adam Topaz (Sep 24 2020 at 23:19):

Does this last goal follow from the monad laws?

view this post on Zulip Adam Topaz (Sep 24 2020 at 23:19):

(I'm away from my computer right now.)

view this post on Zulip Reid Barton (Sep 24 2020 at 23:22):

Kind of... it works when α and β are in the same universe:

lemma {u} continuous_ultrafilter.map {α β : Type u} (f : α  β) : continuous (ultrafilter.map f) :=
begin
  rw continuous_iff_ultrafilter,
  intros u g hg,
  let G : ultrafilter (ultrafilter α) := g, hg⟩,
  change G.val  𝓝 u  (G.map _).val  𝓝 _,
  rw [ultrafilter_converges_iff, ultrafilter_converges_iff],
  rintro rfl,
  exact (mjoin_map_map f G).symm
end

view this post on Zulip Adam Topaz (Sep 24 2020 at 23:22):

Oh right .... That's because of mjoin

view this post on Zulip Reid Barton (Sep 24 2020 at 23:23):

how frustrating

view this post on Zulip Reid Barton (Sep 24 2020 at 23:29):

OK sometimes the simple way is best

lemma continuous_ultrafilter.map {α β : Type*} (f : α  β) : continuous (ultrafilter.map f) :=
begin
  apply continuous_generated_from,
  rintros _ s, rfl⟩,
  exact ultrafilter_is_open_basic (f ⁻¹' s)
end

view this post on Zulip Adam Topaz (Sep 24 2020 at 23:31):

Cool. I guess continuous_generated_from is the boilerplate version of the induction in my original proof. Good to know!


Last updated: May 18 2021 at 07:19 UTC