comap of ultrafilter of surjective function

Stream: maths

[Bernd Losert]

I see mathlib has a version of comap for ultrafilters involving injective functions, but I need a version involving surjective functions. For example, if m : α → β is surjective and u : filter β contains β, then comap m u should contain α, and hence ultrafilter.of (comap m u) also contains α.

[Bernd Losert]

Hmm.. but maybe this construction isn't really functorial.

[Kevin Buzzard]

You can pull back a filter along any map but in general the pullback of an ultrafilter might not be an ultrafilter.

[Kevin Buzzard]

I'm a bit confused about the relevance of containing beta, this is not really much to do with an ultrafilter.

[Kevin Buzzard]

docs#ultrafilter.of

[Adam Topaz]

docs#filter.univ_sets ? Or maybe we're misunderstanding what you mean by "containing $\beta$"

[Kevin Buzzard]

Oh this (ultrafilter.of) just chooses a random ultrafilter containing a filter, it's not functorial at all, as you rightly say

[Bernd Losert]

Yeah. I am trying to prove that the continuous image of a compact set is compact in the convergence space setting. There is a slick proof using ultrafilters, but for that I need a lemma of the kind I mentioned in the original post.

[Reid Barton]

For example if the types/sets involved are finite, then an ultrafilter is just an element, and you can pick an element of the preimage (since the map is surjective) but not in a canonical way

[Adam Topaz]

Is compact defined by saying that every ultrafilter converges to a point?

[Bernd Losert]

Yes, compact means that every ultrafilter containing the compact set converges.

[Adam Topaz]

converges in the compact set, I suppose?

[Bernd Losert]

This is also the case in the topological setting.

[Bernd Losert]

Here's my definition:

def is_compact [p : convergence_space X] (A : set X) := ∀ ⦃ℱ : ultrafilter X⦄, A ∈ ℱ → ∃ x, p.converges ℱ x

[Adam Topaz]

you don't want your x to be a member of A?

[Adam Topaz]

docs#is_compact_iff_ultrafilter_le_nhds

[Bernd Losert]

According to my notes, it doesn't matter, but maybe I need to fix that.

[Adam Topaz]

I don't really know, since I'm not actually familiar with convergence spaces... I'm just going from what I know about topological spaces here.

[Bernd Losert]

Here is the proof from my notes:

Let X,Y be convergence spaces, let f : X → Y be continuous and let A ⊆ X be
compact. Then f(A) is compact: Define g : A → f (A) by g(a) = f(a). Let V be
an ultrafilter on f(A). Since g is onto, g⁻¹[V] is an ultrafilter on A. Since A
is compact, g⁻¹[V] converges. Since g⁻¹[V] converges and is continuous, V = g[g⁻¹[V]]
converges in f(A).

[Adam Topaz]

Since g is onto, g⁻¹[V] is an ultrafilter on A here g^-1[V] is either some strange notation that I don't know, or the assertion is false.

[Adam Topaz]

But for that you should be able to use ultrafilter.of as above. You would need to show that ultrafilter.map (ultrafilter.of (filter.comap F)) = F.

[Adam Topaz]

Can you give a mwe with the definition of a convergence space and of continuity?

[Bernd Losert]

g⁻¹[V] is basically comap g V

[Adam Topaz]

but that's not an ultrafilter.

[Bernd Losert]

Indeed. That's an error in my notes!

[Bernd Losert]

Here's some code:

mport order.filter.partial
import order.filter.ultrafilter
import algebra.support
import category_theory.concrete_category.bundled

noncomputable theory
open set function filter classical option category_theory
open_locale classical filter

variables {X Y Z : Type*}

structure convergence_space (X : Type*) :=
(converges : filter X → X → Prop)
(pure_converges : ∀ x, converges (pure x) x)
(le_converges : ∀ {ℱ 𝒢}, ℱ ≤ 𝒢 → ∀ {x}, converges 𝒢 x → converges ℱ x) -- ℱ ≤ 𝒢 means 𝒢 ⊆ ℱ

attribute [ext] convergence_space
attribute [class] convergence_space

open convergence_space

def continuous [p : convergence_space X] [q : convergence_space Y] (f : X → Y) : Prop :=
∀ ⦃x ℱ⦄, p.converges ℱ x → q.converges (map f ℱ) (f x)

def is_compact [p : convergence_space X] (A : set X) := ∀ ⦃ℱ : ultrafilter X⦄, A ∈ ℱ → ∃ x, p.converges ℱ x

lemma is_compact.image {f : X → Y} {A : set X} [p : convergence_space X] [q : convergence_space Y]
  (h : is_compact A) (h' : continuous f) : is_compact (f '' A) := sorry?

[Bernd Losert]

In my notes, I have this result, which I guess I was relying on:

If G is an ultrafilter and f⁻¹[G] is a filter on X, then G = f[f⁻¹[G]] and G=f[U] for every ultrafilter U on X finer than f⁻¹[G].

[Adam Topaz]

I think this is more-or-less the proof that your notes sketched here:

lemma is_compact.image {f : X → Y} {A : set X} [p : convergence_space X] [q : convergence_space Y]
  (h : is_compact A) (h' : continuous f) : is_compact (f '' A) :=
begin
  rintros F hA,
  haveI : (filter.comap f F).ne_bot := sorry,
  let G := ultrafilter.of (filter.comap f F),
  have hG : G.map f = F, sorry,
  have : A ∈ G, sorry,
  obtain ⟨t,ht⟩ := h this,
  use f t,
  rw ← hG,
  tauto,
end

[Bernd Losert]

Yep, that looks about right. Thanks a lot. I'll try to fill in the sorries.