Confusing definition of filter pushforwards

Stream: maths

[Gareth Ma]

Let $X, Y$ be spaces, $f: X \to Y$ be a map, and $\mathscr{F} \subseteq \mathcal{P}(X)$ be a filter on $X$. I am confused about three(?) different definitions of the pushforward filter $f_*\mathscr{F}$ I saw.

In https://arxiv.org/pdf/1910.12320.pdf, it defines $f_*\mathscr{F} = \{A \subseteq Y : f^{-1}(A) \in \mathscr{F}\}$.

In Mathlib, it defines

def map (f : X → Y) (F : Filter X) : Filter Y where
  sets := preimage f ⁻¹' F.sets

Which is extremely confusing: $f_*\mathscr{F} = (S \mapsto f^{-1}(S))^{-1}(\mathscr{F})$??

In my naive mind, it should simply be defined as $f_*\mathscr{F} = f(\mathscr{F}) = \{f(A) \subseteq Y : A \in \mathscr{F}\}$, or in Lean language, simply f ' F.sets. What goes wrong?

[Yaël Dillies]

Your definition is not a filter!

[Gareth Ma]

pawoegkapwoekhawkepap right. Can I take the filter closure of it then? (Is it then just equivalent)

[Yaël Dillies]

I believe so. Try to prove it!

[Gareth Ma]

Thanks <3

[Gareth Ma]

I guess note for self and others stumbling here, the Mathlib definition and the paper definition is equivalent, because

$\{A : f^{-1}(A) \in \mathscr{F}\} = \{A : (\mathrm{preimage}(f))(A) \in \mathscr{F}\} = (\mathrm{preimage}(f))^{-1}(\mathscr{F})$

And I guess the advantage of Mathlib's definition is that it's purely set theoretical? It's just preimages and images of functions and that's way easy to deal within, rather than some ugly filter on Y that a naive implementation of the paper's definition would require.

[Kevin Buzzard]

It's not images, it's just preimages, which are much easier to work with than images (images have an "exists" in).

[Gareth Ma]

Thanks! never noticed that

[Gareth Ma]

Yaël Dillies said:

I believe so. Try to prove it!

It's either false or I can't prove it.

import Mathlib.Tactic

open Set Filter

variable {α β : Type*} {f : α → β} {F : Filter α}

lemma aux (S : Set β) (h : GenerateSets ((f '' ·) '' F.sets) S) :
    f ⁻¹' S ∈ F := by
  induction' h with h' h' S' T' hT' hST' S' S' T' hS' hT'
  · obtain ⟨x, ⟨hx, rfl⟩⟩ := (mem_image ..).mp h'
    obtain ⟨y, ⟨hy₁, hy₂⟩⟩ := (mem_image ..).mp h'
    rw [← hy₂]
    exact sets_of_superset _ hy₁ (fun a ha ↦ by simp; use a)
  · exact univ_mem
  · cases' subset_iff_ssubset_or_eq.mp hST' with h' h'
    · have h' := aux _ hT' /- well-foundedness problem -/
      exact map.proof_1 f F h' hST'
    · subst h'
      exact S'
  · sorry

I cannot prove the third and fourth case after inducting on h, because one constructor of GeneratingSet is given by

| superset {s t : Set α} : GenerateSets g s → s ⊆ t → GenerateSets g t

Of which I cannot induct over since $\subset$ is not well-founded (I think that's the correct terminology). In other words, there exists (infinite) sets $T$ where there exists an infinite decreasing chain of sets $T \supset T_1 \supset T_2 \supset \cdots$

[Gareth Ma]

(The other direction holds!)

[Jireh Loreaux]

import Mathlib

variable {α β : Type*} {f : α → β} {F : Filter α}

open Filter

lemma Filter.map_eq_generate_image_sets : map f F = generate ((f '' · ) '' F.sets) := by
  apply le_antisymm
  · rw [le_generate_iff]
    rintro _ ⟨s, hs, rfl⟩
    exact image_mem_map hs
  · exact le_map fun s hs ↦ mem_generate_of_mem ⟨s, hs, rfl⟩

[Gareth Ma]

wtf :thinking: I will take a look

[Gareth Ma]

I guess Filter are much more well-behaved than I thought and I should use more of its API :)

[Jireh Loreaux]

By the way, this isn't really the reason you should think of Filter.map as the generalization of the idea of the "image" of a set. The real reason is docs#Filter.map_principal.

[Jireh Loreaux]

And the reason we define Filter.map as we do, instead of via Filter.generate is for the reason Kevin mentioned: it's much easier to work with preimages than with images.

[Jireh Loreaux]

If you've never done it before, you should spend 10 minutes and prove that preimages commute with the usual set operations. Then see why some fail for images. This is an exercise I give all my students in introductory proof courses.

[Gareth Ma]

Is this what it means to be functorial? Or am I confusing this with other notions

[Jireh Loreaux]

There are some functors in play here, but my guess is you're probably confusing this with other contexts in which you've seen the word "functorial". This Stack Exchange post has a brief description of some of the relevant bits.

[Jireh Loreaux]

Do you know how to view any poset as a category?

[Gareth Ma]

Do you just treat set elements as objects and $\leq$ as "edges" (morphisms)?

[Gareth Ma]

But yeah I'm not too familiar with category theory. It's on my TODO list... :sweat:

[Jireh Loreaux]

@Gareth Ma It occurred to me that this is really a statement about filter bases, and so we should have the API to prove it even more simply. And indeed we do!

import Mathlib

variable {α β : Type*} {f : α → β} {F : Filter α} {G : Filter β}

open Filter

example : map f F = generate ((f '' · ) '' F.sets) := F.basis_sets.map f |>.eq_generate

example : comap f G = generate ((f ⁻¹' ·) '' G.sets) := G.basis_sets.comap f |>.eq_generate

[Gareth Ma]

I'm rapidly learning a huge amount of Filter API suddenly hahahaha

[Gareth Ma]

thanks

[Jireh Loreaux]

Another way of looking at this is just that the statement that F = generate s just means that the sets s form a filter basis for F.

[Jireh Loreaux]

which is just:

example : HasBasis (map f F) (· ∈ F.sets) (f '' ·) := F.basis_sets.map f
example : HasBasis (comap f G) (· ∈ G.sets) (f ⁻¹' ·) := G.basis_sets.comap f

[Anatole Dedecker]

Jireh Loreaux said:

Another way of looking at this is just that the statement that F = generate s just means that the sets s form a filter basis for F.

Well, only when s is a filter basis. But indeed the general results are docs#Filter.HasBasis.map and docs#Filter.HasBasis.comap

[Jireh Loreaux]

Anatole Dedecker said:

Well, only when s is a filter basis.

Indeed, that's what I should have said.