# Zulip Chat Archive

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

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

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

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):

Does this last goal follow from the monad laws?

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

#### Reid Barton (Sep 24 2020 at 23:23):

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