Zulip Chat Archive

Stream: Is there code for X?

Topic: Splitting(?) an ultrafilter


view this post on Zulip Adam Topaz (Nov 30 2020 at 00:07):

I don't know whether this has a standard name. Do we have something like this in mathlib?

import order.filter.ultrafilter

open_locale classical
noncomputable theory

open filter

variables {α β : Type*}

lemma splitter (F : ultrafilter (α  β)) : set.range sum.inl  F.1  set.range sum.inr  F.1 :=
mem_or_mem_of_ultrafilter F.2 $ by { convert F.1.univ_sets, tidy }

def split : ultrafilter (α  β)  ultrafilter α  ultrafilter β := λ F,
(splitter F).by_cases
(λ h, sum.inl $
{ val :=
  { sets := { s | sum.inl '' s  F.1 },
    univ_sets := by simpa,
    sets_of_superset := λ S T hS incl, F.1.sets_of_superset hS (set.monotone_image incl),
    inter_sets := sorry },
  property := sorry } )
(λ h, sum.inr $
{ val :=
  { sets := { s | sum.inr '' s  F.1 },
    univ_sets := by simpa,
    sets_of_superset :=  λ S T hS incl, F.1.sets_of_superset hS (set.monotone_image incl),
    inter_sets := sorry },
  property := sorry } )

I have some not-very-pretty proofs for these sorry's, but if anyone wants a golf challenge, I'm sure they can be boiled down to a few lines.

view this post on Zulip Reid Barton (Nov 30 2020 at 00:20):

I think you should prove something like if ABA \to B is injective and μ\mu is an ultrafilter on BB for which the image of AA is "big", then filter.comap of μ\mu is an ultrafilter on AA

view this post on Zulip Reid Barton (Nov 30 2020 at 00:21):

(hopefully I have the statement right)

view this post on Zulip Adam Topaz (Nov 30 2020 at 00:22):

Yes that's right

view this post on Zulip Reid Barton (Nov 30 2020 at 00:23):

and that seems pretty easy because the union of the images of SS and ASA - S is the image of AA which is big

view this post on Zulip Adam Topaz (Nov 30 2020 at 00:25):

Im a bit surprised this is not in mathlib

view this post on Zulip Reid Barton (Nov 30 2020 at 00:25):

I guess comap along an injective function is given by your definition? I don't see that in mathlib though

view this post on Zulip Reid Barton (Nov 30 2020 at 00:26):

image_mem_sets is one half

view this post on Zulip Adam Topaz (Nov 30 2020 at 00:28):

I can also use some shenanigans to define this using the fact that βX\beta X is compact Hausdorff and the disjoint union of two comphaus's is again a CompHaus. But it feels like we should have an explicit description too

view this post on Zulip Adam Topaz (Dec 01 2020 at 02:35):

branch#ultrafilter_comap_large
The proofs could probably use some golfing. I'll try to open a PR soon.

view this post on Zulip Adam Topaz (Dec 01 2020 at 02:37):

Who came up with this comap terminology btw?

view this post on Zulip Adam Topaz (Dec 01 2020 at 03:01):

Adam Topaz said:

Who came up with this comap terminology btw?

:haskell: ?

view this post on Zulip Johan Commelin (Dec 01 2020 at 04:47):

No idea... it's something that already existed in mathlib when I showed up. And it's shorter than pullback, so I went along (-;

view this post on Zulip Adam Topaz (Dec 02 2020 at 23:27):

#5195


Last updated: May 07 2021 at 21:10 UTC