Splitting(?) an ultrafilter

Stream: Is there code for X?

[Adam Topaz]

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]

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]

(hopefully I have the statement right)

[Adam Topaz]

Yes that's right

[Reid Barton]

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]

Im a bit surprised this is not in mathlib

[Reid Barton]

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

[Reid Barton]

image_mem_sets is one half

[Adam Topaz]

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]

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

[Adam Topaz]

Who came up with this comap terminology btw?

[Adam Topaz]

Adam Topaz said:

Who came up with this comap terminology btw?

?

[Johan Commelin]

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]

#5195