description/proof of that for product topological space, subspace, open subset of subspace, and element of subproduct, cross section of open subset is open on cross section of subspace
Topics
About: topological space
The table of contents of this article
Starting Context
- The reader knows a definition of product topological space.
- The reader knows a definition of cross section of subset of product set by element of subproduct set.
- The reader admits the local criterion for openness.
- The reader admits the proposition that for any product set, any subset, any subset that contains the 1st subset, and any element of any subproduct, the cross section of the 1st subset by the element is contained in the cross section of the 2nd subset by the element.
- The reader admits the proposition that for any product set, any subsets, and any element of any subproduct, the cross section of the intersection of the subsets by the element is the intersection of the cross sections of the subsets by the element.
Target Context
- The reader will have a description and a proof of the proposition that for any product topological space, any subspace, any open subset of the subspace, and any element of any subproduct, the cross section of the open subset by the element is open on the cross section of the subspace by the element.
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:
\(J'\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{T_{j'} \in \{\text{ the topological spaces }\} \vert j' \in J'\}\):
\(\times_{j' \in J'} T_{j'}\): \(= \text{ the product topological space }\)
\(T\): \(\subseteq \times_{j' \in J'} T_{j'}\), with the subspace topology
\(U\): \(\in \{\text{ the open subsets of } T\}\)
\(J\): \(\subset J'\), such that \(J \neq \emptyset\)
\(\times_{j \in J} t_j\): \(\in \times_{j \in J} T_j\)
\(U_{[\times_{j \in J} t_j]}\): \(= \text{ the cross section }\)
\(T_{[\times_{j \in J} t_j]}\): \(= \text{ the cross section } \subseteq \times_{l \in J' \setminus J} T_l\) with the subspace topology
//
Statements:
\(U_{[\times_{j \in J} t_j]} \in \{\text{ the open subsets of } T_{[\times_{j \in J} t_j]}\}\)
//
2: Note
When \(T = \times_{j' \in J'} T_{j'}\), \(U\) is open on \(\times_{j' \in J'} T_{j'}\), and as \(T_{[\times_{j \in J} t_j]} = \times_{l \in J' \setminus J} T_l\), \(U_{[\times_{j \in J} t_j]}\) is open on \(\times_{l \in J' \setminus J} T_l\).
3: Proof
Whole Strategy: Step 1: for each \(\times_{l \in J' \setminus J} t_l \in U_{[\times_{j \in J} t_j]}\), \(\times_{j' \in J'} t_{j'} \in U\), and take an open neighborhood of \(\times_{j' \in J'} t_{j'}\), \(U_{\times_{j' \in J'} t_{j'}} = U'_{\times_{j' \in J'} t_{j'}} \cap T \subseteq U\), and see that \((U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]} \cap T_{[\times_{j \in J} t_j]} \subseteq U_{[\times_{j \in J} t_j]}\); Step 2: see that \((U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\) is an open neighborhood of \(\times_{l \in J' \setminus J} t_l\) on \(\times_{l \in J' \setminus J} T_l\).
Step 1:
Let \(\times_{l \in J' \setminus J} t_l \in U_{[\times_{j \in J} t_j]}\) be any.
\(\times_{j' \in J'} t_{j'} \in U\).
There is an open neighborhood of \(\times_{j' \in J'} t_{j'}\), \(U_{\times_{j' \in J'} t_{j'}} \subseteq T\), such that \(U_{\times_{j' \in J'} t_{j'}} \subseteq U\), by the local criterion for openness.
\(U_{\times_{j' \in J'} t_{j'}} = U'_{\times_{j' \in J'} t_{j'}} \cap T\) where \(U'_{\times_{j' \in J'} t_{j'}} \subseteq \times_{j' \in J'} T_{j'}\) is an open neighborhood of \(\times_{j' \in J'} t_{j'}\) on \(\times_{j' \in J'} T_{j'}\), by the definition of subspace topology.
\((U'_{\times_{j' \in J'} t_{j'}} \cap T)_{[\times_{j \in J} t_j]} \subseteq U_{[\times_{j \in J} t_j]}\), by the proposition that for any product set, any subset, any subset that contains the 1st subset, and any element of any subproduct, the cross section of the 1st subset by the element is contained in the cross section of the 2nd subset by the element.
But \((U'_{\times_{j' \in J'} t_{j'}} \cap T)_{[\times_{j \in J} t_j]} = (U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]} \cap T_{[\times_{j \in J} t_j]}\), by the proposition that for any product set, any subsets, and any element of any subproduct, the cross section of the intersection of the subsets by the element is the intersection of the cross sections of the subsets by the element.
So, \((U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]} \cap T_{[\times_{j \in J} t_j]} \subseteq U_{[\times_{j \in J} t_j]}\).
Step 2:
Let us see that \((U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\) is an open neighborhood of \(\times_{l \in J' \setminus J} t_l\) on \(\times_{l \in J' \setminus J} T_l\).
\(\times_{l \in J' \setminus J} t_l \in (U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\), because \(\times_{j' \in J'} t_{j'} \in U'_{\times_{j' \in J'} t_{j'}}\).
Let \(\times_{l \in J' \setminus J} u_l \in (U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\) be any.
Taking for each \(j \in J\), \(u_j := t_j\), \(\times_{j' \in J'} u_{j'} \in U'_{\times_{j' \in J'} t_{j'}}\).
By Note for the definition of product topology, there is a \(\times_{j' \in J'} U'_{u_{j'}} \subseteq U'_{\times_{j' \in J'} t_{j'}}\), where \(U'_{u_{j'}} \subseteq T_{j'}\) is an open neighborhood of \(u_{j'}\) such that only finite of \(U'_{u_{j'}}\) s are not \(T_{j'}\) s.
\(\times_{l \in J' \setminus J} U'_{u_l} \subseteq \times_{l \in J' \setminus J} T_l\) is an open neighborhood of \(\times_{l \in J' \setminus J} u_l\), by Note for the definition of product topology: only finite of \(U'_{u_l}\) s are not \(T_l\) s.
Let us see that \(\times_{l \in J' \setminus J} U'_{u_l} \subseteq (U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\).
Let \(\times_{l \in J' \setminus J} v_l \in \times_{l \in J' \setminus J} U'_{u_l}\) be any.
Taking for each \(j \in J\), \(v_j := t_j\), \(\times_{j' \in J'} v_{j'} \in \times_{j' \in J'} U'_{u_{j'}} \subseteq U'_{\times_{j' \in J'} t_{j'}}\).
That means that \(\times_{l \in J' \setminus J} v_l \in (U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\).
So, \(\times_{l \in J' \setminus J} U'_{u_l} \subseteq (U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\).
By the local criterion for openness, \((U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\) is open on \(\times_{l \in J' \setminus J} T_l\).
So, \((U'_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]} \cap T_{[\times_{j \in J} t_j]}\) is open on \(T_{[\times_{j \in J} t_j]}\), by the definition of subspace topology.
By the local criterion for openness, \(U_{[\times_{j \in J} t_j]}\) is open on \(T_{[\times_{j \in J} t_j]}\).
