filter map on the set level

Stream: general

[Bernd Losert]

Say I have m : set α → set α and f : filter α. How do I "map" m on f?

[Floris van Doorn]

You need some conditions on m to know that any such result is again a filter.

[Bernd Losert]

I'm not too worried about that since I can use filter.generate to get a filter back.

[Floris van Doorn]

maybe docs#filter.map and docs#filter.comap are relevant.

[Bernd Losert]

Unfortunately, map and comap are not going to work.

[Floris van Doorn]

It sounds like you want something like

def my_map {α β} (m : set α → set β) (f : filter α) : filter β :=
filter.generate (m '' f.sets)

I don't know if that is a sensible construction though.

[Bernd Losert]

Remind me what '' does.

[Floris van Doorn]

it's the image of a set under a function, docs#set.image

[Bernd Losert]

Ah, that's right. I had forgotten about it. Thanks.

[Floris van Doorn]

I think the bigger question is: what do you want this map of m on f to do, or what properties do you want it do have?

[Adam Topaz]

Isn't there some Galois connection between sets and filters somewhere?

[Floris van Doorn]

sure: docs#filter.gi_generate

[Bernd Losert]

Floris van Doorn said:

I think the bigger question is: what do you want this map of m on f to do, or what properties do you want it do have?

I have defined the closure cl of a set as an operator of type set X -> set X. I want to build the "closure" of a filter by applying cl to each of the sets in the filter.