Theory TopologicalGroup_ZF
section ‹Topological groups - introduction›
theory TopologicalGroup_ZF imports Topology_ZF_3 Group_ZF_1 Semigroup_ZF
begin
text‹This theory is about the first subject of algebraic topology:
topological groups.›
subsection‹Topological group: definition and notation›
text‹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,T)$ such that $T$ 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 T$ instead
of $G$ and say that the pair of sets $(\bigcup T , f)$ is a group.
This way our definition of being a topological group is a statement about two
sets: the topology $T$ and the group operation $f$ on $G=\bigcup T$.
Since the domain of the group operation is $G\times G$, the pair of
topologies in which $f$ is supposed to be continuous is $T$ and
the product topology on $G\times G$ (which we will call $\tau$ below).›
text‹This way we arrive at the following definition of a predicate that
states that pair of sets is a topological group.›
definition
"IsAtopologicalGroup(T,f) ≡ (T {is a topology}) ∧ IsAgroup(⋃T,f) ∧
IsContinuous(ProductTopology(T,T),T,f) ∧
IsContinuous(T,T,GroupInv(⋃T,f))"
text‹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.
The notation $g+A$ will mean the left translation of the set $A$ by element $g$, i.e.
$g+A=\{g+a|a\in A\}$.
The group operation $G$ induces a natural operation on the subsets of $G$
defined as $\langle A,B\rangle \mapsto \{x+y | x\in A, y\in B \}$.
Such operation has been considered in ‹func_ZF› and called
$f$ ''lifted to subsets of'' $G$. We will denote the value of such operation
on sets $A,B$ as $A+B$.
The set of neigboorhoods of zero (denoted ‹𝒩⇩0›) is the
collection of (not necessarily open) sets whose interior contains the neutral
element of the group.›
locale topgroup = topology0 +
fixes G
defines G_def [simp]: "G ≡ ⋃T"
fixes prodtop ("τ")
defines prodtop_def [simp]: "τ ≡ ProductTopology(T,T)"
fixes f
assumes Ggroup: "IsAgroup(G,f)"
assumes fcon: "IsContinuous(τ,T,f)"
assumes inv_cont: "IsContinuous(T,T,GroupInv(G,f))"
fixes grop (infixl "\<ra>" 90)
defines grop_def [simp]: "x\<ra>y ≡ f`⟨x,y⟩"
fixes grinv ("\<rm> _" 89)
defines grinv_def [simp]: "(\<rm>x) ≡ GroupInv(G,f)`(x)"
fixes grsub (infixl "\<rs>" 90)
defines grsub_def [simp]: "x\<rs>y ≡ x\<ra>(\<rm>y)"
fixes setinv ("\<sm> _" 72)
defines setninv_def [simp]: "\<sm>A ≡ GroupInv(G,f)``(A)"
fixes ltrans (infix "\<ltr>" 73)
defines ltrans_def [simp]: "x \<ltr> A ≡ LeftTranslation(G,f,x)``(A)"
fixes rtrans (infix "\<rtr>" 73)
defines rtrans_def [simp]: "A \<rtr> x ≡ RightTranslation(G,f,x)``(A)"
fixes setadd (infixl "\<sad>" 71)
defines setadd_def [simp]: "A\<sad>B ≡ (f {lifted to subsets of} G)`⟨A,B⟩"
fixes gzero ("𝟬")
defines gzero_def [simp]: "𝟬 ≡ TheNeutralElement(G,f)"
fixes zerohoods ("𝒩⇩0")
defines zerohoods_def [simp]: "𝒩⇩0 ≡ {A ∈ Pow(G). 𝟬 ∈ int(A)}"
fixes listsum ("∑ _" 70)
defines listsum_def[simp]: "∑k ≡ Fold1(f,k)"
text‹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_def
by simp
text‹If 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_def by simp
text‹We can use the ‹group0› locale in the context of ‹topgroup›.›
lemma (in topgroup) group0_valid_in_tgroup: shows "group0(G,f)"
using Ggroup group0_def by simp
text‹We can use the ‹group0› locale in the context of ‹topgroup›.›
sublocale topgroup < group0 G f gzero grop grinv
unfolding group0_def gzero_def grop_def grinv_def using Ggroup by auto
text‹We can use ‹semigr0› locale in the context of ‹topgroup›.›
lemma (in topgroup) semigr0_valid_in_tgroup: shows "semigr0(G,f)"
using Ggroup IsAgroup_def IsAmonoid_def semigr0_def by simp
text‹We can use the ‹prod_top_spaces0› locale in the context of ‹topgroup›.›
lemma (in topgroup) prod_top_spaces0_valid: shows "prod_top_spaces0(T,T,T)"
using topSpaceAssum prod_top_spaces0_def by simp
text‹Negative of a group element is in group.›
lemma (in topgroup) neg_in_tgroup: assumes "g∈G" shows "(\<rm>g) ∈ G"
using assms inverse_in_group by simp
text‹Sum of two group elements is in the group.›
lemma (in topgroup) group_op_closed_add: assumes "x⇩1 ∈ G" "x⇩2 ∈ G"
shows "x⇩1\<ra>x⇩2 ∈ G"
using assms group_op_closed by simp
text‹Zero is in the group.›
lemma (in topgroup) zero_in_tgroup: shows "𝟬∈G"
using group0_2_L2 by simp
text‹ Another lemma about canceling with two group elements written in additive notation ›
lemma (in topgroup) inv_cancel_two_add:
assumes "x⇩1 ∈ G" "x⇩2 ∈ G"
shows
"x⇩1\<ra>(\<rm>x⇩2)\<ra>x⇩2 = x⇩1"
"x⇩1\<ra>x⇩2\<ra>(\<rm>x⇩2) = x⇩1"
"(\<rm>x⇩1)\<ra>(x⇩1\<ra>x⇩2) = x⇩2"
"x⇩1\<ra>((\<rm>x⇩1)\<ra>x⇩2) = x⇩2"
using assms inv_cancel_two by auto
text‹Useful identities proven in the ‹Group_ZF› theory, rewritten here in additive notation.
Note since the group operation notation is left associative we don't really need the first set
of parentheses in some cases.›
lemma (in topgroup) cancel_middle_add: assumes "x⇩1 ∈ G" "x⇩2 ∈ G" "x⇩3 ∈ G"
shows
"(x⇩1\<ra>(\<rm>x⇩2))\<ra>(x⇩2\<ra>(\<rm>x⇩3)) = x⇩1\<ra> (\<rm>x⇩3)"
"((\<rm>x⇩1)\<ra>x⇩2)\<ra>((\<rm>x⇩2)\<ra>x⇩3) = (\<rm>x⇩1)\<ra> x⇩3"
"(\<rm> (x⇩1\<ra>x⇩2)) \<ra> (x⇩1\<ra>x⇩3) = (\<rm>x⇩2)\<ra>x⇩3"
"(x⇩1\<ra>x⇩2) \<ra> (\<rm>(x⇩3\<ra>x⇩2)) =x⇩1\<ra> (\<rm>x⇩3)"
"(\<rm>x⇩1) \<ra> (x⇩1\<ra>x⇩2\<ra>x⇩3) \<ra> (\<rm>x⇩3) = x⇩2"
proof -
from assms have "x⇩1\<ra> (\<rm>x⇩3) = (x⇩1\<ra>(\<rm>x⇩2))\<ra>(x⇩2\<ra>(\<rm>x⇩3))"
using group0_2_L14A(1) by blast
thus "(x⇩1\<ra>(\<rm>x⇩2))\<ra>(x⇩2\<ra>(\<rm>x⇩3)) = x⇩1\<ra> (\<rm>x⇩3)" by simp
from assms have "(\<rm>x⇩1)\<ra> x⇩3 = ((\<rm>x⇩1)\<ra>x⇩2)\<ra>((\<rm>x⇩2)\<ra>x⇩3)"
using group0_2_L14A(2) by blast
thus "((\<rm>x⇩1)\<ra>x⇩2)\<ra>((\<rm>x⇩2)\<ra>x⇩3) = (\<rm>x⇩1)\<ra> x⇩3" by simp
from assms show "(\<rm> (x⇩1\<ra>x⇩2)) \<ra> (x⇩1\<ra>x⇩3) = (\<rm>x⇩2)\<ra>x⇩3"
using cancel_middle(1) by simp
from assms show "(x⇩1\<ra>x⇩2) \<ra> (\<rm>(x⇩3\<ra>x⇩2)) =x⇩1\<ra> (\<rm>x⇩3)"
using cancel_middle(2) by simp
from assms show "(\<rm>x⇩1) \<ra> (x⇩1\<ra>x⇩2\<ra>x⇩3) \<ra> (\<rm>x⇩3) = x⇩2"
using cancel_middle(3) by simp
qed
text‹ We can cancel an element on the right from both sides of an equation. ›
lemma (in topgroup) cancel_right_add:
assumes "x⇩1 ∈ G" "x⇩2 ∈ G" "x⇩3 ∈ G" "x⇩1\<ra>x⇩2 = x⇩3\<ra>x⇩2"
shows "x⇩1 = x⇩3"
using assms cancel_right by simp
text‹ We can cancel an element on the left from both sides of an equation. ›
lemma (in topgroup) cancel_left_add:
assumes "x⇩1 ∈ G" "x⇩2 ∈ G" "x⇩3 ∈ G" "x⇩1\<ra>x⇩2 = x⇩1\<ra>x⇩3"
shows "x⇩2 = x⇩3"
using assms cancel_left by simp
text‹We can put an element on the other side of an equation.›
lemma (in topgroup) put_on_the_other_side:
assumes "x⇩1 ∈ G" "x⇩2 ∈ G" "x⇩3 = x⇩1\<ra>x⇩2"
shows "x⇩3\<ra>(\<rm>x⇩2) = x⇩1" and "(\<rm>x⇩1)\<ra>x⇩3 = x⇩2"
using assms group0_2_L18 by auto
text‹A simple equation from lemma ‹simple_equation0› in ‹Group_ZF› in additive notation ›
lemma (in topgroup) simple_equation0_add:
assumes "x⇩1 ∈ G" "x⇩2 ∈ G" "x⇩3 ∈ G" "x⇩1\<ra>(\<rm>x⇩2) = (\<rm>x⇩3)"
shows "x⇩3 = x⇩2 \<ra> (\<rm>x⇩1)"
using assms simple_equation0 by blast
text‹A simple equation from lemma ‹simple_equation1› in ‹Group_ZF› in additive notation ›
lemma (in topgroup) simple_equation1_add:
assumes "x⇩1 ∈ G" "x⇩2 ∈ G" "x⇩3 ∈ G" "(\<rm>x⇩1)\<ra>x⇩2 = (\<rm>x⇩3)"
shows "x⇩3 = (\<rm>x⇩2) \<ra> x⇩1"
using assms simple_equation1 by blast
text‹The set comprehension form of negative of a set. The proof uses the ‹ginv_image› lemma from
‹Group_ZF› theory which states the same thing in multiplicative notation. ›
lemma (in topgroup) ginv_image_add: assumes "V⊆G"
shows "(\<sm>V)⊆G" and "(\<sm>V) = {\<rm>x. x ∈ V}"
using assms ginv_image by auto
text‹ The additive notation version of ‹ginv_image_el› lemma from ‹Group_ZF› theory ›
lemma (in topgroup) ginv_image_el_add: assumes "V⊆G" "x ∈ (\<sm>V)"
shows "(\<rm>x) ∈ V"
using assms ginv_image_el by simp
text‹Of course the product topology is a topology (on $G\times G$).›
lemma (in topgroup) prod_top_on_G:
shows "τ {is a topology}" and "⋃τ = G×G"
using topSpaceAssum Top_1_4_T1 by auto
text‹Let's recall that $f$ is a binary operation on $G$ in this context.›
lemma (in topgroup) topgroup_f_binop: shows "f : G×G → G"
using Ggroup group0_def group0.group_oper_fun by simp
text‹A subgroup of a topological group is a topological group
with relative topology
and restricted operation. Relative topology is the same
as ‹T {restricted to} H›
which is defined to be $\{V \cap H: V\in T\}$ in ‹ZF1› theory.›
lemma (in topgroup) top_subgroup: assumes A1: "IsAsubgroup(H,f)"
shows "IsAtopologicalGroup(T {restricted to} H,restrict(f,H×H))"
proof -
let ?τ⇩0 = "T {restricted to} H"
let ?f⇩H = "restrict(f,H×H)"
have "⋃?τ⇩0 = G ∩ H" using union_restrict by simp
also from A1 have "… = H"
using group0_3_L2 by blast
finally have "⋃?τ⇩0 = H" by simp
have "?τ⇩0 {is a topology}" using Top_1_L4 by simp
moreover from A1 ‹⋃?τ⇩0 = H› have "IsAgroup(⋃?τ⇩0,?f⇩H)"
using IsAsubgroup_def by simp
moreover have "IsContinuous(ProductTopology(?τ⇩0,?τ⇩0),?τ⇩0,?f⇩H)"
proof -
have "two_top_spaces0(τ, T,f)"
using topSpaceAssum prod_top_on_G topgroup_f_binop prod_top_on_G
two_top_spaces0_def by simp
moreover
from A1 have "H ⊆ G" using group0_3_L2 by simp
then have "H×H ⊆ ⋃τ" using prod_top_on_G by auto
moreover have "IsContinuous(τ,T,f)" using fcon by simp
ultimately have
"IsContinuous(τ {restricted to} H×H, T {restricted to} ?f⇩H``(H×H),?f⇩H)" using two_top_spaces0.restr_restr_image_cont
by simp
moreover have
"ProductTopology(?τ⇩0,?τ⇩0) = τ {restricted to} H×H" using topSpaceAssum prod_top_restr_comm
by simp
moreover from A1 have "?f⇩H``(H×H) = H" using image_subgr_op
by simp
ultimately show ?thesis by simp
qed
moreover have "IsContinuous(?τ⇩0,?τ⇩0,GroupInv(⋃?τ⇩0,?f⇩H))"
proof -
let ?g = "restrict(GroupInv(G,f),H)"
have "GroupInv(G,f) : G → G"
using Ggroup group0_2_T2 by simp
then have "two_top_spaces0(T,T,GroupInv(G,f))"
using topSpaceAssum two_top_spaces0_def by simp
moreover from A1 have "H ⊆ ⋃T" using group0_3_L2 by simp
ultimately have
"IsContinuous(?τ⇩0,T {restricted to} ?g``(H),?g)"
using inv_cont two_top_spaces0.restr_restr_image_cont
by simp
moreover from A1 have "?g``(H) = H" using restr_inv_onto by simp
moreover
from A1 have "GroupInv(H,?f⇩H) = ?g" using group0_3_T1 by simp
with ‹⋃?τ⇩0 = H› have "?g = GroupInv(⋃?τ⇩0,?f⇩H)" by simp
ultimately show ?thesis by simp
qed
ultimately show ?thesis unfolding IsAtopologicalGroup_def by simp
qed
subsection‹Interval arithmetic, translations and inverse of set›
text‹In this section we list some properties of operations of translating a
set and reflecting it around the neutral element of the group. Many of the results
are proven in other theories, here we just collect them and rewrite in notation
specific to the ‹topgroup› context.›
text‹Different ways of looking at adding sets.›
lemma (in topgroup) interval_add: assumes "A⊆G" "B⊆G" shows
"A\<sad>B ⊆ G"
"A\<sad>B = f``(A×B)"
"A\<sad>B = (⋃x∈A. x\<ltr>B)"
"A\<sad>B = {x\<ra>y. ⟨x,y⟩ ∈ A×B}"
proof -
from assms show "A\<sad>B ⊆ G" and "A\<sad>B = f``(A×B)" and "A\<sad>B = {x\<ra>y. ⟨x,y⟩ ∈ A×B}"
using topgroup_f_binop lift_subsets_explained by auto
from assms show "A\<sad>B = (⋃x∈A. x\<ltr>B)" using image_ltrans_union by simp
qed
text‹ If the neutral element is in a set, then it is in the sum of the sets. ›
lemma (in topgroup) interval_add_zero: assumes "A⊆G" "𝟬∈A"
shows "𝟬 ∈ A\<sad>A"
proof -
from assms have "𝟬\<ra>𝟬 ∈ A\<sad>A" using interval_add(4) by auto
then show "𝟬 ∈ A\<sad>A" using group0_2_L2 by auto
qed
text‹Some lemmas from ‹Group_ZF_1› about images of set by translations
written in additive notation›
lemma (in topgroup) lrtrans_image: assumes "V⊆G" "x∈G"
shows
"x\<ltr>V = {x\<ra>v. v∈V}"
"V\<rtr>x = {v\<ra>x. v∈V}"
using assms ltrans_image rtrans_image by auto
text‹ Right and left translations of a set are subsets of the group.
This is of course typically applied to the subsets of the group, but formally we don't
need to assume that. ›
lemma (in topgroup) lrtrans_in_group_add: assumes "x∈G"
shows "x\<ltr>V ⊆ G" and "V\<rtr>x ⊆G"
using assms lrtrans_in_group by auto
text‹ A corollary from ‹interval_add› ›
corollary (in topgroup) elements_in_set_sum: assumes "A⊆G" "B⊆G"
"t ∈ A\<sad>B" shows "∃s∈A. ∃q∈B. t=s\<ra>q"
using assms interval_add(4) by auto
text‹ A corollary from ‹ lrtrans_image› ›
corollary (in topgroup) elements_in_ltrans:
assumes "B⊆G" "g∈G" "t ∈ g\<ltr>B"
shows "∃q∈B. t=g\<ra>q"
using assms lrtrans_image(1) by simp
text‹ Another corollary of ‹lrtrans_image› ›
corollary (in topgroup) elements_in_rtrans:
assumes "B⊆G" "g∈G" "t ∈ B\<rtr>g" shows "∃q∈B. t=q\<ra>g"
using assms lrtrans_image(2) by simp
text‹Another corollary from ‹interval_add› ›
corollary (in topgroup) elements_in_set_sum_inv:
assumes "A⊆G" "B⊆G" "t=s\<ra>q" "s∈A" "q∈B"
shows "t ∈ A\<sad>B"
using assms interval_add by auto
text‹Another corollary of ‹lrtrans_image› ›
corollary (in topgroup) elements_in_ltrans_inv: assumes "B⊆G" "g∈G" "q∈B" "t=g\<ra>q"
shows "t ∈ g\<ltr>B"
using assms lrtrans_image(1) by auto
text‹Another corollary of ‹rtrans_image_add› ›
lemma (in topgroup) elements_in_rtrans_inv:
assumes "B⊆G" "g∈G" "q∈B" "t=q\<ra>g"
shows "t ∈ B\<rtr>g"
using assms lrtrans_image(2) by auto
text‹Right and left translations are continuous.›
lemma (in topgroup) trans_cont: assumes "g∈G" shows
"IsContinuous(T,T,RightTranslation(G,f,g))" and
"IsContinuous(T,T,LeftTranslation(G,f,g))"
using assms trans_eq_section topgroup_f_binop fcon prod_top_spaces0_valid
prod_top_spaces0.fix_1st_var_cont prod_top_spaces0.fix_2nd_var_cont
by auto
text‹Left and right translations of an open set are open.›
lemma (in topgroup) open_tr_open: assumes "g∈G" and "V∈T"
shows "g\<ltr>V ∈ T" and "V\<rtr>g ∈ T"
using assms neg_in_tgroup trans_cont IsContinuous_def trans_image_vimage by auto
text‹Right and left translations are homeomorphisms.›
lemma (in topgroup) tr_homeo: assumes "g∈G" shows
"IsAhomeomorphism(T,T,RightTranslation(G,f,g))" and
"IsAhomeomorphism(T,T,LeftTranslation(G,f,g))"
using assms trans_bij trans_cont open_tr_open bij_cont_open_homeo
by auto
text‹Left translations preserve interior.›
lemma (in topgroup) ltrans_interior: assumes A1: "g∈G" and A2: "A⊆G"
shows "g \<ltr> int(A) = int(g\<ltr>A)"
proof -
from assms have "A ⊆ ⋃T" and "IsAhomeomorphism(T,T,LeftTranslation(G,f,g))" using tr_homeo
by auto
then show ?thesis using int_top_invariant by simp
qed
text‹Right translations preserve interior.›
lemma (in topgroup) rtrans_interior: assumes A1: "g∈G" and A2: "A⊆G"
shows "int(A) \<rtr> g = int(A\<rtr>g)"
proof -
from assms have "A ⊆ ⋃T" and "IsAhomeomorphism(T,T,RightTranslation(G,f,g))" using tr_homeo
by auto
then show ?thesis using int_top_invariant by simp
qed
text‹Translating by an inverse and then by an element cancels out.›
lemma (in topgroup) trans_inverse_elem: assumes "g∈G" and "A⊆G"
shows "g\<ltr>((\<rm>g)\<ltr>A) = A"
using assms neg_in_tgroup trans_comp_image group0_2_L6 trans_neutral image_id_same
by simp
text‹Inverse of an open set is open.›
lemma (in topgroup) open_inv_open: assumes "V∈T" shows "(\<sm>V) ∈ T"
using assms inv_image_vimage inv_cont IsContinuous_def by simp
text‹Inverse is a homeomorphism.›
lemma (in topgroup) inv_homeo: shows "IsAhomeomorphism(T,T,GroupInv(G,f))"
using group_inv_bij inv_cont open_inv_open bij_cont_open_homeo by simp
text‹Taking negative preserves interior.›
lemma (in topgroup) int_inv_inv_int: assumes "A ⊆ G"
shows "int(\<sm>A) = \<sm>(int(A))"
using assms inv_homeo int_top_invariant by simp
subsection‹Neighborhoods of zero›
text‹Zero neighborhoods are (not necessarily open) sets whose interior
contains the neutral element of the group. In the ‹topgroup› locale
the collection of neighboorhoods of zero is denoted ‹𝒩⇩0›. ›
text‹The whole space is a neighborhood of zero.›
lemma (in topgroup) zneigh_not_empty: shows "G ∈ 𝒩⇩0"
using topSpaceAssum IsATopology_def Top_2_L3 zero_in_tgroup
by simp
text‹Any element that belongs to a subset of the group belongs to that subset with the
interior of a neighborhood of zero added. ›
lemma (in topgroup) elem_in_int_sad: assumes "A⊆G" "g∈A" "H ∈ 𝒩⇩0"
shows "g ∈ A\<sad>int(H)"
proof -
from assms(3) have "𝟬 ∈ int(H)" and "int(H) ⊆ G" using Top_2_L2 by auto
with assms(1,2) have "g\<ra>𝟬 ∈ A\<sad>int(H)" using elements_in_set_sum_inv
by simp
with assms(1,2) show ?thesis using group0_2_L2 by auto
qed
text‹Any element belongs to the interior of any neighboorhood of zero
left translated by that element.›
lemma (in topgroup) elem_in_int_ltrans:
assumes "g∈G" and "H ∈ 𝒩⇩0"
shows "g ∈ int(g\<ltr>H)" and "g ∈ int(g\<ltr>H) \<sad> int(H)"
proof -
from assms(2) have "𝟬 ∈ int(H)" and "int(H) ⊆ G" using Top_2_L2 by auto
with assms(1) have "g ∈ g \<ltr> int(H)" using neut_trans_elem by simp
with assms show "g ∈ int(g\<ltr>H)" using ltrans_interior by simp
from assms(1) have "int(g\<ltr>H) ⊆ G" using lrtrans_in_group_add(1) Top_2_L1
by blast
with ‹g ∈ int(g\<ltr>H)› assms(2) show "g ∈ int(g\<ltr>H) \<sad> int(H)"
using elem_in_int_sad by simp
qed
text‹Any element belongs to the interior of any neighboorhood of zero
right translated by that element.›
lemma (in topgroup) elem_in_int_rtrans:
assumes A1: "g∈G" and A2: "H ∈ 𝒩⇩0"
shows "g ∈ int(H\<rtr>g)" and "g ∈ int(H\<rtr>g) \<sad> int(H)"
proof -
from A2 have "𝟬 ∈ int(H)" and "int(H) ⊆ G" using Top_2_L2 by auto
with A1 have "g ∈ int(H) \<rtr> g" using neut_trans_elem by simp
with assms show "g ∈ int(H\<rtr>g)" using rtrans_interior by simp
from assms(1) have "int(H\<rtr>g) ⊆ G" using lrtrans_in_group_add(2) Top_2_L1
by blast
with ‹g ∈ int(H\<rtr>g)› assms(2) show "g ∈ int(H\<rtr>g) \<sad> int(H)"
using elem_in_int_sad by simp
qed
text‹Negative of a neighborhood of zero is a neighborhood of zero.›
lemma (in topgroup) neg_neigh_neigh: assumes "H ∈ 𝒩⇩0"
shows "(\<sm>H) ∈ 𝒩⇩0"
proof -
from assms have "int(H) ⊆ G" and "𝟬 ∈ int(H)" using Top_2_L1 by auto
with assms have "𝟬 ∈ int(\<sm>H)" using neut_inv_neut int_inv_inv_int by simp
moreover
have "GroupInv(G,f):G→G" using Ggroup group0_2_T2 by simp
then have "(\<sm>H) ⊆ G" using func1_1_L6 by simp
ultimately show ?thesis by simp
qed
text‹Left translating an open set by a negative of a point that belongs to it
makes it a neighboorhood of zero.›
lemma (in topgroup) open_trans_neigh: assumes A1: "U∈T" and "g∈U"
shows "(\<rm>g)\<ltr>U ∈ 𝒩⇩0"
proof -
let ?H = "(\<rm>g)\<ltr>U"
from assms have "g∈G" by auto
then have "(\<rm>g) ∈ G" using neg_in_tgroup by simp
with A1 have "?H∈T" using open_tr_open by simp
hence "?H ⊆ G" by auto
moreover have "𝟬 ∈ int(?H)"
proof -
from assms have "U⊆G" and "g∈U" by auto
with ‹?H∈T› show "𝟬 ∈ int(?H)" using elem_trans_neut Top_2_L3 by auto
qed
ultimately show ?thesis by simp
qed
text‹Right translating an open set by a negative of a point that belongs to it
makes it a neighboorhood of zero.›
lemma (in topgroup) open_trans_neigh_2: assumes A1: "U∈T" and "g∈U"
shows "U\<rtr>(\<rm>g) ∈ 𝒩⇩0"
proof -
let ?H = "U\<rtr>(\<rm>g)"
from assms have "g∈G" by auto
then have "(\<rm>g) ∈ G" using neg_in_tgroup by simp
with A1 have "?H∈T" using open_tr_open by simp
hence "?H ⊆ G" by auto
moreover have "𝟬 ∈ int(?H)"
proof -
from assms have "U⊆G" and "g∈U" by auto
with ‹?H∈T› show "𝟬 ∈ int(?H)" using elem_trans_neut Top_2_L3 by auto
qed
ultimately show ?thesis by simp
qed
text‹Right and left translating an neighboorhood of zero by a point and its negative
makes it back a neighboorhood of zero.›
lemma (in topgroup) lrtrans_neigh: assumes "W∈𝒩⇩0" and "x∈G"
shows "x\<ltr>(W\<rtr>(\<rm>x)) ∈ 𝒩⇩0" and "(x\<ltr>W)\<rtr>(\<rm>x) ∈ 𝒩⇩0"
proof -
from assms(2) have "x\<ltr>(W\<rtr>(\<rm>x)) ⊆ G" using lrtrans_in_group_add(1) by simp
moreover have "𝟬 ∈ int(x\<ltr>(W\<rtr>(\<rm>x)))"
proof -
from assms(2) have "int(W\<rtr>(\<rm>x)) ⊆ G"
using neg_in_tgroup lrtrans_in_group_add(2) Top_2_L1 by blast
with assms(2) have "(x\<ltr>int((W\<rtr>(\<rm>x)))) = {x\<ra>y. y∈int(W\<rtr>(\<rm>x))}"
using lrtrans_image(1) by simp
moreover from assms have "(\<rm>x) ∈ int(W\<rtr>(\<rm>x))"
using neg_in_tgroup elem_in_int_rtrans(1) by simp
ultimately have "x\<ra>(\<rm>x) ∈ x\<ltr>int(W\<rtr>(\<rm>x))" by auto
with assms show ?thesis using group0_2_L6 neg_in_tgroup lrtrans_in_group_add(2) ltrans_interior
by simp
qed
ultimately show "x\<ltr>(W\<rtr>(\<rm>x)) ∈ 𝒩⇩0" by simp
from assms(2) have "(x\<ltr>W)\<rtr>(\<rm>x) ⊆ G" using lrtrans_in_group_add(2) neg_in_tgroup
by simp
moreover have "𝟬 ∈ int((x\<ltr>W)\<rtr>(\<rm>x))"
proof -
from assms(2) have "int((x\<ltr>W)) ⊆ G" using lrtrans_in_group_add(1) Top_2_L1 by blast
with assms(2) have "int(x\<ltr>W) \<rtr> (\<rm>x) = {y\<ra>(\<rm>x).y∈int(x\<ltr>W)}"
using neg_in_tgroup lrtrans_image(2) by simp
moreover from assms have "x ∈ int(x\<ltr>W)" using elem_in_int_ltrans(1) by simp
ultimately have "x\<ra>(\<rm>x) ∈ int(x\<ltr>W) \<rtr> (\<rm>x)" by auto
with assms(2) have "𝟬 ∈ int(x\<ltr>W) \<rtr> (\<rm>x)" using group0_2_L6 by simp
with assms show ?thesis using group0_2_L6 neg_in_tgroup lrtrans_in_group_add(1) rtrans_interior
by auto
qed
ultimately show "(x\<ltr>W)\<rtr>(\<rm>x) ∈ 𝒩⇩0" by simp
qed
text‹If $A$ is a subset of $B$ translated by $-x$ then its translation by $x$ is a subset of $B$.›
lemma (in topgroup) trans_subset:
assumes "A ⊆ ((\<rm>x)\<ltr>B)""x∈G" "B⊆G"
shows "x\<ltr>A ⊆ B"
proof-
from assms(1) have "x\<ltr>A ⊆ (x\<ltr> ((\<rm>x)\<ltr>B))" by auto
with assms(2,3) show "x\<ltr>A ⊆ B"
using neg_in_tgroup trans_comp_image group0_2_L6 trans_neutral image_id_same by simp
qed
text‹ Every neighborhood of zero has a symmetric subset that is a neighborhood of zero.›
theorem (in topgroup) exists_sym_zerohood:
assumes "U∈𝒩⇩0"
shows "∃V∈𝒩⇩0. (V⊆U ∧ (\<sm>V)=V)"
proof
let ?V = "U∩(\<sm>U)"
have "U⊆G" using assms unfolding zerohoods_def by auto
then have "?V⊆G" by auto
have invg:" GroupInv(G, f) ∈ G → G" using group0_2_T2 Ggroup by auto
have invb:"GroupInv(G, f) ∈bij(G,G)" using group_inv_bij(2) by auto
have "(\<sm>?V)=GroupInv(G,f)-``?V" unfolding setninv_def using inv_image_vimage
by auto
also have "…=(GroupInv(G,f)-``U)∩(GroupInv(G,f)-``(\<sm>U))" using invim_inter_inter_invim invg
by auto
also have "…=(\<sm>U)∩(GroupInv(G,f)-``(GroupInv(G,f)``U))"
unfolding setninv_def using inv_image_vimage by auto
also from ‹U⊆G› have "…=(\<sm>U)∩U" using inj_vimage_image invb unfolding bij_def
by auto
finally have "(\<sm>?V)=?V" by auto
then show "?V ⊆ U ∧ (\<sm> ?V) = ?V" by auto
from assms have "(\<sm>U)∈𝒩⇩0" using neg_neigh_neigh by auto
with assms have "𝟬 ∈ int(U)∩int(\<sm>U)" unfolding zerohoods_def by auto
moreover have "int(U)∩int(\<sm>U) = int(?V)" using int_inter_int by simp
ultimately have "𝟬 ∈ int(?V)" by (rule set_mem_eq)
with ‹?V⊆G› show "?V∈𝒩⇩0" using zerohoods_def by auto
qed
text‹ We can say even more than in ‹exists_sym_zerohood›:
every neighborhood of zero $U$ has a symmetric subset that is a neighborhood of zero and its
set double is contained in $U$.›
theorem (in topgroup) exists_procls_zerohood:
assumes "U∈𝒩⇩0"
shows "∃V∈𝒩⇩0. (V⊆U∧ (V\<sad>V)⊆U ∧ (\<sm>V)=V)"
proof-
have "int(U)∈T" using Top_2_L2 by auto
then have "f-``(int(U))∈τ" using fcon IsContinuous_def by auto
moreover have fne:"f ` ⟨𝟬, 𝟬⟩ = 𝟬" using group0_2_L2 by auto
moreover
have "𝟬∈int(U)" using assms unfolding zerohoods_def by auto
then have "f -`` {𝟬}⊆f-``(int(U))" using func1_1_L8 vimage_def by auto
then have "GroupInv(G,f)⊆f-``(int(U))" using group0_2_T3 by auto
then have "⟨𝟬,𝟬⟩∈f-``(int(U))" using fne zero_in_tgroup unfolding GroupInv_def
by auto
ultimately obtain W V where
wop:"W∈T" and vop:"V∈T" and cartsub:"W×V⊆f-``(int(U))" and zerhood:"⟨𝟬,𝟬⟩∈W×V"
using prod_top_point_neighb topSpaceAssum
unfolding prodtop_def by force
then have "𝟬∈W" and "𝟬∈V" by auto
then have "𝟬∈W∩V" by auto
have sub:"W∩V⊆G" using wop vop G_def by auto
have assoc:"f∈G×G→G" using group_oper_fun by auto
{
fix t s assume "t∈W∩V" and "s∈W∩V"
then have "t∈W" and "s∈V" by auto
then have "⟨t,s⟩∈W×V" by auto
then have "⟨t,s⟩∈f-``(int(U))" using cartsub by auto
then have "f`⟨t,s⟩∈int(U)" using func1_1_L15 assoc by auto
} hence "{f`⟨t,s⟩. ⟨t,s⟩∈(W∩V)×(W∩V)}⊆int(U)" by auto
then have "(W∩V)\<sad>(W∩V)⊆int(U)"
unfolding setadd_def using lift_subsets_explained(4) assoc sub
by auto
then have "(W∩V)\<sad>(W∩V)⊆U" using Top_2_L1 by auto
from topSpaceAssum have "W∩V∈T" using vop wop unfolding IsATopology_def by auto
then have "int(W∩V)=W∩V" using Top_2_L3 by auto
with sub ‹𝟬∈W∩V› have "W∩V∈𝒩⇩0" unfolding zerohoods_def by auto
then obtain Q where "Q∈𝒩⇩0" and "Q⊆W∩V" and "(\<sm>Q)=Q" using exists_sym_zerohood by blast
then have "Q×Q⊆(W∩V)×(W∩V)" by auto
moreover from ‹Q⊆W∩V› have "W∩V⊆G" and "Q⊆G" using vop wop unfolding G_def by auto
ultimately have "Q\<sad>Q⊆(W∩V)\<sad>(W∩V)" using interval_add(2) func1_1_L8 by auto
with ‹(W∩V)\<sad>(W∩V)⊆U› have "Q\<sad>Q⊆U" by auto
from ‹Q∈𝒩⇩0› have "𝟬∈Q" unfolding zerohoods_def using Top_2_L1 by auto
with ‹Q\<sad>Q⊆U› ‹Q⊆G› have "𝟬\<ltr>Q⊆U" using interval_add(3) by auto
with ‹Q⊆G› have "Q⊆U" unfolding ltrans_def gzero_def using trans_neutral(2) image_id_same
by auto
with ‹Q∈𝒩⇩0› ‹Q\<sad>Q⊆U› ‹(\<sm>Q)=Q› show ?thesis by auto
qed
subsection‹Closure in topological groups›
text‹This section is devoted to a characterization of closure
in topological groups.›
text‹Closure of a set is contained in the sum of the set and any
neighboorhood of zero.›
lemma (in topgroup) cl_contains_zneigh:
assumes A1: "A⊆G" and A2: "H ∈ 𝒩⇩0"
shows "cl(A) ⊆ A\<sad>H"
proof
fix x assume "x ∈ cl(A)"
from A1 have "cl(A) ⊆ G" using Top_3_L11 by simp
with ‹x ∈ cl(A)› have "x∈G" by auto
have "int(H) ⊆ G" using Top_2_L2 by auto
let ?V = "int(x \<ltr> (\<sm>H))"
have "?V = x \<ltr> (\<sm>int(H))"
proof -
from A2 ‹x∈G› have "?V = x \<ltr> int(\<sm>H)"
using neg_neigh_neigh ltrans_interior by simp
with A2 show ?thesis using int_inv_inv_int by simp
qed
have "A∩?V ≠ 0"
proof -
from A2 ‹x∈G› ‹x ∈ cl(A)› have "?V∈T" and "x ∈ cl(A) ∩ ?V"
using neg_neigh_neigh elem_in_int_ltrans(1) Top_2_L2 by auto
with A1 show "A∩?V ≠ 0" using cl_inter_neigh by simp
qed
then obtain y where "y∈A" and "y∈?V" by auto
with ‹?V = x \<ltr> (\<sm>int(H))› ‹int(H) ⊆ G› ‹x∈G› have "x ∈ y\<ltr>int(H)"
using ltrans_inv_in by simp
with ‹y∈A› have "x ∈ (⋃y∈A. y\<ltr>H)" using Top_2_L1 func1_1_L8 by auto
with assms show "x ∈ A\<sad>H" using interval_add(3) by simp
qed
text‹The next theorem provides a characterization of closure in topological
groups in terms of neighborhoods of zero.›
theorem (in topgroup) cl_topgroup:
assumes "A⊆G" shows "cl(A) = (⋂H∈𝒩⇩0. A\<sad>H)"
proof
from assms show "cl(A) ⊆ (⋂H∈𝒩⇩0. A\<sad>H)"
using zneigh_not_empty cl_contains_zneigh by auto
next
{ fix x assume "x ∈ (⋂H∈𝒩⇩0. A\<sad>H)"
then have "x ∈ A\<sad>G" using zneigh_not_empty by auto
with assms have "x∈G" using interval_add by blast
have "∀U∈T. x∈U ⟶ U∩A ≠ 0"
proof -
{ fix U assume "U∈T" and "x∈U"
let ?H = "\<sm>((\<rm>x)\<ltr>U)"
from ‹U∈T› and ‹x∈U› have "(\<rm>x)\<ltr>U ⊆ G" and "?H ∈ 𝒩⇩0"
using open_trans_neigh neg_neigh_neigh by auto
with ‹x ∈ (⋂H∈𝒩⇩0. A\<sad>H)› have "x ∈ A\<sad>?H" by auto
with assms ‹?H ∈ 𝒩⇩0› obtain y where "y∈A" and "x ∈ y\<ltr>?H"
using interval_add(3) by auto
have "y∈U"
proof -
from assms ‹y∈A› have "y∈G" by auto
with ‹(\<rm>x)\<ltr>U ⊆ G› and ‹x ∈ y\<ltr>?H› have "y ∈ x\<ltr>((\<rm>x)\<ltr>U)"
using ltrans_inv_in by simp
with ‹U∈T› ‹x∈G› show "y∈U"
using neg_in_tgroup trans_comp_image group0_2_L6 trans_neutral image_id_same
by auto
qed
with ‹y∈A› have "U∩A ≠ 0" by auto
} thus ?thesis by simp
qed
with assms ‹x∈G› have "x ∈ cl(A)" using inter_neigh_cl by simp
} thus "(⋂H∈𝒩⇩0. A\<sad>H) ⊆ cl(A)" by auto
qed
subsection‹Sums of sequences of elements and subsets›
text‹In this section we consider properties of the function $G^n\rightarrow G$,
$x=(x_0,x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i$. We will model the cartesian product
$G^n$ by the space of sequences $n\rightarrow G$, where $n=\{0,1,...,n-1 \}$ is a natural number.
This space is equipped with a natural product topology defined in ‹Topology_ZF_3›.›
text‹Let's recall first that the sum of elements of a group is an element of the group.›
lemma (in topgroup) sum_list_in_group:
assumes "n ∈ nat" and "x: succ(n)→G"
shows "(∑x) ∈ G"
proof -
from assms have "semigr0(G,f)" and "n ∈ nat" "x: succ(n)→G"
using semigr0_valid_in_tgroup by auto
then have "Fold1(f,x) ∈ G" by (rule semigr0.prod_type)
thus "(∑x) ∈ G" by simp
qed
text‹In this context ‹x\<ra>y› is the same as the value of the group operation
on the elements $x$ and $y$. Normally we shouldn't need to state this a s separate lemma.›
lemma (in topgroup) grop_def1: shows "f`⟨x,y⟩ = x\<ra>y" by simp
text‹Another theorem from ‹Semigroup_ZF› theory that is useful to have in the
additive notation.›
lemma (in topgroup) shorter_set_add:
assumes "n ∈ nat" and "x: succ(succ(n))→G"
shows "(∑x) = (∑Init(x)) \<ra> (x`(succ(n)))"
proof -
from assms have "semigr0(G,f)" and "n ∈ nat" "x: succ(succ(n))→G"
using semigr0_valid_in_tgroup by auto
then have "Fold1(f,x) = f`⟨Fold1(f,Init(x)),x`(succ(n))⟩"
by (rule semigr0.shorter_seq)
thus ?thesis by simp
qed
text‹Sum is a continuous function in the product topology.›
theorem (in topgroup) sum_continuous: assumes "n ∈ nat"
shows "IsContinuous(SeqProductTopology(succ(n),T),T,{⟨x,∑x⟩.x∈succ(n)→G})"
proof -
note ‹n ∈ nat›
moreover have "IsContinuous(SeqProductTopology(succ(0),T),T,{⟨x,∑x⟩.x∈succ(0)→G})"
proof -
have "{⟨x,∑x⟩.x∈succ(0)→G} = {⟨x,x`(0)⟩. x∈1→G}"
using semigr0_valid_in_tgroup semigr0.prod_of_1elem by simp
moreover have
"IsAhomeomorphism(SeqProductTopology(1,T),T,{⟨x,x`(0)⟩. x∈1→⋃T})" using topSpaceAssum singleton_prod_top1
by simp
ultimately show ?thesis using IsAhomeomorphism_def by simp
qed
moreover have "∀k∈nat.
IsContinuous(SeqProductTopology(succ(k),T),T,{⟨x,∑x⟩.x∈succ(k)→G})
⟶
IsContinuous(SeqProductTopology(succ(succ(k)),T),T,{⟨x,∑x⟩.x∈succ(succ(k))→G})"
proof -
{ fix k assume "k ∈ nat"
let ?s = "{⟨x,∑x⟩.x∈succ(k)→G}"
let ?g = "{⟨p,⟨?s`(fst(p)),snd(p)⟩⟩. p ∈ (succ(k)→G)×G}"
let ?h = "{⟨x,⟨Init(x),x`(succ(k))⟩⟩. x ∈ succ(succ(k))→G}"
let ?φ = "SeqProductTopology(succ(k),T)"
let ?ψ = "SeqProductTopology(succ(succ(k)),T)"
assume "IsContinuous(?φ,T,?s)"
from ‹k ∈ nat› have "?s: (succ(k)→G) → G"
using sum_list_in_group ZF_fun_from_total by simp
have "?h: (succ(succ(k))→G)→(succ(k)→G)×G"
proof -
{ fix x assume "x ∈ succ(succ(k))→G"
with ‹k ∈ nat› have "Init(x) ∈ (succ(k)→G)"
using init_props by simp
with ‹k ∈ nat› ‹x : succ(succ(k))→G›
have "⟨Init(x),x`(succ(k))⟩ ∈ (succ(k)→G)×G" using apply_funtype
by blast
} then show ?thesis using ZF_fun_from_total by simp
qed
moreover have "?g:((succ(k)→G)×G)→(G×G)"
proof -
{ fix p assume "p ∈ (succ(k)→G)×G"
hence "fst(p): succ(k)→G" and "snd(p) ∈ G" by auto
with ‹?s: (succ(k)→G) → G› have "⟨?s`(fst(p)),snd(p)⟩ ∈ G×G"
using apply_funtype by blast
} then show "?g:((succ(k)→G)×G)→(G×G)" using ZF_fun_from_total
by simp
qed
moreover have "f : G×G → G" using topgroup_f_binop by simp
ultimately have "f O ?g O ?h :(succ(succ(k))→G)→G" using comp_fun
by blast
from ‹k ∈ nat› have "IsContinuous(?ψ,ProductTopology(?φ,T),?h)"
using topSpaceAssum finite_top_prod_homeo IsAhomeomorphism_def
by simp
moreover have "IsContinuous(ProductTopology(?φ,T),τ,?g)"
proof -
from topSpaceAssum have
"T {is a topology}" "?φ {is a topology}" "⋃?φ = succ(k)→G"
using seq_prod_top_is_top by auto
moreover from ‹⋃?φ = succ(k)→G› ‹?s: (succ(k)→G) → G›
have "?s:⋃?φ→⋃T" by simp
moreover note ‹IsContinuous(?φ,T,?s)›
moreover from ‹⋃?φ = succ(k)→G›
have "?g = {⟨p,⟨?s`(fst(p)),snd(p)⟩⟩. p ∈ ⋃?φ×⋃T}"
by simp
ultimately have "IsContinuous(ProductTopology(?φ,T),ProductTopology(T,T),?g)"
using cart_prod_cont1 by blast
thus ?thesis by simp
qed
moreover have "IsContinuous(τ,T,f)" using fcon by simp
moreover have "{⟨x,∑x⟩.x∈succ(succ(k))→G} = f O ?g O ?h"
proof -
let ?d = "{⟨x,∑x⟩.x∈succ(succ(k))→G}"
from ‹k∈nat› have "∀x∈succ(succ(k))→G. (∑x) ∈ G"
using sum_list_in_group by blast
then have "?d:(succ(succ(k))→G)→G"
using sum_list_in_group ZF_fun_from_total by simp
moreover note ‹f O ?g O ?h :(succ(succ(k))→G)→G›
moreover have "∀x∈succ(succ(k))→G. ?d`(x) = (f O ?g O ?h)`(x)"
proof
fix x assume "x∈succ(succ(k))→G"
then have I: "?h`(x) = ⟨Init(x),x`(succ(k))⟩"
using ZF_fun_from_tot_val1 by simp
moreover from ‹k∈nat› ‹x∈succ(succ(k))→G›
have "Init(x): succ(k)→G"
using init_props by simp
moreover from ‹k∈nat› ‹x:succ(succ(k))→G›
have II: "x`(succ(k)) ∈ G"
using apply_funtype by blast
ultimately have "?h`(x) ∈ (succ(k)→G)×G" by simp
then have "?g`(?h`(x)) = ⟨?s`(fst(?h`(x))),snd(?h`(x))⟩"
using ZF_fun_from_tot_val1 by simp
with I have "?g`(?h`(x)) = ⟨?s`(Init(x)),x`(succ(k))⟩"
by simp
with ‹Init(x): succ(k)→G› have "?g`(?h`(x)) = ⟨∑Init(x),x`(succ(k))⟩"
using ZF_fun_from_tot_val1 by simp
with ‹k ∈ nat› ‹x: succ(succ(k))→G›
have "f`(?g`(?h`(x))) = (∑x)"
using shorter_set_add by simp
with ‹x ∈ succ(succ(k))→G› have "f`(?g`(?h`(x))) = ?d`(x)"
using ZF_fun_from_tot_val1 by simp
moreover from
‹?h: (succ(succ(k))→G)→(succ(k)→G)×G›
‹?g:((succ(k)→G)×G)→(G×G)›
‹f:(G×G)→G› ‹x∈succ(succ(k))→G›
have "(f O ?g O ?h)`(x) = f`(?g`(?h`(x)))" by (rule func1_1_L18)
ultimately show "?d`(x) = (f O ?g O ?h)`(x)" by simp
qed
ultimately show "{⟨x,∑x⟩.x∈succ(succ(k))→G} = f O ?g O ?h"
using func_eq by simp
qed
moreover note ‹IsContinuous(τ,T,f)›
ultimately have "IsContinuous(?ψ,T,{⟨x,∑x⟩.x∈succ(succ(k))→G})"
using comp_cont3 by simp
} thus ?thesis by simp
qed
ultimately show ?thesis by (rule ind_on_nat)
qed
end