Cofinite filters and directed set filters

We assume that E is an infinite set.

Cofinite filters

The cofinite filter \mathcal F_{\text {cof}} over E is the set of subsets F of E such that E \backslash F is finite.

Since E is infinite, \emptyset is not in \mathcal F_{\text {cof}}.

It is trivial to check that any superset in E of an element of \mathcal F_{\text {cof}} is in \mathcal F_{\text {cof}}, and that the intersection of any two elements of \mathcal F_{\text {cof}} is in \mathcal F_{\text {cof}}. Thus \mathcal F_{\text {cof}} is a filter over E.

The cofinite filter over E is defined independently of any ordering on E.


If \mathcal F is an ultrafilter over E, then either it is a principal ultrafilter, or finer than the cofinite filter, but not both.


Directed set filters

Directed set = ensemble ordonné filtrant, a partially ordered set (E, \le) such that for any x, y \in E, there exists a \in E with x \le a and y \le a.

The directed set filter \mathcal F_{\text{dsf}} is defined by the filter base \mathcal B_{\text{dsf}} = \{ \ \{x \in E\ |\ a \le x \}\ \}_{a \in E}; that is that the elements of \mathcal B_{\text{dsf}} are the “segments” of all elements of E greater than any a \in E.


If (E, \le) has no maximal element (that is, for all elements of E, there is another element of E that is strictly greater), then the directed set filter is finer than the cofinite filter.


Let F be an element of the cofinite filter over E.

Then E \backslash F is finite. Since (E, \le) is a directed set, there exists an a_1 \in E that is greater than all elements of E \backslash F. There exists an a \in E that is strictly greater than all elements of E \backslash F. All elements in the segment \{x \in E\ |\ a \le x \} are strictly greater, hence different from, all elements of E \backslash F, that is, that they belong to F. Thus \{x \in E\ |\ a \le x \} \subseteq F, and since \{x \in E\ |\ a \le x \} belongs to the filter base \mathcal B_{\text{dsf}}, F belongs to the filter \mathcal F_{\text{dsf}}.

Thus the cofinite filter is a subset of the directed set filter.