Stream: Is there code for X?

Topic: Splitting(?) an ultrafilter

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.

Reid Barton (Nov 30 2020 at 00:20):

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

Reid Barton (Nov 30 2020 at 00:21):

(hopefully I have the statement right)

Yes that's right

Reid Barton (Nov 30 2020 at 00:23):

and that seems pretty easy because the union of the images of $S$ and $A - S$ is the image of $A$ which is big

Adam Topaz (Nov 30 2020 at 00:25):

Im a bit surprised this is not in mathlib

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

Reid Barton (Nov 30 2020 at 00:26):

image_mem_sets is one half

Adam Topaz (Nov 30 2020 at 00:28):

I can also use some shenanigans to define this using the fact that $\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

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.

Adam Topaz (Dec 01 2020 at 02:37):

Who came up with this comap terminology btw?

Adam Topaz (Dec 01 2020 at 03:01):

Who came up with this comap terminology btw?

?

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 (-;

Adam Topaz (Dec 02 2020 at 23:27):

#5195

Last updated: May 07 2021 at 21:10 UTC