theory Topology_ZF_8 imports Topology_ZF_6 EquivClass1
begin
Suppose \(T\) is a topology, \(r\) is an equivalence relation on \(X = \bigcup T\) and \(P_r : X \rightarrow X/r\) maps an element of \(X\) to its equivalence class \(r\{x \}\). Then we can define a topology (on \(X/r\)) by taking the collection of those subsets \(V\) of \(X/r\) for which the inverse image by the projection \(P_r\) is in \(T\). This is the weakest topology on \(X/r\) such that \(P_r\) is continuous. In this theory we consider a seemingly more general situation where we start with a topology \(T\) on \(X=\bigcup T\) and a surjection \(f:X\rightarrow Y\) and define a topology on \(Y\) by taking those subsets \(V\) of \(Y\) for which the inverse image by the mapping \(f\) is in \(T\). Turns out that this construction is in a way equivalent to the previous one as the topology defined this way is homeomorphic to the topology defined by the equivalence relation \(r_f\) on \(X\) that relates two elements of \(X\) if \(f\) has the same value on them.
Definition of quotient topology
In this section we define the quotient topology generated by a topology \(T\) and a surjection \(f:\bigcup T \rightarrow Y\), and show its basic properties.
For a topological space \(X=\bigcup T\) and a surjection \(f:X\rightarrow Y\) we define \( \text{ quotient topology in } Y\text{ by } f \) as the collection of subsets of \(Y\) whose inverse images by \(f\) are open.
definition (in topology0)
\( f\in \text{surj}(\bigcup T,Y) \Longrightarrow \text{ quotient topology in } Y\text{ by } f \equiv \) \( \{U\in Pow(Y).\ f^{-1}U\in T\} \)
Outside of the topology0 context we will indicate also the generating topology and write \( \text{ quotient topology in } Y\text{ by } f\text{ from } X \).
abbreviation
\( \text{ quotient topology in } Y\text{ by } f\text{ from } T \equiv topology0.\ \text{QuotientTop}(T,Y,f) \)
The quotient topology is indeed a topology.
theorem (in topology0) quotientTop_is_top:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( (\text{ quotient topology in } Y\text{ by } f) \text{ is a topology } \)proof have \( (\text{ quotient topology in } Y\text{ by } f)=\{U \in Pow(Y) .\ f^{-1}(U) \in T\} \) using QuotientTop_def, assms
moreover {
}
moreover {
}
ultimately show \( thesis \) using IsATopology_def
qed
fix \( M \) \( x \) \( B \)
assume M: \( M \subseteq \{U \in Pow(Y) .\ f^{-1}(U) \in T\} \)
then have \( \bigcup M\subseteq Y \)
moreover
}
}
have A1: \( f^{-1}(\bigcup M) = (\bigcup y\in (\bigcup M).\ f^{-1}\{y\}) \) using vimage_eq_UN
moreover {
fix \( A \)
assume \( A\in M \)
with M have \( A\in Pow(Y) \), \( f^{-1}(A) \in T \)
have \( f^{-1}(A) = (\bigcup y\in A.\ f^{-1}\{y\}) \) using vimage_eq_UN
hence \( (\bigcup A\in M.\ f^{-1}(A)) = (\bigcup y\in \bigcup M.\ f^{-1}\{y\}) \)
with A1 have A2: \( f^{-1}(\bigcup M)=\bigcup \{f^{-1} A.\ A\in M\} \)
moreover {
fix \( A \)
assume \( A\in M \)
with M have \( f^{-1}(A)\in T \)
hence \( \{f^{-1}(A).\ A\in M\}\subseteq T \)
then have \( (\bigcup \{f^{-1}(A).\ A\in M\})\in T \) using topSpaceAssum unfolding IsATopology_def
with A2 have \( (f^{-1}(\bigcup M))\in T \)
ultimately have \( \bigcup M\in \{U\in Pow(Y).\ f^{-1}U\in T\} \)
fix \( U \) \( V \)
assume \( U \in \{U\in Pow(Y).\ f^{-1}U\in T\} \), \( V\in \{U\in Pow(Y).\ f^{-1}U\in T\} \)
then have \( U\in Pow(Y) \), \( V\in Pow(Y) \), \( f^{-1}U\in T \), \( f^{-1}V\in T \)
then have \( f^{-1}(U\cap V)\in T \) using topSpaceAssum, invim_inter_inter_invim, assms unfolding IsATopology_def, surj_def
with \( U\in Pow(Y) \), \( V\in Pow(Y) \) have \( U\cap V\in \{U\in Pow(Y).\ f^{-1}(U)\in T\} \)
The quotient function is continuous.
lemma (in topology0) quotient_func_cont:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( \text{IsContinuous}(T,(\text{ quotient topology in } Y\text{ by } f),f) \) unfolding IsContinuous_def using QuotientTop_def, assmsOne of the important properties of this topology, is that a function from the quotient space is continuous iff the composition with the quotient function is continuous.
theorem (in two_top_spaces0) cont_quotient_top:
assumes \( h\in \text{surj}(\bigcup \tau _1,Y) \), \( g:Y\rightarrow \bigcup \tau _2 \), \( \text{IsContinuous}(\tau _1,\tau _2,g\circ h) \)
shows \( \text{IsContinuous}((\text{ quotient topology in } Y\text{ by } h\text{ from } \tau _1),\tau _2,g) \)proof{
}
fix \( U \)
assume \( U\in \tau _2 \)
with assms(3) have \( (g\circ h)^{-1}(U)\in \tau _1 \) unfolding IsContinuous_def
then have \( h^{-1}(g^{-1}(U))\in \tau _1 \) using vimage_comp
with assms(1) have \( g^{-1}(U)\in (\text{ quotient topology in } Y\text{ by } h\text{ from } \tau _1) \) using QuotientTop_def, tau1_is_top, func1_1_L3, assms(2) unfolding topology0_def
then show \( thesis \) unfolding IsContinuous_def
qed
The underlying set of the quotient topology is \(Y\).
lemma (in topology0) total_quo_func:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( (\bigcup (\text{ quotient topology in } Y\text{ by } f))=Y \)proof from assms have \( f^{-1}Y=\bigcup T \) using func1_1_L4 unfolding surj_def
moreover
qed
have \( \bigcup T\in T \) using topSpaceAssum unfolding IsATopology_def
ultimately have \( Y\in (\text{ quotient topology in }Y\{by\}f\{from\}T) \) using QuotientTop_def, assms
then show \( thesis \) using QuotientTop_def, assms
Quotient topologies from equivalence relations
In this section we will show that the quotient topologies come from an equivalence relation.
The quotient projection \(b\mapsto r\{ b\}\) is a function that maps the domain of the relation to the quotient. Note we do not need to assume that \(r\) is an equivalence relation.
lemma quotient_proj_fun:
shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}:A\rightarrow A//r \) unfolding Pi_def, function_def, domain_def unfolding quotient_defThe quotient projection is a surjection. Again \(r\) does not need to be an equivalence relation here
lemma quotient_proj_surj:
shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}\in \text{surj}(A,A//r) \)proof{
}
fix \( y \)
assume \( y\in A//r \)
then obtain \( x \) where \( x\in A \), \( y=r\{x\} \) unfolding quotient_def
then have \( \exists x\in A.\ \{\langle b,r\{b\}\rangle .\ b\in A\}(x) = y \) using ZF_fun_from_tot_val1
then show \( thesis \) using quotient_proj_fun unfolding surj_def
qed
The inverse image of a subset \(U\) of the quotient by the quotient projection is the union of \(U\). Note since \(U\) is a subset of \(A/r\) it is a collection of equivalence classes.
lemma preim_equi_proj:
assumes \( U\subseteq A//r \), \( \text{equiv}(A,r) \)
shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}(U) = \bigcup U \)proof{
}
}
fix \( y \)
assume \( y\in \bigcup U \)
then obtain \( V \) where \( y\in V \) and \( V\in U \)
with assms have \( y \in \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}(U) \) using EquivClass_1_L1, EquivClass_1_L2
thus \( \bigcup U\subseteq \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}U \)
{
fix \( y \)
assume \( y\in \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}U \)
then have yy: \( y\in \{x\in A.\ r\{x\}\in U\} \)
hence \( r\{y\}\in U \)
moreover
from yy have \( y\in r\{y\} \) using assms, equiv_class_self
ultimately have \( y\in \bigcup U \)
thus \( \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}U\subseteq \bigcup U \)
qed
Now we define what a quotient topology from an equivalence relation is:
definition (in topology0)
\( \text{equiv}(\bigcup T,r)\Longrightarrow (\text{ quotient by } r) \equiv \text{ quotient topology in } (\bigcup T)//r\text{ by } \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \)
Outside of the topology0 context we need to indicate the original topology.
abbreviation
\( T \text{ quotient by } r \equiv topology0.\ \text{EquivQuo}(T,r) \)
First, another description of the topology (more intuitive):
theorem (in topology0) quotient_equiv_rel:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( (\text{ quotient by }r)=\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\} \)proof have \( (\text{ quotient topology in }(\bigcup T)//r\{by}\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\})=\)
\( \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\\} \) using QuotientTop_def, quotient_proj_surj
moreover
qed
have \( \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}=\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\} \)proof
ultimately show \( thesis \) using EquivQuo_def, assms
{
}
}
fix \( U \)
assume \( U\in \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\} \)
with assms have \( U\in \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\} \) using preim_equi_proj
thus \( \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}\subseteq \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\} \)
{
fix \( U \)
assume \( U\in \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\} \)
with assms have \( U\in \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\} \) using preim_equi_proj
thus \( \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}\subseteq \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\} \)
qed
We apply previous results to this topology.
theorem (in topology0) total_quo_equi:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( \bigcup (\text{ quotient by }r)=(\bigcup T)//r \) using total_quo_func, quotient_proj_surj, EquivQuo_def, assmsThe quotient by an equivalence relation is indeed a topology.
theorem (in topology0) equiv_quo_is_top:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( (\text{ quotient by }r)\text{ is a topology } \) using quotientTop_is_top, quotient_proj_surj, EquivQuo_def, assmsThe next theorem is the main result of this section: all quotient topologies arise from an equivalence relation given by the quotient function \(f:X\to Y\). This means that any quotient topology is homeomorphic to a topology given by an equivalence relation quotient.
theorem (in topology0) equiv_quotient_top:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
defines \( r\equiv \{\langle x,y\rangle \in \bigcup T\times \bigcup T.\ f(x)=f(y)\} \)
defines \( g\equiv \{\langle y,f^{-1}\{y\}\rangle .\ y\in Y\} \)
shows \( \text{equiv}(\bigcup T,r) \) and \( \text{IsAhomeomorphism}((\text{ quotient topology in }Y\{by\}f),(\text{ quotient by }r),g) \)proof from assms(1) have ff: \( f:\bigcup T\rightarrow Y \) unfolding surj_def
from assms(2) show B: \( \text{equiv}(\bigcup T,r) \) unfolding equiv_def, refl_def, sym_def, trans_def, r_def
have gg: \( g:Y\rightarrow ((\bigcup T)//r) \)proof
{
}
}
fix \( B \)
assume \( B\in g \)
then obtain \( y \) where Y: \( y\in Y \), \( B=\langle y,f^{-1}\{y\}\rangle \) unfolding g_def
then have \( f^{-1}\{y\}\subseteq \bigcup T \) using func1_1_L3, ff
then have eq: \( f^{-1}\{y\}=\{x\in \bigcup T.\ \langle x,y\rangle \in f\} \) using vimage_iff
from assms(1), Y obtain \( A \) where A1: \( A\in \bigcup T \), \( f(A)=y \) unfolding surj_def
with ff have A: \( A \in f^{-1}\{y\} \) using func1_1_L15
{
fix \( t \)
assume \( t\in f^{-1}\{y\} \)
with A, eq have \( t\in \bigcup T \), \( A\in \bigcup T \), \( \langle t,y\rangle \in f \), \( \langle A,y\rangle \in f \)
then have \( ft=fA \) using apply_equality, assms(1) unfolding surj_def
with assms(2), \( t\in \bigcup T \), \( A\in \bigcup T \) have \( \langle A,t\rangle \in r \)
then have \( t\in r\{A\} \) using image_iff
hence \( f^{-1}\{y\}\subseteq r\{A\} \)
moreover {
}
fix \( t \)
assume \( t\in r\{A\} \)
with assms(2) have un: \( t\in \bigcup T \), \( A\in \bigcup T \) and eq2: \( f(t)=f(A) \) using image_iff
from ff, un have \( \langle t,f(t)\rangle \in f \) using func1_1_L5A(1)
with eq2, A1, un, eq have \( t\in f^{-1}\{y\} \)
hence \( r\{A\}\subseteq f^{-1}\{y\} \)
ultimately have \( f^{-1}\{y\}=r\{A\} \)
with A1(1) have \( f^{-1}\{y\} \in (\bigcup T)//r \) using A1(1) unfolding quotient_def
with Y have \( B\in Y\times (\bigcup T)//r \)
then show \( thesis \) unfolding Pi_def, function_def, domain_def, g_def
qed
then have gg2: \( g:Y\rightarrow (\bigcup (\text{ quotient by }r)) \) using total_quo_equi, B
{
fix \( s \)
assume S: \( s\in (\text{ quotient topology in }Y\{by\}f) \)
then have \( s\in Pow(Y) \) and P: \( f^{-1}(s)\in T \) using QuotientTop_def, topSpaceAssum, assms(1)
have \( f^{-1}s=(\bigcup y\in s.\ f^{-1}\{y\}) \) using vimage_eq_UN
moreover
from \( s\in Pow(Y) \) have \( \forall y\in s.\ \langle y,f^{-1}\{y\}\rangle \in g \) unfolding g_def
then have \( \forall y\in s.\ gy=f^{-1}\{y\} \) using apply_equality, gg
ultimately have \( f^{-1}s=(\bigcup y\in s.\ gy) \)
with P have \( (\bigcup y\in s.\ gy)\in T \)
moreover
from \( s\in Pow(Y) \) have \( \forall y\in s.\ gy\in (\bigcup T)//r \) using apply_type, gg
ultimately have \( \{gy.\ y\in s\}\in (\text{ quotient by }r) \) using quotient_equiv_rel, B
with \( s\in Pow(Y) \) have \( gs\in (\text{ quotient by }r) \) using func_imagedef, gg
hence gopen: \( \forall s\in (\text{ quotient topology in }Y\{by\}f).\ gs\in (T\text{ quotient by }r) \)
have pr_fun: \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}:\bigcup T\rightarrow (\bigcup T)//r \) using quotient_proj_fun
{
fix \( b \)
assume b: \( b\in \bigcup T \)
have bY: \( f(b)\in Y \) using apply_funtype, ff, b
with b have com: \( (g\circ f)b=g(fb) \) using comp_fun_apply, ff
from bY have pg: \( \langle fb,f^{-1}(\{fb\})\rangle \in g \) unfolding g_def
then have \( g(fb) = f^{-1}(\{fb\}) \) using apply_equality, gg
with com have comeq: \( (g\circ f)b=f^{-1}(\{fb\}) \)
from b have A: \( f\{b\}=\{fb\} \), \( \{b\}\subseteq \bigcup T \) using func_imagedef, ff
from A(2) have \( b \in f^{-1}(f \{b\}) \) using func1_1_L9, ff
with A(1) have \( b\in f^{-1}(\{fb\}) \)
moreover
from pg have \( f^{-1}(\{fb\})\in (\bigcup T)//r \) using gg unfolding Pi_def
ultimately have \( r\{b\}=f^{-1}(\{fb\}) \) using EquivClass_1_L2, B
then have \( (g\circ f)b=r\{b\} \) using comeq
moreover
from b, pr_fun have \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}b=r\{b\} \) using apply_equality
ultimately have \( (g\circ f)b=\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}b \)
hence reg: \( \forall b\in \bigcup T.\ (g\circ f)(b)=\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(b) \)
moreover
{
have compp: \( g\circ f\in \bigcup T\rightarrow (\bigcup T)//r \) using comp_fun, ff, gg
moreover from compp, pr_fun, reg have feq: \( (g\circ f)=\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \) by (rule func_eq )
then have \( \text{IsContinuous}(T,\text{ quotient by }r,(g\circ f)) \) using quotient_func_cont, quotient_proj_surj, EquivQuo_def, topSpaceAssum, B
moreover have \( (g\circ f):\bigcup T\rightarrow \bigcup (\text{ quotient by }r) \) using comp_fun, ff, gg2
ultimately have gcont: \( \text{IsContinuous}(\text{ quotient topology in }Y\{by\}f,\text{ quotient by }r,g) \) using cont_quotient_top, assms(1), gg2, topSpaceAssum, equiv_quo_is_top, B unfolding two_top_spaces0_def
fix \( x \) \( y \)
assume T: \( x\in Y \), \( y\in Y \), \( g(x)=g(y) \)
with assms(3) have \( f(f^{-1}\{x\})=f(f^{-1}\{y\}) \) using apply_equality, gg
with assms(1), T(1,2) have \( x=y \) using surj_image_vimage
with gg2 have \( g\in \text{inj}(Y,\bigcup (\text{ quotient by }r)) \) unfolding inj_def
moreover
qed
have \( g\circ f\in \text{surj}(\bigcup T, (\bigcup T)//r) \) using feq, quotient_proj_surj
with ff, gg, B have \( g\in \text{surj}(Y,\bigcup (T\text{ quotient by }r)) \) using comp_mem_surjD1, total_quo_equi
ultimately have \( g\in \text{bij}(\bigcup (\text{ quotient topology in }Y\{by\}f),\bigcup (\text{ quotient by }r)) \) unfolding bij_def using total_quo_func, assms(1)
with gcont, gopen show \( \text{IsAhomeomorphism}((\text{ quotient topology in }Y\{by\}f),(\text{ quotient by }r),g) \) using bij_cont_open_homeo
The mapping \(\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle\) is a function that maps the product of the carrier by itself to the product of the quotients. Note \(r\) does not have to be an equivalence relation.
lemma product_equiv_rel_fun:
shows \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}:(\bigcup T\times \bigcup T)\rightarrow ((\bigcup T)//r\times (\bigcup T)//r) \)proof have \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}\in \bigcup T\rightarrow (\bigcup T)//r \) using quotient_proj_fun
moreover
qed
have \( \forall A\in \bigcup T.\ \langle A,r\{A\}\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \)
ultimately have \( \forall A\in \bigcup T.\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}A=r\{A\} \) using apply_equality
hence \( \{\langle \langle b,c\rangle ,r\{b\},r\{c\}\rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} = \)
\( \{\langle \langle x,y\rangle ,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(x),\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(y)\rangle .\ \langle x,y\rangle \in \bigcup T\times \bigcup T\} \)
then show \( thesis \) using prod_fun, quotient_proj_fun
The mapping \(\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle\) is a surjection of the product of the carrier by itself onto the carrier of the product topology. Again \(r\) does not have to be an equivalence relation for this.
lemma (in topology0) prod_equiv_rel_surj:
shows \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}\in \text{surj}(\bigcup (T\times _tT),((\bigcup T)//r\times (\bigcup T)//r)) \)proof have fun: \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}:(\bigcup T\times \bigcup T)\rightarrow ((\bigcup T)//r\times (\bigcup T)//r) \) using product_equiv_rel_fun
moreover {
}
ultimately show \( thesis \) unfolding surj_def using Top_1_4_T1(3), topSpaceAssum
qed
fix \( M \)
assume \( M\in ((\bigcup T)//r\times (\bigcup T)//r) \)
then obtain \( M1 \) \( M2 \) where M: \( M=\langle M1,M2\rangle \), \( M1\in (\bigcup T)//r \), \( M2\in (\bigcup T)//r \)
then obtain \( m1 \) \( m2 \) where m: \( m1\in \bigcup T \), \( m2\in \bigcup T \), \( M1=r\{m1\} \), \( M2=r\{m2\} \) unfolding quotient_def
then have mm: \( \langle m1,m2\rangle \in (\bigcup T\times \bigcup T) \)
hence \( \langle \langle m1,m2\rangle ,\langle r\{m1\},r\{m2\}\rangle \rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} \)
with fun have \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}\langle m1,m2\rangle =\langle r\{m1\},r\{m2\}\rangle \) using apply_equality
with M(1), m(3,4), mm have \( \exists R\in (\bigcup T\times \bigcup T).\ \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}(R) = M \)
The product quotient projection (i.e. the mapping the mapping \(\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle\) is continuous.
lemma (in topology0) product_quo_fun:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( \text{IsContinuous}(T\times _tT,(\text{ quotient by } r)\times _t(\text{ quotient by } r),\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}) \)proof have \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}:\bigcup T\rightarrow (\bigcup T)//r \) using quotient_proj_fun
moreover
qed
have \( \forall A\in \bigcup T.\ \langle A,r\{A\}\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \)
ultimately have \( \forall A\in \bigcup T.\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}A=r\{A\} \) using apply_equality
hence IN: \( \{\langle \langle b,c\rangle ,r\{b\},r\{c\}\rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} = \)
\( \{\langle \langle x,y\rangle ,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(x),\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(y)\rangle .\ \langle x,y\rangle \in \bigcup T\times \bigcup T\} \)
with assms have cont: \( \text{IsContinuous}(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}) \) using quotient_func_cont, quotient_proj_surj, EquivQuo_def
with assms have tot: \( \bigcup (T\text{ quotient by }r) = (\bigcup T) // r \) and top: \( (\text{ quotient by }r) \text{ is a topology } \) using total_quo_equi, equiv_quo_is_top
then have fun: \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}:\bigcup T\rightarrow \bigcup (\text{ quotient by }r) \) using quotient_proj_fun
then have \( two\_top\_spaces0(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}) \) unfolding two_top_spaces0_def using topSpaceAssum, top
with fun, cont, top, IN show \( thesis \) using product_cont_functions, topSpaceAssum
The product of quotient topologies is a quotient topology given that the quotient map is open. This isn't true in general.
theorem (in topology0) prod_quotient:
assumes \( \text{equiv}(\bigcup T,r) \), \( \forall A\in T.\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(A) \in (\text{ quotient by } r) \)
shows \( ((\text{ quotient by } r)\times _t\text{ quotient by } r) = \) \( (\text{ quotient topology in } (((\bigcup T)//r)\times ((\bigcup T)//r))\text{ by } (\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\})\text{ from } (T\times _tT)) \)proof let \( T_r = \text{ quotient by } r \)
let \( R = (\text{ quotient topology in } (((\bigcup T)//r)\times ((\bigcup T)//r))\text{ by } (\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\})\text{ from } (T\times _tT)) \)
{
fix \( A \)
assume A: \( A\in T_r\times _tT_r \)
with assms(1) have \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \in T\times _tT \) using product_quo_fun unfolding IsContinuous_def
moreover
from A have \( A\subseteq \bigcup ((T_r)\times _t(T_r)) \)
with assms(1) have \( A\in Pow(((\bigcup T)//r)\times ((\bigcup T)//r)) \) using Top_1_4_T1(3), equiv_quo_is_top, total_quo_equi
ultimately have \( A\in R \) using QuotientTop_def, Top_1_4_T1(1), topSpaceAssum, prod_equiv_rel_surj unfolding topology0_def
thus \( (T_r)\times _t(T_r) \subseteq R \)
{
fix \( A \)
assume \( A\in R \)
with assms(1) have A: \( A \subseteq ((\bigcup T)//r)\times ((\bigcup T)//r) \), \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \in T\times _tT \) using QuotientTop_def, Top_1_4_T1(1), topSpaceAssum, prod_equiv_rel_surj unfolding topology0_def
{
fix \( C \)
assume \( C\in A \)
with A(1) obtain \( C_1 \) \( C_2 \) where CC: \( C=\langle C_1,C_2\rangle \), \( C_1\in ((\bigcup T)//r) \), \( C_2\in ((\bigcup T)//r) \)
then obtain \( c_1 \) \( c_2 \) where CC1: \( c_1\in \bigcup T \), \( c_2\in \bigcup T \) and CC2: \( C_1=r\{c_1\} \), \( C_2=r\{c_2\} \) unfolding quotient_def
with \( C\in A \), CC have \( \langle c_1,c_2\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \) using vimage_iff
with A(2) have \( \exists V W.\ V\in T \wedge W\in T \wedge V\times W \subseteq \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \wedge \langle c_1,c_2\rangle \in V\times W \) using prod_top_point_neighb, topSpaceAssum
then obtain \( V \) \( W \) where VW: \( V\in T \), \( W\in T \), \( V\times W \subseteq \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \), \( c_1\in V \), \( c_2\in W \)
let \( V_r = \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(V) \)
let \( W_r = \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(W) \)
from VW, assms have P: \( (V_r\times W_r) \in (T_r)\times _t(T_r) \) using prod_open_open_prod, equiv_quo_is_top
{
fix \( S \)
assume \( S\in (V_r\times W_r) \)
then obtain \( s_1 \) \( s_2 \) where S: \( S=\langle s_1,s_2\rangle \), \( s_1\in V_r \), \( s_2\in W_r \)
then obtain \( t_1 \) \( t_2 \) where T: \( \langle t_1,s_1\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \), \( \langle t_2,s_2\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \), \( t_1\in V \), \( t_2\in W \) using image_iff
with VW(3) have \( \exists S_0\in A.\ \langle \langle t_1,t_2\rangle ,S_0\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} \) using vimage_iff
then obtain \( S_0 \) where \( S_0\in A \) and \( \langle \langle t_1,t_2\rangle ,S_0\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} \)
moreover
from S(1), T, VW(1,2) have \( \langle \langle t_1,t_2\rangle ,S\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} \)
ultimately have \( S\in A \) using product_equiv_rel_fun unfolding Pi_def, function_def
hence sub: \( V_r\times W_r \subseteq A \)
from CC, CC2, CC1, \( c_1\in V \), \( c_2\in W \) have \( C \in V_r\times W_r \) using image_iff
with P, sub have \( \exists U\in (T_r)\times _t(T_r).\ U\subseteq A \wedge C\in U \) by (rule witness_exists1 )
hence \( \forall C\in A.\ \exists U\in (T_r)\times _t(T_r).\ C\in U \wedge U\subseteq A \)
with assms(1) have \( A\in (T_r)\times _t(T_r) \) using open_neigh_open, Top_1_4_T1, equiv_quo_is_top, assms unfolding topology0_def
thus \( R \subseteq (T_r)\times _t(T_r) \)
qed
end
Definition of QuotientTop:
\( f\in \text{surj}(\bigcup T,Y) \Longrightarrow \text{ quotient topology in } Y\text{ by } f \equiv \)
\( \{U\in Pow(Y).\ f^{-1}U\in T\} \)
Definition of IsATopology:
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \)
\( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
lemma invim_inter_inter_invim:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A\cap B) = f^{-1}(A) \cap f^{-1}(B) \)Definition of IsContinuous:
\( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
lemma vimage_comp: shows \( (r\circ s)^{-1}(A) = s^{-1}(r^{-1}(A)) \)
lemma func1_1_L3:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(D) \subseteq X \) lemma func1_1_L4:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(Y) = X \) lemma ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \) lemma quotient_proj_fun: shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}:A\rightarrow A//r \)
lemma EquivClass_1_L1:
assumes \( \text{equiv}(A,r) \) and \( C \in A//r \) and \( x\in C \)
shows \( x\in A \) lemma EquivClass_1_L2:
assumes \( \text{equiv}(A,r) \), \( C \in A//r \) and \( x\in C \)
shows \( r\{x\} = C \) lemma quotient_proj_surj: shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}\in \text{surj}(A,A//r) \)
lemma preim_equi_proj:
assumes \( U\subseteq A//r \), \( \text{equiv}(A,r) \)
shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}(U) = \bigcup U \)Definition of EquivQuo:
\( \text{equiv}(\bigcup T,r)\Longrightarrow (\text{ quotient by } r) \equiv \text{ quotient topology in } (\bigcup T)//r\text{ by } \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \)
lemma (in topology0) total_quo_func:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( (\bigcup (\text{ quotient topology in } Y\text{ by } f))=Y \) theorem (in topology0) quotientTop_is_top:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( (\text{ quotient topology in } Y\text{ by } f) \text{ is a topology } \) lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma func1_1_L5A:
assumes \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)
shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \) theorem (in topology0) total_quo_equi:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( \bigcup (\text{ quotient by }r)=(\bigcup T)//r \) theorem (in topology0) quotient_equiv_rel:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( (\text{ quotient by }r)=\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\} \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma func1_1_L9:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( A \subseteq f^{-1}(f(A)) \) lemma func_eq:
assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)
shows \( f = g \) lemma (in topology0) quotient_func_cont:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( \text{IsContinuous}(T,(\text{ quotient topology in } Y\text{ by } f),f) \) theorem (in two_top_spaces0) cont_quotient_top:
assumes \( h\in \text{surj}(\bigcup \tau _1,Y) \), \( g:Y\rightarrow \bigcup \tau _2 \), \( \text{IsContinuous}(\tau _1,\tau _2,g\circ h) \)
shows \( \text{IsContinuous}((\text{ quotient topology in } Y\text{ by } h\text{ from } \tau _1),\tau _2,g) \) theorem (in topology0) equiv_quo_is_top:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( (\text{ quotient by }r)\text{ is a topology } \) lemma surj_image_vimage:
assumes \( f \in \text{surj}(X,Y) \) and \( A\subseteq Y \)
shows \( f(f^{-1}(A)) = A \) lemma bij_cont_open_homeo:
assumes \( f \in \text{bij}(\bigcup T,\bigcup S) \) and \( \text{IsContinuous}(T,S,f) \) and \( \forall U\in T.\ f(U) \in S \)
shows \( \text{IsAhomeomorphism}(T,S,f) \) lemma prod_fun:
assumes \( f:X_1\rightarrow X_2 \), \( g:X_3\rightarrow X_4 \)
shows \( \{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times X_3\}:X_1\times X_3\rightarrow X_2\times X_4 \) lemma product_equiv_rel_fun: shows \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}:(\bigcup T\times \bigcup T)\rightarrow ((\bigcup T)//r\times (\bigcup T)//r) \)
theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) theorem (in two_top_spaces0) product_cont_functions:
assumes \( f:X_1\rightarrow X_2 \), \( g:\bigcup \tau _3\rightarrow \bigcup \tau _4 \), \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( \text{IsContinuous}(\tau _3,\tau _4,g) \), \( \tau _4\text{ is a topology } \), \( \tau _3\text{ is a topology } \)
shows \( \text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _3), \text{ProductTopology}(\tau _2,\tau _4),\{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times \bigcup \tau _3\}) \) lemma (in topology0) product_quo_fun:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( \text{IsContinuous}(T\times _tT,(\text{ quotient by } r)\times _t(\text{ quotient by } r),\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}) \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) lemma (in topology0) prod_equiv_rel_surj: shows \( \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}\in \text{surj}(\bigcup (T\times _tT),((\bigcup T)//r\times (\bigcup T)//r)) \)
lemma prod_top_point_neighb:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( U \in \text{ProductTopology}(T,S) \) and \( x \in U \)
shows \( \exists V W.\ V\in T \wedge W\in S \wedge V\times W \subseteq U \wedge x \in V\times W \) lemma prod_open_open_prod:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( U\in T \), \( V\in S \)
shows \( U\times V \in \text{ProductTopology}(T,S) \) lemma witness_exists1:
assumes \( x\in X \), \( \phi (x) \), \( \psi (x) \)
shows \( \exists x\in X.\ \phi (x) \wedge \psi (x) \) lemma (in topology0) open_neigh_open:
assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)
shows \( V\in T \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8