Zulip Chat Archive

Stream: maths

Topic: comap of ultrafilter of surjective function


Bernd Losert (Jan 08 2022 at 21:47):

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 (Jan 08 2022 at 21:48):

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

Kevin Buzzard (Jan 08 2022 at 22:23):

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

Kevin Buzzard (Jan 08 2022 at 22:25):

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

Kevin Buzzard (Jan 08 2022 at 22:25):

docs#ultrafilter.of

Adam Topaz (Jan 08 2022 at 22:25):

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

Kevin Buzzard (Jan 08 2022 at 22:26):

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

Bernd Losert (Jan 08 2022 at 22:30):

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 (Jan 08 2022 at 22:30):

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 (Jan 08 2022 at 22:33):

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

Bernd Losert (Jan 08 2022 at 22:34):

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

Adam Topaz (Jan 08 2022 at 22:34):

converges in the compact set, I suppose?

Bernd Losert (Jan 08 2022 at 22:34):

This is also the case in the topological setting.

Bernd Losert (Jan 08 2022 at 22:35):

Here's my definition:

def is_compact [p : convergence_space X] (A : set X) :=   : ultrafilter X⦄, A     x, p.converges  x

Adam Topaz (Jan 08 2022 at 22:37):

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

Adam Topaz (Jan 08 2022 at 22:37):

docs#is_compact_iff_ultrafilter_le_nhds

Bernd Losert (Jan 08 2022 at 22:38):

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

Adam Topaz (Jan 08 2022 at 22:39):

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 (Jan 08 2022 at 22:44):

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 (Jan 08 2022 at 22:45):

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 (Jan 08 2022 at 22:46):

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 (Jan 08 2022 at 22:47):

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

Bernd Losert (Jan 08 2022 at 22:48):

g⁻¹[V] is basically comap g V

Adam Topaz (Jan 08 2022 at 22:48):

but that's not an ultrafilter.

Bernd Losert (Jan 08 2022 at 22:50):

Indeed. That's an error in my notes!

Bernd Losert (Jan 08 2022 at 22:50):

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 (Jan 08 2022 at 22:54):

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 (Jan 08 2022 at 22:56):

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 (Jan 08 2022 at 22:59):

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


Last updated: Dec 20 2023 at 11:08 UTC