section ‹Topological groups 2›
theory TopologicalGroup_ZF_2 imports Topology_ZF_8 TopologicalGroup_ZF Group_ZF_2
begin
text‹This theory deals with quotient topological groups.›
subsection‹Quotients of topological groups›
text‹The quotient topology given by the quotient group equivalent relation, has
an open quotient map.›
theorem(in topgroup) quotient_map_topgroup_open:
assumes "IsAsubgroup(H,f)" "A∈T"
defines "r ≡ QuotientGroupRel(G,f,H)"
shows "{⟨b,r``{b}⟩. b∈⋃T}``A∈(T{quotient by}r)"
proof-
have eqT:"equiv(⋃T,r)" and eqG:"equiv(G,r)" using group0.Group_ZF_2_4_L3 assms(1) unfolding r_def IsAnormalSubgroup_def
using group0_valid_in_tgroup by auto
have subA:"A⊆G" using assms(2) by auto
have subH:"H⊆G" using group0.group0_3_L2[OF group0_valid_in_tgroup assms(1)].
have A1:"{⟨b,r``{b}⟩. b∈⋃T}-``({⟨b,r``{b}⟩. b∈⋃T}``A)=H\<sad>A"
proof
{
fix t assume "t∈{⟨b,r``{b}⟩. b∈⋃T}-``({⟨b,r``{b}⟩. b∈⋃T}``A)"
then have "∃m∈({⟨b,r``{b}⟩. b∈⋃T}``A). ⟨t,m⟩∈{⟨b,r``{b}⟩. b∈⋃T}" using vimage_iff by auto
then obtain m where "m∈({⟨b,r``{b}⟩. b∈⋃T}``A)""⟨t,m⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto
then obtain b where "b∈A""⟨b,m⟩∈{⟨b,r``{b}⟩. b∈⋃T}""t∈G" and rel:"r``{t}=m" using image_iff by auto
then have "r``{b}=m" by auto
then have "r``{t}=r``{b}" using rel by auto
with ‹b∈A›subA have "⟨t,b⟩∈r" using eq_equiv_class[OF _ eqT] by auto
then have "f`⟨t,GroupInv(G,f)`b⟩∈H" unfolding r_def QuotientGroupRel_def by auto
then obtain h where "h∈H" and prd:"f`⟨t,GroupInv(G,f)`b⟩=h" by auto
then have "h∈G" using subH by auto
have "b∈G" using ‹b∈A›‹A∈T› by auto
then have "(\<rm>b)∈G" using neg_in_tgroup by auto
from prd have "t=f`⟨h, GroupInv(G, f) ` (\<rm> b)⟩" using group0.group0_2_L18(1)[OF group0_valid_in_tgroup ‹t∈G›‹(\<rm>b)∈G›‹h∈G›]
unfolding grinv_def by auto
then have "t=f`⟨h,b⟩" using group0.group_inv_of_inv[OF group0_valid_in_tgroup ‹b∈G›]
unfolding grinv_def by auto
then have "⟨⟨h,b⟩,t⟩∈f" using apply_Pair[OF topgroup_f_binop] ‹h∈G›‹b∈G› by auto moreover
from ‹h∈H›‹b∈A› have "⟨h,b⟩∈H×A" by auto
ultimately have "t∈f``(H×A)" using image_iff by auto
with subA subH have "t∈H\<sad>A" using interval_add(2) by auto
}
then show "({⟨b,r``{b}⟩. b∈⋃T}-``({⟨b,r``{b}⟩. b∈⋃T}``A))⊆H\<sad>A" by force
{
fix t assume "t∈H\<sad>A"
with subA subH have "t∈f``(H×A)" using interval_add(2) by auto
then obtain ha where "ha∈H×A""⟨ha,t⟩∈f" using image_iff by auto
then obtain h aa where "ha=⟨h,aa⟩""h∈H""aa∈A" by auto
then have "h∈G""aa∈G" using subH subA by auto
from ‹⟨ha,t⟩∈f› have "t∈G" using topgroup_f_binop unfolding Pi_def by auto
from ‹ha=⟨h,aa⟩› ‹⟨ha,t⟩∈f› have "t=f`⟨h,aa⟩" using apply_equality[OF _ topgroup_f_binop] by auto
then have "f`⟨t,\<rm>aa⟩=h" using group0.group0_2_L18(1)[OF group0_valid_in_tgroup ‹h∈G›‹aa∈G›‹t∈G›]
by auto
with ‹h∈H›‹t∈G›‹aa∈G› have "⟨t,aa⟩∈r" unfolding r_def QuotientGroupRel_def by auto
then have "r``{t}=r``{aa}" using eqT equiv_class_eq by auto
with ‹aa∈G› have "⟨aa,r``{t}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto
with ‹aa∈A› have A1:"r``{t}∈({⟨b,r``{b}⟩. b∈⋃T}``A)" using image_iff by auto
from ‹t∈G› have "⟨t,r``{t}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto
with A1 have "t∈{⟨b,r``{b}⟩. b∈⋃T}-``({⟨b,r``{b}⟩. b∈⋃T}``A)" using vimage_iff by auto
}
then show "H\<sad>A⊆{⟨b,r``{b}⟩. b∈⋃T}-``({⟨b,r``{b}⟩. b∈⋃T}``A)" by auto
qed
have "H\<sad>A=(⋃x∈H. x \<ltr> A)" using interval_add(3) subH subA by auto moreover
have "∀x∈H. x \<ltr> A∈T" using open_tr_open(1) assms(2) subH by blast
then have "{x \<ltr> A. x∈H}⊆T" by auto
then have "(⋃x∈H. x \<ltr> A)∈T" using topSpaceAssum unfolding IsATopology_def by auto
ultimately have "H\<sad>A∈T" by auto
with A1 have "{⟨b,r``{b}⟩. b∈⋃T}-``({⟨b,r``{b}⟩. b∈⋃T}``A)∈T" by auto
then have "({⟨b,r``{b}⟩. b∈⋃T}``A)∈{quotient topology in}((⋃T)//r){by}{⟨b,r``{b}⟩. b∈⋃T}{from}T"
using QuotientTop_def topSpaceAssum quotient_proj_surj using
func1_1_L6(2)[OF quotient_proj_fun] by auto
then show "({⟨b,r``{b}⟩. b∈⋃T}``A)∈(T{quotient by}r)" using EquivQuo_def[OF eqT] by auto
qed
text‹A quotient of a topological group is just a quotient group with an appropiate
topology that makes product and inverse continuous.›
theorem (in topgroup) quotient_top_group_F_cont:
assumes "IsAnormalSubgroup(G,f,H)"
defines "r ≡ QuotientGroupRel(G,f,H)"
defines "F ≡ QuotientGroupOp(G,f,H)"
shows "IsContinuous(ProductTopology(T{quotient by}r,T{quotient by}r),T{quotient by}r,F)"
proof-
have eqT:"equiv(⋃T,r)" and eqG:"equiv(G,r)" using group0.Group_ZF_2_4_L3 assms(1) unfolding r_def IsAnormalSubgroup_def
using group0_valid_in_tgroup by auto
have fun:"{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:G×G→(G//r)×(G//r)" using product_equiv_rel_fun unfolding G_def by auto
have C:"Congruent2(r,f)" using Group_ZF_2_4_L5A[OF Ggroup assms(1)] unfolding r_def.
with eqT have "IsContinuous(ProductTopology(T,T),ProductTopology(T{quotient by}r,T{quotient by}r),{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})"
using product_quo_fun by auto
have tprod:"topology0(ProductTopology(T,T))" unfolding topology0_def using Top_1_4_T1(1)[OF topSpaceAssum topSpaceAssum].
have Hfun:"{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}∈surj(⋃ProductTopology(T,T),⋃(({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))))" using prod_equiv_rel_surj
total_quo_equi[OF eqT] topology0.total_quo_func[OF tprod prod_equiv_rel_surj] unfolding F_def QuotientGroupOp_def r_def
by auto
have Ffun:"F:⋃(({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T))))→⋃(T{quotient by}r)"
using EquivClass_1_T1[OF eqG C] using total_quo_equi[OF eqT] topology0.total_quo_func[OF tprod prod_equiv_rel_surj] unfolding F_def QuotientGroupOp_def r_def
by auto
have cc:"(F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}):G×G→G//r" using comp_fun[OF fun EquivClass_1_T1[OF eqG C]]
unfolding F_def QuotientGroupOp_def r_def by auto
then have "(F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}):⋃(ProductTopology(T,T))→⋃(T{quotient by}r)" using Top_1_4_T1(3)[OF topSpaceAssum topSpaceAssum]
total_quo_equi[OF eqT] by auto
then have two:"two_top_spaces0(ProductTopology(T,T),T{quotient by}r,(F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}))" unfolding two_top_spaces0_def
using Top_1_4_T1(1)[OF topSpaceAssum topSpaceAssum] equiv_quo_is_top[OF eqT] by auto
have "IsContinuous(ProductTopology(T,T),T,f)" using fcon prodtop_def by auto moreover
have "IsContinuous(T,T{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont[OF quotient_proj_surj]
unfolding EquivQuo_def[OF eqT] by auto
ultimately have cont:"IsContinuous(ProductTopology(T,T),T{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T} O f)"
using comp_cont by auto
{
fix A assume A:"A∈G×G"
then obtain g1 g2 where A_def:"A=⟨g1,g2⟩" "g1∈G""g2∈G" by auto
then have "f`A=g1\<ra>g2" and p:"g1\<ra>g2∈⋃T" unfolding grop_def using
apply_type[OF topgroup_f_binop] by auto
then have "{⟨b,r``{b}⟩. b∈⋃T}`(f`A)={⟨b,r``{b}⟩. b∈⋃T}`(g1\<ra>g2)" by auto
with p have "{⟨b,r``{b}⟩. b∈⋃T}`(f`A)=r``{g1\<ra>g2}" using apply_equality[OF _ quotient_proj_fun]
by auto
then have Pr1:"({⟨b,r``{b}⟩. b∈⋃T} O f)`A=r``{g1\<ra>g2}" using comp_fun_apply[OF topgroup_f_binop A] by auto
from A_def(2,3) have "⟨g1,g2⟩∈⋃T×⋃T" by auto
then have "⟨⟨g1,g2⟩,⟨r``{g1},r``{g2}⟩⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto
then have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`A=⟨r``{g1},r``{g2}⟩" using A_def(1) apply_equality[OF _ product_equiv_rel_fun]
by auto
then have "F`({⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`A)=F`⟨r``{g1},r``{g2}⟩" by auto
then have "F`({⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`A)=r``({g1\<ra>g2})" using group0.Group_ZF_2_2_L2[OF group0_valid_in_tgroup eqG C
_ A_def(2,3)] unfolding F_def QuotientGroupOp_def r_def by auto moreover
note fun ultimately have "(F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})`A=r``({g1\<ra>g2})" using comp_fun_apply[OF _ A] by auto
then have "(F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})`A=({⟨b,r``{b}⟩. b∈⋃T} O f)`A" using Pr1 by auto
}
then have "(F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})=({⟨b,r``{b}⟩. b∈⋃T} O f)" using fun_extension[OF cc comp_fun[OF topgroup_f_binop quotient_proj_fun]]
unfolding F_def QuotientGroupOp_def r_def by auto
then have A:"IsContinuous(ProductTopology(T,T),T{quotient by}r,F O {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})" using cont by auto
have "IsAsubgroup(H,f)" using assms(1) unfolding IsAnormalSubgroup_def by auto
then have "∀A∈T. {⟨b, r `` {b}⟩ . b ∈ ⋃T} `` A ∈ ({quotient by}r)" using quotient_map_topgroup_open unfolding r_def by auto
with eqT have "ProductTopology({quotient by}r,{quotient by}r)=({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))" using prod_quotient
by auto
with A show "IsContinuous(ProductTopology(T{quotient by}r,T{quotient by}r),T{quotient by}r,F)"
using two_top_spaces0.cont_quotient_top[OF two Hfun Ffun] topology0.total_quo_func[OF tprod prod_equiv_rel_surj] unfolding F_def QuotientGroupOp_def r_def
by auto
qed
lemma (in group0) Group_ZF_2_4_L8:
assumes "IsAnormalSubgroup(G,P,H)"
defines "r ≡ QuotientGroupRel(G,P,H)"
and "F ≡ QuotientGroupOp(G,P,H)"
shows "GroupInv(G//r,F):G//r→G//r"
using group0_2_T2[OF Group_ZF_2_4_T1[OF _ assms(1)]] groupAssum using assms(2,3)
by auto
theorem (in topgroup) quotient_top_group_INV_cont:
assumes "IsAnormalSubgroup(G,f,H)"
defines "r ≡ QuotientGroupRel(G,f,H)"
defines "F ≡ QuotientGroupOp(G,f,H)"
shows "IsContinuous(T{quotient by}r,T{quotient by}r,GroupInv(G//r,F))"
proof-
have eqT:"equiv(⋃T,r)" and eqG:"equiv(G,r)" using group0.Group_ZF_2_4_L3 assms(1) unfolding r_def IsAnormalSubgroup_def
using group0_valid_in_tgroup by auto
have two:"two_top_spaces0(T,T{quotient by}r,{⟨b,r``{b}⟩. b∈G})" unfolding two_top_spaces0_def
using topSpaceAssum equiv_quo_is_top[OF eqT] quotient_proj_fun total_quo_equi[OF eqT] by auto
have "IsContinuous(T,T,GroupInv(G,f))" using inv_cont. moreover
{
fix g assume G:"g∈G"
then have "GroupInv(G,f)`g=\<rm>g" using grinv_def by auto
then have "r``({GroupInv(G,f)`g})=GroupInv(G//r,F)`(r``{g})" using group0.Group_ZF_2_4_L7
[OF group0_valid_in_tgroup assms(1) G] unfolding r_def F_def by auto
then have "{⟨b,r``{b}⟩. b∈G}`(GroupInv(G,f)`g)=GroupInv(G//r,F)`({⟨b,r``{b}⟩. b∈G}`g)"
using apply_equality[OF _ quotient_proj_fun] G neg_in_tgroup unfolding grinv_def
by auto
then have "({⟨b,r``{b}⟩. b∈G}O GroupInv(G,f))`g=(GroupInv(G//r,F)O {⟨b,r``{b}⟩. b∈G})`g"
using comp_fun_apply[OF quotient_proj_fun G] comp_fun_apply[OF group0_2_T2[OF Ggroup] G] by auto
}
then have A1:"{⟨b,r``{b}⟩. b∈G}O GroupInv(G,f)=GroupInv(G//r,F)O {⟨b,r``{b}⟩. b∈G}" using fun_extension[
OF comp_fun[OF quotient_proj_fun group0.Group_ZF_2_4_L8[OF group0_valid_in_tgroup assms(1)]]
comp_fun[OF group0_2_T2[OF Ggroup] quotient_proj_fun[of "G""r"]]] unfolding r_def F_def by auto
have "IsContinuous(T,T{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont[OF quotient_proj_surj]
unfolding EquivQuo_def[OF eqT] by auto
ultimately have "IsContinuous(T,T{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T}O GroupInv(G,f))"
using comp_cont by auto
with A1 have "IsContinuous(T,T{quotient by}r,GroupInv(G//r,F)O {⟨b,r``{b}⟩. b∈G})" by auto
then have "IsContinuous({quotient topology in}(⋃T) // r{by}{⟨b, r `` {b}⟩ . b ∈ ⋃T}{from}T,T{quotient by}r,GroupInv(G//r,F))"
using two_top_spaces0.cont_quotient_top[OF two quotient_proj_surj, of "GroupInv(G//r,F)""r"] group0.Group_ZF_2_4_L8[OF group0_valid_in_tgroup assms(1)]
using total_quo_equi[OF eqT] unfolding r_def F_def by auto
then show ?thesis unfolding EquivQuo_def[OF eqT].
qed
text‹Finally we can prove that quotient groups of topological groups
are topological groups.›
theorem(in topgroup) quotient_top_group:
assumes "IsAnormalSubgroup(G,f,H)"
defines "r ≡ QuotientGroupRel(G,f,H)"
defines "F ≡ QuotientGroupOp(G,f,H)"
shows "IsAtopologicalGroup({quotient by}r,F)"
unfolding IsAtopologicalGroup_def using total_quo_equi equiv_quo_is_top
Group_ZF_2_4_T1 Ggroup assms(1) quotient_top_group_INV_cont quotient_top_group_F_cont
group0.Group_ZF_2_4_L3 group0_valid_in_tgroup assms(1) unfolding r_def F_def IsAnormalSubgroup_def
by auto
end