blob: 59b647f7971bdce8062e205b04d5d8b111355e3d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
\import{set.tex}
\import{set/powerset.tex}
\section{Filters}
\subsection{Definition and basic properties of filters}
\begin{abbreviation}\label{upwardclosed}
$F$ is upward-closed in $S$ iff
for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$.
\end{abbreviation}
\begin{definition}\label{filter}
$F$ is a filter on $S$ iff
$F$ is a family of subsets of $S$
and $S\in F$
and $\emptyset\notin F$
and $F$ is closed under binary intersections
and $F$ is upward-closed in $S$.
\end{definition}
\begin{proposition}\label{filter_ext_complement}
Let $F, G$ be filters on $S$.
Suppose for all $A\subseteq S$ we have $S\setminus A\in F$ iff $S\setminus A\in G$.
Then $F = G$.
\end{proposition}
\begin{proof}
Follows by set extensionality.
\end{proof}
\begin{proposition}\label{filter_inter_in_iff}
Let $F$ be a filter on $S$.
Suppose $A, B\subseteq S$.
Then $A\inter B\in F$ iff $A, B\in F$.
\end{proposition}
\begin{proof}
We have $A\inter B\subseteq A, B$.
Follows by \cref{filter}.
\end{proof}
\begin{proposition}\label{filter_setminus_in}
Let $F$ be a filter on $S$.
Suppose $A\in F$.
Suppose $B\subseteq S$ and $S\setminus B\in F$.
Then $A\setminus B\in F$.
\end{proposition}
\begin{proof}
We have $A\subseteq S$.
Thus $A\setminus B = A\inter (S\setminus B)$ by \cref{setminus_eq_inter_complement}.
Now $S\setminus B\subseteq S$.
Follows by \cref{filter_inter_in_iff}.
\end{proof}
\subsection{Principal filters over a set}
\begin{definition}\label{principalfilter}
$\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$.
\end{definition}
\begin{proposition}\label{principalfilter_is_filter}
Suppose $A\subseteq S$.
Suppose $A$ is inhabited.
Then $\principalfilter{S}{A}$ is a filter on $S$.
\end{proposition}
\begin{proof}
$S$ is inhabited. % since $A$ is inhabited and $A\subseteq S$.
$\principalfilter{S}{A}$ is a family of subsets of $S$.
$S\in \principalfilter{S}{A}$.
$\emptyset\notin \principalfilter{S}{A}$.
$\principalfilter{S}{A}$ is closed under binary intersections.
$\principalfilter{S}{A}$ is upward-closed in $S$.
Follows by \cref{filter}.
\end{proof}
\begin{proposition}\label{principalfilter_elem_generator}
Suppose $A\subseteq S$.
$A\in\principalfilter{S}{A}$.
\end{proposition}
\begin{proof}
$A\in\pow{S}$.
\end{proof}
\begin{proposition}\label{principalfilter_notelem_implies_notsupseteq}
Let $X\in\pow{S}$.
Suppose $X\notin\principalfilter{S}{A}$.
Then $A\not\subseteq X$.
\end{proposition}
\begin{definition}\label{maximalfilter}
$F$ is a maximal filter on $S$ iff
$F$ is a filter on $S$ and there exists no filter $F'$ on $S$ such that $F\subset F'$.
\end{definition}
\begin{proposition}\label{principalfilter_singleton_is_filter}
Suppose $a\in S$.
Then $\principalfilter{S}{\{a\}}$ is a filter on $S$.
\end{proposition}
\begin{proof}
$\{a\}\subseteq S$.
$\{a\}$ is inhabited.
Follows by \cref{principalfilter_is_filter}.
\end{proof}
\begin{proposition}\label{principalfilter_singleton_is_maximal_filter}
Suppose $a\in S$.
Then $\principalfilter{S}{\{a\}}$ is a maximal filter on $S$.
\end{proposition}
\begin{proof}
$\{a\}\subseteq S$.
$\{a\}$ is inhabited.
Thus $\principalfilter{S}{\{a\}}$ is a filter on $S$ by \cref{principalfilter_is_filter}.
It suffices to show that there exists no filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$.
Suppose not.
Take a filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$.
Take $X\in F'$ such that $X\notin \principalfilter{S}{\{a\}}$.
$X\in\pow{S}$.
Thus $\{a\}\not\subseteq X$ by \cref{principalfilter_notelem_implies_notsupseteq}.
Thus $a\notin X$.
$\{a\}\in F'$
% TODO clean
by \cref{principalfilter,elem_subseteq,union_intro_left,subset,union_absorb_subseteq_left,subseteq_refl,powerset_intro}.
Thus $\emptyset = X\inter \{a\}$.
Hence $\emptyset\in F'$ by \cref{filter}.
Follows by \hyperref[filter]{contradiction to the definition of a filter}.
\end{proof}
|
