How do these definitions of filters coincide?

Question

A definition of a filter:

Given a non-empty set $S$, a filter $F$ on $S$ is a non-empty collection of subsets of $S$ that satisfy

(i) $\emptyset\notin F$

(ii) If $A_1,A_2\in F$ then $A_1\cap A_1\in F$

(iii) If $A\subset B$ and $A\in F$, then $B\in F$

Now given $f:X\to Y$ a function between two topological spaces, a filter $F$ on $X$, one defines

$f(F)=\{B\subset Y:f^{-1}(B)\in F\}$

It's easy to see that this defines a filter, but later on there is another definition given in terms of filter basis:

$f(F)$ is a filter on $Y$ generated by the basis $G=\{f(A):A\in F\}$

I don't understand how these two definitions are equivalent.

Given $B\in f(F)$ in a sense of first definition, $f^{-1}(B)\in F$. But $B=f(f^{-1}(B))$ and hence $B\in G$. So in fact $f(F)\subset G$; but the filter generated by $G$ must contain $G$, so in fact if the two definitions agree then $f(F)=G$.

But I don't see how $G$ is necessarily a filter itself: there is no guarantee that interseion of two sets in $G$ is again in $G$, because images do not commute under intersections in general.

Answer 1

Given $A,B \in F$, then $D = f(A \cap B) \subset f(A) \cap f(B)$. Since $D \in G$,
this shows that $G$ is down directed which is sufficient for $G$ to be a
filter base.

Answer 2

Let $\mathcal{G} = \{B \subseteq Y: f^{-1}[B] \in \mathcal{F}\}$ and $\mathcal{G}' = \{B \subseteq Y: \exists A \in \mathcal{F}: f[A] \subseteq B\}$.

The first is your original definition of $f[\mathcal{F}]$, while the second one is the filter generated by the collection $\{f[A]: A \in \mathcal{F}\}$.

To see the latter is a filter: properties (iii) and (i) are obvious: if $B$ contains some $f[A]$ ($A \in \mathcal{F}$) and $B \subseteq B'$, $B'$ contains that same $f[A]$ so is also in $\mathcal{G}'$. As $A \neq \emptyset$, for all $A \in \mathcal{F}$, all sets $f[A]$ (and their enlargements too) are also non-empty. If $B_1, B_2 \in \mathcal{G}'$. find $A_1 ,A_2 \in \mathcal{F}$ with $f[A_1] \subseteq B_1, f[A_2] \subseteq B_2$. But then $A_1 \cap A_2 \in \mathcal{F}$, and $f[A_1 \cap A_2] \subseteq f[A_1] \cap f[A_2] \subseteq B_1 \cap B_2$, so $B_1 \cap B_2 \in \mathcal{G}'$, using $A_1 \cap A_2$ as a witness.

Why are these filters the same? Let $B \in \mathcal{G}$. Then $f^{-1}[B] \in \mathcal{F}$ and $f[f^{-1}[B]] \subseteq B$, so taking $A = f^{-1}[B]$ we have that $B \in \mathcal{G}'$.

Let $B \in \mathcal{G}'$, so $f[A] \subseteq B$ for some $A \in \mathcal{F}$. But then $A \subseteq f^{-1}[B]$ and by property (iii) of the filter definition, $f^{-1}[B] \in \mathcal{F}$. So $B \in \mathcal{G}$.

So we have equality.