## Stream: maths

### Topic: Ultrafilter map continuous

#### 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...

#### 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...

#### 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 }


#### Adam Topaz (Sep 24 2020 at 22:40):

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

#### 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

/- 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 := _,

end CompHaus


#### 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.

#### Adam Topaz (Sep 24 2020 at 22:43):

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

#### Reid Barton (Sep 24 2020 at 22:43):

No just a file I had lying around

Ah ok. Thanks.

#### Adam Topaz (Sep 24 2020 at 22:46):

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

#### Reid Barton (Sep 24 2020 at 22:48):

I agree it seems to be missing

#### 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.

#### 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


#### 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.

#### 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.

#### Adam Topaz (Sep 24 2020 at 23:07):

I guess it's not there :oh_no:

#### 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


#### Adam Topaz (Sep 24 2020 at 23:19):

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

#### 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


#### Adam Topaz (Sep 24 2020 at 23:22):

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

how frustrating

#### 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


#### 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