Theory TopologicalGroup_ZF_2

theory TopologicalGroup_ZF_2
imports Topology_ZF_8 TopologicalGroup_ZF Group_ZF_2
(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2013 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

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