description/proof of that net with directed index set has universal subnet
Topics
About: topological space
The table of contents of this article
Starting Context
- The reader knows a definition of subnet of net with directed index set.
- The reader knows a definition of universal net with directed index set.
- The reader knows a definition of net with directed index set frequently in subset.
- The reader admits Zorn's lemma.
Target Context
- The reader will have a description and a proof of the proposition that any net with any directed index set has a universal subnet.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(D_2\): \(\in \{\text{ the directed sets }\}\)
\(T\): \(\in \{\text{ the topological spaces }\}\)
\(f_2\): \(: D_2 \to T\)
//
Statements:
\(\exists D_1 \in \{\text{ the directed sets }\}, \exists f_1 : D_1 \to D_2 \in \{\text{ the final maps }\} (f_2 \circ f_1 \in \{\text{ the universal nets }\})\)
//
2: Proof
Whole Strategy: Step 1: define \(S' := \{S \subseteq Pow (T) \vert \forall s \in S (f_2 \in \{\text{ the nets frequently in } s\}) \land \forall s_1, s_2 \in S (s_1 \cap s_2 \in S))\}\) with the relation such that \(s'_1 \le s'_2\) if and only if \(s'_1 \subseteq s'_2\); Step 2: take a maximal \(\widetilde{S} \in S'\), by Zorn's lemma; Step 3: define \(D_1 := \{(\widetilde{s}, d_2) \in \widetilde{S} \times D_2 \vert f_2 (d_2) \in \widetilde{s}\}\) with the relation such that \((\widetilde{s}_1, d_{2, 1}) \le (\widetilde{s}_2, d_{2, 2})\) if and only if \(\widetilde{s}_2 \subseteq \widetilde{s}_1\) and \(d_{2, 1} \le d_{2, 2}\) and define \(f_1: (\widetilde{s}, d_2) \mapsto d_2\); Step 4: see that \(f_2 \circ f_1\) is a universal subnet.
Step 1:
Let us define \(S' := \{S \subseteq Pow (T) \vert \forall s \in S (f_2 \in \{\text{ the nets frequently in } s\}) \land \forall s_1, s_2 \in S (s_1 \cap s_2 \in S))\}\), which is indeed a set, by the subset axiom: \(S \subseteq Pow (T)\) equals \(S \in Pow (Pow (T))\) and the predicate of \(S\) is a legitimate formula.
\(S'\) is not empty, because at least, \(\{T\} \in S'\).
Let us define the relation on \(S'\) such that for each \(s'_1, s'_2 \in S'\), \(s'_1 \le s'_2\) if and only if \(s'_1 \subseteq s'_2\).
Step 2:
For any chain of \(S'\) (means any nonempty subset of \(S'\) such that for any 2 elements of the subset, one of the elements is contained in the other element), \(C = \{S_j \vert j \in J\} \subseteq S'\), \(\cup C \in S'\), because for each \(s \in \cup C\), \(s \in S_j\) for an \(S_j \in S'\), so, \(f_2\) is frequently in \(s\), and for each \(s_1, s_2 \in \cup C\), \(s_1 \in S_j\) and \(s_2 \in S_l\), but as \(S_j \subseteq S_l\) or \(S_l \subseteq S_j\), \(s_1, s_2 \in S_l\) or \(s_1, s_2 \in S_j\), so, \(s_1 \cap s_2 \in S_l \subseteq \cup C\) or \(s_1 \cap s_2 \in S_j \subseteq \cup C\).
So, by Zorn's lemma, there is a maximal element, \(\widetilde{S} \in S'\).
Note that \(T \in \widetilde{S}\), because otherwise, \(\widetilde{S} \cup \{T\} \in S'\), because for each \(s \in \widetilde{S} \cup \{T\}\), \(s \in \widetilde{S}\) or \(s = T\), and when \(s \in \widetilde{S}\), \(f_2\) would be frequently in \(s\), and when \(s = T\), \(f_2\) would be frequently in \(T\), and for each \(s_1, s_2 \in \widetilde{S} \cup \{T\}\), when \(s_1 \neq T\) and \(s_2 \neq T\), \(s_1 \cap s_2 \in \widetilde{S} \subseteq \widetilde{S} \cup \{T\}\), when \(s_1 = T\) and \(s_2 \neq T\), \(s_1 \cap s_2 = s_2 \in \widetilde{S} \subseteq \widetilde{S} \cup \{T\}\), when \(s_1 \neq T\) and \(s_2 = T\), \(s_1 \cap s_2 = s_1 \in \widetilde{S} \subseteq \widetilde{S} \cup \{T\}\), and when \(s_1 = T\) and \(s_2 = T\), \(s_1 \cap s_2 = T \in \widetilde{S} \cup \{T\}\), a contradiction against that \(\widetilde{S}\) is maximal.
Step 3:
Let us define \(D_1 := \{(\widetilde{s}, d_2) \in \widetilde{S} \times D_2 \vert f_2 (d_2) \in \widetilde{s}\}\).
Note that each \(\widetilde{s} \in \widetilde{S}\) appears in \(D_1\), because \(\widetilde{S} \in S'\), which means that there is a \({d_2}'\) such that \(f_2 ({d_2}') \in \widetilde{s}\), so, \((\widetilde{s}, {d_2}') \in D_1\).
Let us define the relation on \(D_1\) such that for each \((\widetilde{s}_1, d_{2, 1}), (\widetilde{s}_2, d_{2, 2}) \in D_1\), \((\widetilde{s}_1, d_{2, 1}) \le ((\widetilde{s}_2, d_{2, 2})\) if and only if \(\widetilde{s}_2 \subseteq \widetilde{s}_1\) and \(d_{2, 1} \le d_{2, 2}\).
\(D_1\) is a directed set, because 1) \((\widetilde{s}, d_2) \leq (\widetilde{s}, d_2)\) for each \((\widetilde{s}, d_2) \in D_1\); 2) if \((\widetilde{s}_1, d_{2, 1}) \leq (\widetilde{s}_2, d_{2, 2})\) and \((\widetilde{s}_2, d_{2, 2}) \leq (\widetilde{s}_3, d_{2, 3})\), \((\widetilde{s}_1, d_{2, 1}) \leq (\widetilde{s}_3, d_{2, 3})\), because \(\widetilde{s}_3 \subseteq \widetilde{s}_2 \subseteq \widetilde{s}_1\) and \(d_{2, 1} \le d_{2, 2} \le d_{2, 3}\); 3) for each pair, \((\widetilde{s}_1, d_{2, 1}), (\widetilde{s}_2, d_{2, 2}) \in D_1\), take \(\widetilde{s}_3 := \widetilde{s}_1 \cap \widetilde{s}_2 \in \widetilde{S}\) and a \(d_{2, 4} \in D_2\) such that \(d_{2, 1}, d_{2, 2} \le d_{2, 4}\) and a \(d_{2, 3} \in D_1\) such that \(d_{2, 4} \le d_{2, 3}\) and \(f_2 (d_{2, 3}) \in \widetilde{s}_3\), then, \((\widetilde{s}_3, d_{2, 3}) \in D_1\) and \((\widetilde{s}_1, d_{2, 1}), (\widetilde{s}_2, d_{2, 2}) \le (\widetilde{s}_3, d_{2, 3})\).
Let us define \(f_1: (\widetilde{s}, d_2) \mapsto d_2\).
\(f_1\) is final, because for each \(d_2 \in D_2\), take any \(\widetilde{s} \in \widetilde{S}\) and a \({d_2}' \in D_2\) such that \(d_2 \le {d_2}'\) and \(f_2 ({d_2}') \in \widetilde{s}\), then, \((\widetilde{s}, {d_2}') \in D_1\), and for each \((\widetilde{s}', {d_2}'') \in D_1\) such that \((\widetilde{s}, {d_2}') \le (\widetilde{s}', {d_2}'')\), \(d_2 \le f_1 ((\widetilde{s}', {d_2}'')) = {d_2}''\), because \(d_2 \le {d_2}' \le {d_2}''\).
So, \(f_2 \circ f_1\) is a subnet.
Step 4:
Let us see that \(f_2 \circ f_1\) is a universal subnet.
Let \(S \subseteq T\) be any.
If \(f_2 \circ f_1\) is eventually in \(T \setminus S\), the conditions for \(f_2 \circ f_1\) to be universal will be satisfied for \(S\).
Let us suppose otherwise.
That implies that there is no \(d_1 \in D_1\) such that for each \({d_1}' \in D_1\) such that \(d_1 \le {d_1}'\), \(f_2 \circ f_1 ({d_1}') \in T \setminus S\), which implies that for each \(d_1 \in D_1\), there is a \({d_1}' \in D_1\) such that \(d_1 \le {d_1}'\) and \(f_2 \circ f_1 ({d_1}') \notin T \setminus S\), which implies that \(f_2 \circ f_1 ({d_1}') \in S\), which means that \(f_2 \circ f_1\) is frequently in \(S\).
Let \(\widetilde{s} \in \widetilde{S}\) be any.
Let \(d_2 \in D_2\) be any.
There is a \((\widetilde{s}, {d_2}') \in D_1\) such that \(d_2 \le {d_2}'\).
There is a \((\widetilde{s}', {d_2}'') \in D_1\) such that \((\widetilde{s}, {d_2}') \le (\widetilde{s}', {d_2}'')\) and \(f_2 \circ f_1 ((\widetilde{s}', {d_2}'')) = f_2 ({d_2}'') \in S\), because \(f_2 \circ f_1\) is frequently in \(S\).
\(f_2 ({d_2}'') \in \widetilde{s}' \cap S \subseteq \widetilde{s} \cap S\), which means that \(f_2\) is frequently in \(\widetilde{s} \cap S\): \(d_2 \le {d_2}' \le {d_2}''\).
Let us think of \(\widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\).
\(\widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\} \in S'\), because for each \(\widetilde{s} \cap S\), \(f_2\) is frequently in \(\widetilde{s} \cap S\) and for each \(s_1, s_2 \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\), when \(s_1 \in \widetilde{S}\) and \(s_2 \in \widetilde{S}\), \(s_1 \cap s_2 \in \widetilde{S} \subseteq \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\), when \(s_1 = \widetilde{s} \cap S\) and \(s_2 \in \widetilde{S}\), \(s_1 \cap s_2 = \widetilde{s} \cap S \cap s_2 = (\widetilde{s} \cap s_2) \cap S \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\), when \(s_1 \in \widetilde{S}\) and \(s_2 = \widetilde{s} \cap S\), \(s_1 \cap s_2 = s_1 \cap \widetilde{s} \cap S = (s_1 \cap \widetilde{s}) \cap S \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\), and when \(s_1 = \widetilde{s}' \cap S\) and \(s_2 = \widetilde{s} \cap S\), \(s_1 \cap s_2 = \widetilde{s} \cap S \cap \widetilde{s}' \cap S = (\widetilde{s} \cap \widetilde{s}') \cap S \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\).
But as \(\widetilde{S}\) is maximal, \(\widetilde{S} = \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\).
Especially, \(T \cap S = S \in \widetilde{S}\): \(T \in \widetilde{S}\).
If \(f_2 \circ f_1\) was frequently in \(T \setminus S\), \(T \setminus S \in \widetilde{S}\), because the logic for \(S \in \widetilde{S}\) was based only on the assumption that \(S\) was a subset in which \(f_2 \circ f_1\) was frequent and \(T \setminus S\) would be such a subset. Then, \(S \cap (T \setminus S) = \emptyset \in \widetilde{S}\), a contradiction, because \(f_2\) was not frequently in \(\emptyset\).
So, \(f_2 \circ f_1\) is not frequently in \(T \setminus S\).
That means that for a \(d_1 \in D_1\), there is no \({d_1}' \in D_1\) such that \(d_1 \le {d_1}'\) and \(f_2 \circ f_1 ({d_1}') \in T \setminus S\), which implies that for each \({d_1}' \in D_1\) such that \(d_1 \le {d_1}'\), \(f_2 \circ f_1 ({d_1}') \notin T \setminus S\), which means that \(f_2 \circ f_1 ({d_1}') \in S\).
That means that \(f_2 \circ f_1\) is eventually in \(S\).
So, for each \(S\), \(f_2 \circ f_1\) is eventually in \(T \setminus S\) or is eventually in \(S\).
So, \(f_2 \circ f_1\) is universal.
