A distributive law for filter objects

I recently proved the following conjecture (now a theorem):

Theorem A\cap^{\mathfrak{F}}\bigcup{}^{\mathfrak{F}}S = \bigcup{}^{\mathfrak{F}} \{ A\cap^{\mathfrak{F}} X | X\in S \} for every set A\in\mathscr{P}\mho and every S\in\mathscr{P}\mathfrak{F} where \mathfrak{F} is the set of filter objects on some set \mho.

This theorem is a direct consequence of the following lemma:

Lemma A\cap^{\mathfrak{F}} is a lower adjoint of (\mho\setminus A)\cup^{\mathfrak{F}} for every set A\in\mathscr{P}\mho.

Proof That A\cap^{\mathfrak{F}} and (\mho\setminus A)\cup^{\mathfrak{F}} are monotone is obvious.

We need to prove (for every x,y\in\mathfrak{F}) that

x \subseteq (\mho\setminus A)\cup^{\mathfrak{F}}(A\cap^{\mathfrak{F}}x) and A\cap^{\mathfrak{F}}((\mho\setminus A)\cup^{\mathfrak{F}}y) \subseteq y.

Really, (\mho \setminus A) \cup^{\mathfrak{F}} (A \cap^{\mathfrak{F}} x) =\\ ((\mho \setminus A) \cup^{\mathfrak{F}} A) \cap^{\mathfrak{F}} ((\mho\setminus A) \cup^{\mathfrak{F}} x) =\\ \mho \cap^{\mathfrak{F}} ((\mho\setminus A) \cup^{\mathfrak{F}} x) =\\ (\mho \setminus A) \cup^{\mathfrak{F}} x\supseteq x
and
A \cap^{\mathfrak{F}} ((\mho\setminus A)\cup^{\mathfrak{F}} y) =\\ (A \cap^{\mathfrak{F}} (\mho \setminus A))\cup^{\mathfrak{F}} (A \cap^{\mathfrak{F}} y) =\\ \emptyset \cup^{\mathfrak{F}}(A \cap^{\mathfrak{F}} y) =\\ A \cap^{\mathfrak{F}} y \subseteq y.

Leave a Reply