theory TopologicalGroup_ZF imports Topology_ZF_2 Group_ZF
begin
This theory is about the first subject of algebraic topology: topological groups.
Topological group: definition and notation
Topological group is a group that is a topological space at the same time. This means that a topological group is a triple of sets, say \((G,f,\tau)\) such that \(\tau\) is a topology on \(G\), \(f\) is a group operation on \(G\) and both \(f\) and the operation of taking inverse in \(G\) are continuous. Since IsarMathLib defines topology without using the carrier, (see Topology_ZF), in our setup we just use \(\bigcup \tau\) instead of \(G\) and say that the pair of sets \((\bigcup \tau , f)\) is a group. This way our definition of being a topological group is a statement about two sets: the topology \(\tau\) and the group operation \(f\) on \(\bigcup \tau\). Since the domain of the group operation is \(G\times G\), the pair of topologies in which \(f\) is supposed to be continuous is \(\tau\) and the product topology on \(G\times G\).
This way we arrive at the following definition of a predicate that states that pair of sets is a topological group.
Definition
\( IsAtopologicalGroup(\tau ,f) \equiv (\tau \text{ is a topology }) \wedge \text{IsAgroup}(\bigcup \tau ,f) \wedge \) \( IsContinuous(ProductTopology(\tau ,\tau ),\tau ,f) \wedge \) \( IsContinuous(\tau ,\tau ,GroupInv(\bigcup \tau ,f)) \)
We will inherit notation from the topology0 locale. That locale assumes that \(T\) is a topology. For convenience we will denote \(G=\bigcup T\) and \(\tau\) to be the product topology on \(G\times G\). To that we add some notation specific to groups. We will use additive notation for the group operation, even though we don't assume that the group is abelian.
Locale topgroup = topology0 +
defines \( G \equiv \bigcup T \)
defines \( \tau \equiv ProductTopology(T,T) \)
assumes Ggroup: \( \text{IsAgroup}(G,f) \)
assumes fcon: \( IsContinuous(\tau ,T,f) \)
assumes inv_cont: \( IsContinuous(T,T,GroupInv(G,f)) \)
defines \( x + y \equiv f\langle x,y\rangle \)
defines \( ( - x) \equiv GroupInv(G,f)(x) \)
defines \( x - y \equiv x + ( - y) \)
The first lemma states that we indeeed talk about topological group in the context of topgroup locale.
lemma (in topgroup) topGroup:
shows \( IsAtopologicalGroup(T,f) \) using topSpaceAssum , Ggroup , fcon , inv_cont , IsAtopologicalGroup_defIf a pair of sets \((T,f)\) forms a topological group, then all theorems proven in the topgroup context are valid as applied to \((T,f)\).
lemma topGroupLocale:
assumes \( IsAtopologicalGroup(T,f) \)
shows \( topgroup(T,f) \) using assms , IsAtopologicalGroup_def , topgroup_def , topgroup_axioms.intro , topology0_defWe can use the group0 locale in the context of topgroup.
lemma (in topgroup) group0_valid_in_tgroup:
shows \( group0(G,f) \) using Ggroup , group0_defOf course the product topology is a topology (on \(G\times G\)).
lemma (in topgroup) prod_top_on_G:
shows \( \tau \text{ is a topology } \) and \( \bigcup \tau = G\times G \) using topSpaceAssum , Top_1_4_T1Let's recall that \(f\) is a binary operation on \(G\) in this context.
lemma (in topgroup) topgroup_f_binop:
shows \( f : G\times G \rightarrow G \) using Ggroup , group0_def , group_oper_assocAA subgroup of a topological group is a topological group with relative topology and restricted operation.Relative topology is the same as \( T \text{ restricted to } H \) which is defined to be \(\{V \cup H: V\in T\}\) in ZF1 theory.
lemma (in topgroup) top_subgroup:
assumes A1: \( IsAsubgroup(H,f) \)
shows \( IsAtopologicalGroup(T \text{ restricted to } H,restrict(f,H\times H)) \)proof let \( \tau _0 = T \text{ restricted to } H \)
let \( f_H = restrict(f,H\times H) \)
have \( \bigcup \tau _0 = G \cap H \) using union_restrict
also
from A1 have \( \ldots = H \) using group0_valid_in_tgroup , group0_3_L2
finally have \( \bigcup \tau _0 = H \)
have \( \tau _0 \text{ is a topology } \) using Top_1_L4
moreover
qed
from A1, \( \bigcup \tau _0 = H \) have \( \text{IsAgroup}(\bigcup \tau _0,f_H) \) using IsAsubgroup_def
moreover have \( IsContinuous(ProductTopology(\tau _0,\tau _0),\tau _0,f_H) \)proof
moreover have \( two\_top\_spaces0(\tau , T,f) \) using topSpaceAssum , prod_top_on_G , topgroup_f_binop , prod_top_on_G , two_top_spaces0_def
moreover
from A1 have \( H \subseteq G \) using group0_valid_in_tgroup , group0_3_L2
then have \( H\times H \subseteq \bigcup \tau \) using prod_top_on_G
moreover have \( IsContinuous(\tau ,T,f) \) using fcon
ultimately have \( IsContinuous(\tau \text{ restricted to } H\times H, T \text{ restricted to } f_H(H\times H),f_H) \) using restr_restr_image_cont
moreover
qed
have \( ProductTopology(\tau _0,\tau _0) = \tau \text{ restricted to } H\times H \) using topSpaceAssum , prod_top_restr_comm
moreover from A1 have \( f_H(H\times H) = H \) using image_subgr_op
ultimately show \( thesis \)
have \( IsContinuous(\tau _0,\tau _0,GroupInv(\bigcup \tau _0,f_H)) \)proof
ultimately show \( thesis \) unfolding IsAtopologicalGroup_def
let \( g = restrict(GroupInv(G,f),H) \)
have \( GroupInv(G,f) : G \rightarrow G \) using Ggroup , group0_2_T2
then have \( two\_top\_spaces0(T,T,GroupInv(G,f)) \) using topSpaceAssum , two_top_spaces0_def
moreover
from A1 have \( H \subseteq \bigcup T \) using group0_valid_in_tgroup , group0_3_L2
ultimately have \( IsContinuous(\tau _0,T \text{ restricted to } g(H),g) \) using inv_cont , restr_restr_image_cont
moreover
qed
from A1 have \( g(H) = H \) using group0_valid_in_tgroup , restr_inv_onto
moreover from A1 have \( GroupInv(H,f_H) = g \) using group0_valid_in_tgroup , group0_3_T1
with \( \bigcup \tau _0 = H \) have \( g = GroupInv(\bigcup \tau _0,f_H) \)
ultimately show \( thesis \)
end
Definition of IsAtopologicalGroup:
\( IsAtopologicalGroup(\tau ,f) \equiv (\tau \text{ is a topology }) \wedge \text{IsAgroup}(\bigcup \tau ,f) \wedge \)
\( IsContinuous(ProductTopology(\tau ,\tau ),\tau ,f) \wedge \)
\( IsContinuous(\tau ,\tau ,GroupInv(\bigcup \tau ,f)) \)
theorem Top_1_4_T1: assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) shows \( ProductTopology(T,S) \text{ is a topology } \), \( ProductCollection(T,S) \text{ is a base for } ProductTopology(T,S) \), \( \bigcup ProductTopology(T,S) = \bigcup T \times \bigcup S \)
lemma (in group0) group_oper_assocA: shows \( P : G\times G\rightarrow G \)
lemma union_restrict: shows \( \bigcup (M \text{ restricted to } X) = (\bigcup M) \cap X \)
lemma (in topgroup) group0_valid_in_tgroup: shows \( group0(G,f) \)
lemma (in group0) group0_3_L2: assumes \( IsAsubgroup(H,P) \) shows \( H \subseteq G \)
lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)
Definition of IsAsubgroup:
\( IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H)) \)
lemma (in topgroup) prod_top_on_G: shows \( \tau \text{ is a topology } \) and \( \bigcup \tau = G\times G \)
lemma (in topgroup) topgroup_f_binop: shows \( f : G\times G \rightarrow G \)
lemma (in two_top_spaces0) restr_restr_image_cont: assumes \( A \subseteq X_1 \) and \( f \text{ is continuous } \) and \( g = restrict(f,A) \) and \( \tau _3 = \tau _1 \text{ restricted to } A \) shows \( IsContinuous(\tau _3, \tau _2 \text{ restricted to } g(A),g) \)
lemma prod_top_restr_comm: assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) shows \( ProductTopology(T \text{ restricted to } A,S \text{ restricted to } B) =\)
\( ProductTopology(T,S) \text{ restricted to } (A\times B) \)
lemma image_subgr_op: assumes \( IsAsubgroup(H,P) \) shows \( restrict(P,H\times H)(H\times H) = H \)
theorem group0_2_T2: assumes \( \text{IsAgroup}(G,f) \) shows \( GroupInv(G,f) : G\rightarrow G \)
lemma (in group0) restr_inv_onto: assumes \( IsAsubgroup(H,P) \) shows \( restrict(GroupInv(G,P),H)(H) = H \)
theorem (in group0) group0_3_T1: assumes \( IsAsubgroup(H,P) \) and \( g = restrict(P,H\times H) \) shows \( GroupInv(H,g) = restrict(GroupInv(G,P),H) \)
