Ultrafilter map continuous

Stream: maths

[Adam Topaz]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Adam Topaz]

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

[Reid Barton]

No just a file I had lying around

[Adam Topaz]

Ah ok. Thanks.

[Adam Topaz]

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

[Reid Barton]

I agree it seems to be missing

[Adam Topaz]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

I guess it's not there :oh_no:

[Reid Barton]

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]

Does this last goal follow from the monad laws?

[Adam Topaz]

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

[Reid Barton]

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]

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

[Reid Barton]

how frustrating

[Reid Barton]

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]

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