src/HOL/Algebra/Zassenhaus.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 68466 3d8241f4198b
child 68555 22d51874f37d
permissions -rw-r--r--
More on Algebra by Paulo and Martin
lp15@68466
     1
(*  Title:      HOL/Algebra/Zassenhaus.thy
lp15@68466
     2
    Author:     Martin Baillon
lp15@68466
     3
*)
lp15@68466
     4
lp15@68466
     5
section \<open>The Zassenhaus Lemma\<close>
lp15@68466
     6
lp15@68443
     7
theory Zassenhaus
lp15@68443
     8
  imports Coset Group_Action
lp15@68443
     9
begin
lp15@68443
    10
lp15@68466
    11
text \<open>Proves the second isomorphism theorem and the Zassenhaus lemma.\<close>
lp15@68443
    12
lp15@68466
    13
subsection \<open>Lemmas about normalizer\<close>
lp15@68443
    14
lp15@68466
    15
lemma (in group) subgroup_in_normalizer:
lp15@68443
    16
  assumes "subgroup H G"
lp15@68443
    17
  shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
lp15@68443
    18
proof(intro group.normal_invI)
lp15@68443
    19
  show "Group.group (G\<lparr>carrier := normalizer G H\<rparr>)"
lp15@68452
    20
    by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset)
lp15@68443
    21
  have K:"H \<subseteq> (normalizer G H)" unfolding normalizer_def
lp15@68443
    22
  proof
lp15@68443
    23
    fix x assume xH: "x \<in> H"
lp15@68452
    24
    from xH have xG : "x \<in> carrier G" using subgroup.subset assms by auto
lp15@68443
    25
    have "x <# H = H"
lp15@68443
    26
      by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
lp15@68452
    27
         l_repr_independence one_closed subgroup.subset)
lp15@68466
    28
    moreover have "H #> inv x = H"
lp15@68443
    29
      by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
lp15@68443
    30
    ultimately have "x <# H #> (inv x) = H" by simp
lp15@68443
    31
    thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H"
lp15@68452
    32
      using assms xG subgroup.subset unfolding stabilizer_def by auto
lp15@68443
    33
  qed
lp15@68443
    34
  thus "subgroup H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
lp15@68452
    35
    using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset)
lp15@68443
    36
  show  " \<And>x h. x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>) \<Longrightarrow> h \<in> H \<Longrightarrow>
lp15@68443
    37
             x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
lp15@68443
    38
               \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
lp15@68443
    39
    proof-
lp15@68443
    40
    fix x h assume xnorm : "x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>)" and hH : "h \<in> H"
lp15@68443
    41
    have xnormalizer:"x \<in> normalizer G H" using xnorm by simp
lp15@68443
    42
    moreover have hnormalizer:"h \<in> normalizer G H" using hH K by auto
lp15@68443
    43
    ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
lp15@68443
    44
    moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x =  inv x"
lp15@68443
    45
      using xnormalizer
lp15@68452
    46
      by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
lp15@68443
    47
    ultimately  have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
lp15@68443
    48
                \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
lp15@68443
    49
                  = x \<otimes>h \<otimes> inv x"
lp15@68443
    50
      using  hnormalizer by simp
lp15@68443
    51
    have  "x \<otimes>h \<otimes> inv x \<in> (x <# H #> inv x)"
lp15@68443
    52
      unfolding l_coset_def r_coset_def using hH  by auto
lp15@68443
    53
    moreover have "x <# H #> inv x = H"
lp15@68452
    54
      using xnormalizer assms subgroup.subset[OF assms]
lp15@68443
    55
      unfolding normalizer_def stabilizer_def by auto
lp15@68443
    56
    ultimately have "x \<otimes>h \<otimes> inv x \<in> H" by simp
lp15@68443
    57
    thus  " x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
lp15@68443
    58
               \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
lp15@68443
    59
      using xhxegal hH xnorm by simp
lp15@68443
    60
  qed
lp15@68443
    61
qed
lp15@68443
    62
lp15@68443
    63
lp15@68445
    64
lemma (in group) normal_imp_subgroup_normalizer:
lp15@68443
    65
  assumes "subgroup H G"
lp15@68445
    66
    and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
lp15@68466
    67
  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
lp15@68443
    68
proof-
lp15@68443
    69
  have N_carrierG : "N \<subseteq> carrier(G)"
lp15@68452
    70
    using assms normal_imp_subgroup subgroup.subset
lp15@68443
    71
    by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
lp15@68443
    72
  {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
lp15@68443
    73
    proof
lp15@68445
    74
      fix x assume xH : "x \<in> H"
lp15@68452
    75
      hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset  by auto
lp15@68445
    76
      have "   N #> x = x <# N" using assms xH
lp15@68445
    77
        unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
lp15@68445
    78
      hence "x <# N #> inv x =(N #> x) #> inv x"
lp15@68445
    79
        by simp
lp15@68445
    80
      also have "... = N #> \<one>"
lp15@68466
    81
        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp
lp15@68445
    82
      finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
lp15@68445
    83
      thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
lp15@68445
    84
        using xcarrierG by (simp add : N_carrierG)
lp15@68445
    85
    qed}
lp15@68443
    86
  thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
lp15@68443
    87
    using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
lp15@68452
    88
      assms normal_imp_subgroup subgroup.subset
lp15@68443
    89
    by (metis  group.incl_subgroup is_group)
lp15@68443
    90
qed
lp15@68443
    91
lp15@68443
    92
lp15@68443
    93
subsection \<open>Second Isomorphism Theorem\<close>
lp15@68443
    94
lp15@68445
    95
lemma (in group) mult_norm_subgroup:
lp15@68443
    96
  assumes "normal N G"
lp15@68443
    97
    and "subgroup H G"
lp15@68443
    98
  shows "subgroup (N<#>H) G" unfolding subgroup_def
lp15@68443
    99
proof-
lp15@68443
   100
  have  A :"N <#> H \<subseteq> carrier G"
lp15@68452
   101
    using assms  setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset)
lp15@68443
   102
lp15@68443
   103
  have B :"\<And> x y. \<lbrakk>x \<in> (N <#> H); y \<in> (N <#> H)\<rbrakk> \<Longrightarrow> (x \<otimes> y) \<in> (N<#>H)"
lp15@68443
   104
  proof-
lp15@68443
   105
    fix x y assume B1a: "x \<in> (N <#> H)"  and B1b: "y \<in> (N <#> H)"
lp15@68443
   106
    obtain n1 h1 where B2:"n1 \<in> N \<and> h1 \<in> H \<and> n1\<otimes>h1 = x"
lp15@68443
   107
      using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD)
lp15@68443
   108
    obtain n2 h2 where B3:"n2 \<in> N \<and> h2 \<in> H \<and> n2\<otimes>h2 = y"
lp15@68443
   109
      using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
lp15@68443
   110
    have "N #> h1 = h1 <# N"
lp15@68452
   111
      using normalI B2 assms normal.coset_eq subgroup.subset by blast
lp15@68466
   112
    hence "h1\<otimes>n2 \<in> N #> h1"
lp15@68443
   113
      using B2 B3 assms l_coset_def by fastforce
lp15@68466
   114
    from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2"
lp15@68466
   115
      using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
lp15@68443
   116
    have " x\<otimes>y =  n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3
lp15@68443
   117
      by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier)
lp15@68443
   118
    moreover have B4 :"n1 \<otimes> y2 \<in>N"
lp15@68443
   119
      using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def)
lp15@68443
   120
    moreover have "h1 \<otimes> h2 \<in>H" using B2 B3 assms by (simp add: subgroup.m_closed)
lp15@68443
   121
    hence "(n1 \<otimes> y2) \<otimes> (h1 \<otimes> h2) \<in>(N<#>H) "
lp15@68443
   122
      using B4  unfolding set_mult_def by auto
lp15@68443
   123
    hence "n1 \<otimes> y2 \<otimes> h1 \<otimes> h2 \<in>(N<#>H)"
lp15@68443
   124
      using m_assoc B2 B3 assms  normal_imp_subgroup by (metis B4 subgroup.mem_carrier)
lp15@68443
   125
    ultimately show  "x \<otimes> y \<in> N <#> H" by auto
lp15@68443
   126
  qed
lp15@68443
   127
  have C :"\<And> x. x\<in>(N<#>H)  \<Longrightarrow> (inv x)\<in>(N<#>H)"
lp15@68443
   128
lp15@68443
   129
  proof-
lp15@68443
   130
    fix x assume C1 : "x \<in> (N<#>H)"
lp15@68443
   131
    obtain n h where C2:"n \<in> N \<and> h \<in> H \<and> n\<otimes>h = x"
lp15@68443
   132
      using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD)
lp15@68443
   133
    have C3 :"inv(n\<otimes>h) = inv(h)\<otimes>inv(n)"
lp15@68443
   134
      by (meson C2  assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier)
lp15@68443
   135
    hence "... \<otimes>h \<in> N"
lp15@68443
   136
      using assms C2
lp15@68443
   137
      by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier)
lp15@68466
   138
    hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)"
lp15@68443
   139
      using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
lp15@68443
   140
    have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n"
lp15@68466
   141
      using  subgroup.subset[OF assms(2)]
lp15@68443
   142
      by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
lp15@68443
   143
    thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp
lp15@68443
   144
  qed
lp15@68443
   145
lp15@68443
   146
  have D : "\<one> \<in> N <#> H"
lp15@68443
   147
  proof-
lp15@68443
   148
    have D1 : "\<one> \<in> N"
lp15@68443
   149
      using assms by (simp add: normal_def subgroup.one_closed)
lp15@68443
   150
     have D2 :"\<one> \<in> H"
lp15@68443
   151
      using assms by (simp add: subgroup.one_closed)
lp15@68443
   152
    thus "\<one> \<in> (N <#> H)"
lp15@68443
   153
      using set_mult_def D1 assms by fastforce
lp15@68443
   154
  qed
lp15@68443
   155
  thus "(N <#> H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> N <#> H \<longrightarrow> y \<in> N <#> H \<longrightarrow> x \<otimes> y \<in> N <#> H)) \<and>
lp15@68443
   156
    \<one> \<in> N <#> H \<and> (\<forall>x. x \<in> N <#> H \<longrightarrow> inv x \<in> N <#> H)" using A B C D assms by blast
lp15@68443
   157
qed
lp15@68466
   158
lp15@68443
   159
lp15@68445
   160
lemma (in group) mult_norm_sub_in_sub:
lp15@68443
   161
  assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
lp15@68443
   162
  assumes "subgroup H (G\<lparr>carrier:=K\<rparr>)"
lp15@68443
   163
  assumes "subgroup K G"
lp15@68443
   164
  shows  "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)"
lp15@68443
   165
proof-
lp15@68443
   166
  have Hyp:"subgroup (N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) (G\<lparr>carrier := K\<rparr>)"
lp15@68443
   167
    using group.mult_norm_subgroup[where ?G = "G\<lparr>carrier := K\<rparr>"] assms subgroup_imp_group by auto
lp15@68452
   168
  have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup.subset by blast
lp15@68443
   169
  also have "... \<subseteq> K" by simp
lp15@68443
   170
  finally have Incl1:"H \<subseteq> K" by simp
lp15@68452
   171
  have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
lp15@68443
   172
  also have "... \<subseteq> K" by simp
lp15@68443
   173
  finally have Incl2:"N \<subseteq> K" by simp
lp15@68443
   174
  have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
lp15@68445
   175
    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
lp15@68443
   176
  thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
lp15@68443
   177
qed
lp15@68443
   178
lp15@68443
   179
lp15@68445
   180
lemma (in group) subgroup_of_normal_set_mult:
lp15@68443
   181
  assumes "normal N G"
lp15@68443
   182
and "subgroup H G"
lp15@68443
   183
shows "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
lp15@68443
   184
proof-
lp15@68443
   185
  have "\<one> \<in> N" using normal_imp_subgroup assms(1) subgroup_def by blast
lp15@68443
   186
  hence "\<one> <# H \<subseteq> N <#> H" unfolding set_mult_def l_coset_def by blast
lp15@68443
   187
  hence H_incl : "H \<subseteq> N <#> H"
lp15@68443
   188
    by (metis assms(2) lcos_mult_one subgroup_def)
lp15@68443
   189
  show "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
lp15@68443
   190
  using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] .
lp15@68443
   191
qed
lp15@68443
   192
lp15@68443
   193
lp15@68445
   194
lemma (in group) normal_in_normal_set_mult:
lp15@68443
   195
  assumes "normal N G"
lp15@68443
   196
and "subgroup H G"
lp15@68443
   197
shows "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
lp15@68443
   198
proof-
lp15@68443
   199
  have "\<one> \<in> H" using  assms(2) subgroup_def by blast
lp15@68443
   200
  hence "N #> \<one>  \<subseteq> N <#> H" unfolding set_mult_def r_coset_def by blast
lp15@68443
   201
  hence N_incl : "N \<subseteq> N <#> H"
lp15@68443
   202
    by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def)
lp15@68443
   203
  thus "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
lp15@68443
   204
    using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
lp15@68443
   205
    by (simp add : inf_absorb1)
lp15@68443
   206
qed
lp15@68443
   207
lp15@68443
   208
lp15@68445
   209
proposition (in group) weak_snd_iso_thme:
lp15@68466
   210
  assumes "subgroup  H G"
lp15@68443
   211
    and "N\<lhd>G"
lp15@68443
   212
  shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
lp15@68443
   213
proof-
lp15@68443
   214
  define f where "f =  (#>) N"
lp15@68443
   215
  have GroupNH : "Group.group (G\<lparr>carrier := N<#>H\<rparr>)"
lp15@68443
   216
    using subgroup_imp_group assms mult_norm_subgroup by simp
lp15@68443
   217
  have  HcarrierNH :"H \<subseteq> carrier(G\<lparr>carrier := N<#>H\<rparr>)"
lp15@68452
   218
    using assms subgroup_of_normal_set_mult subgroup.subset by blast
lp15@68443
   219
  hence HNH :"H \<subseteq> N<#>H" by simp
lp15@68443
   220
  have op_hom : "f \<in> hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N)" unfolding hom_def
lp15@68443
   221
  proof
lp15@68443
   222
    have "\<And>x . x \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<Longrightarrow>
lp15@68443
   223
       (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in>  carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   224
    proof-
lp15@68443
   225
      fix x assume  "x \<in> carrier (G\<lparr>carrier :=H\<rparr>)"
lp15@68443
   226
      hence xH : "x \<in> H" by simp
lp15@68443
   227
      hence "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in> rcosets\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> N"
lp15@68443
   228
        using HcarrierNH RCOSETS_def[where ?G = "G\<lparr>carrier := N <#> H\<rparr>"] by blast
lp15@68443
   229
      thus "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in>  carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   230
        unfolding FactGroup_def by simp
lp15@68443
   231
    qed
lp15@68443
   232
    hence "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<rightarrow>
lp15@68443
   233
            carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" by auto
lp15@68443
   234
    hence "f \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<rightarrow> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   235
      unfolding r_coset_def f_def  by simp
lp15@68443
   236
    moreover have "\<And>x y. x\<in>carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> y\<in>carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow>
lp15@68443
   237
                  f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)"
lp15@68443
   238
    proof-
lp15@68443
   239
      fix x y assume "x\<in>carrier (G\<lparr>carrier := H\<rparr>)" "y\<in>carrier (G\<lparr>carrier := H\<rparr>)"
lp15@68443
   240
      hence xHyH :"x \<in> H" "y \<in> H" by auto
lp15@68443
   241
      have Nxeq :"N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x = N #>x" unfolding r_coset_def by simp
lp15@68443
   242
      have Nyeq :"N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y = N #>y" unfolding r_coset_def by simp
lp15@68443
   243
lp15@68443
   244
      have "x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y =x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp
lp15@68443
   245
      hence "N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y
lp15@68443
   246
             = N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp
lp15@68443
   247
      also have "... = (N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x) <#>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub>
lp15@68443
   248
                       (N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y)"
lp15@68443
   249
        using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y]
lp15@68443
   250
             xHyH assms HcarrierNH by auto
lp15@68443
   251
      finally show "f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)"
lp15@68443
   252
        unfolding  FactGroup_def r_coset_def f_def  using Nxeq Nyeq  by auto
lp15@68443
   253
    qed
lp15@68443
   254
    hence "(\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>).
lp15@68443
   255
           f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))" by blast
lp15@68443
   256
    ultimately show  " f \<in> carrier (G\<lparr>carrier := H\<rparr>) \<rightarrow> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N) \<and>
lp15@68443
   257
    (\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>).
lp15@68443
   258
     f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))"
lp15@68443
   259
      by auto
lp15@68443
   260
  qed
lp15@68443
   261
  hence homomorphism : "group_hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N) f"
lp15@68443
   262
    unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)]
lp15@68443
   263
             normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto
lp15@68443
   264
  moreover have im_f :  "(f  ` carrier(G\<lparr>carrier:=H\<rparr>)) = carrier(G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   265
  proof
lp15@68443
   266
    show  "f ` carrier (G\<lparr>carrier := H\<rparr>) \<subseteq> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   267
      using op_hom unfolding hom_def using funcset_image by blast
lp15@68443
   268
  next
lp15@68443
   269
    show "carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N) \<subseteq> f ` carrier (G\<lparr>carrier := H\<rparr>)"
lp15@68443
   270
    proof
lp15@68443
   271
      fix x assume p : " x \<in> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   272
      hence "x \<in> \<Union>{y. \<exists>x\<in>carrier (G\<lparr>carrier := N <#> H\<rparr>). y = {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> x}}"
lp15@68443
   273
        unfolding FactGroup_def RCOSETS_def by auto
lp15@68443
   274
      hence hyp :"\<exists>y. \<exists>h\<in>carrier (G\<lparr>carrier := N <#> H\<rparr>). y = {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> h} \<and> x \<in> y"
lp15@68443
   275
        using Union_iff by blast
lp15@68443
   276
      from hyp obtain nh where nhNH:"nh \<in>carrier (G\<lparr>carrier := N <#> H\<rparr>)"
lp15@68443
   277
                          and "x \<in> {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> nh}"
lp15@68443
   278
        by blast
lp15@68443
   279
      hence K: "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N nh" by simp
lp15@68443
   280
      have "nh \<in> N <#> H" using nhNH by simp
lp15@68443
   281
      from this obtain n h where nN : "n \<in> N" and hH : " h \<in> H" and nhnh: "n \<otimes> h = nh"
lp15@68443
   282
        unfolding set_mult_def by blast
lp15@68443
   283
      have  "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N (n \<otimes> h)" using K nhnh by simp
lp15@68443
   284
      hence  "x = (#>) N (n \<otimes> h)" using K nhnh unfolding r_coset_def by auto
lp15@68443
   285
      also have "... = (N #> n) #>h"
lp15@68452
   286
        using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup
lp15@68443
   287
        by (metis subgroup.mem_carrier)
lp15@68443
   288
      finally have "x = (#>) N h"
lp15@68443
   289
        using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier)
lp15@68443
   290
      thus "x \<in> f ` carrier (G\<lparr>carrier := H\<rparr>)" using hH unfolding f_def by simp
lp15@68443
   291
    qed
lp15@68443
   292
  qed
lp15@68443
   293
  moreover have ker_f :"kernel (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N<#>H\<rparr> Mod N) f  = N\<inter>H"
lp15@68443
   294
    unfolding kernel_def f_def
lp15@68443
   295
    proof-
lp15@68443
   296
      have "{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = \<one>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub>} =
lp15@68443
   297
            {x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = N}" unfolding FactGroup_def by simp
lp15@68443
   298
      also have "... = {x \<in> carrier (G\<lparr>carrier := H\<rparr>). x \<in> N}"
lp15@68443
   299
        using coset_join1
lp15@68443
   300
        by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group
lp15@68443
   301
          normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group)
lp15@68443
   302
      also have "... =N \<inter> (carrier(G\<lparr>carrier := H\<rparr>))" by auto
lp15@68443
   303
      finally show "{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N#>x = \<one>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub>} = N \<inter> H"
lp15@68443
   304
        by simp
lp15@68443
   305
    qed
lp15@68443
   306
    ultimately have "(G\<lparr>carrier := H\<rparr> Mod N \<inter> H) \<cong> (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
lp15@68443
   307
      using group_hom.FactGroup_iso[OF homomorphism im_f] by auto
lp15@68443
   308
    hence "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H"
lp15@68443
   309
      by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup)
lp15@68443
   310
    thus "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
lp15@68443
   311
qed
lp15@68443
   312
lp15@68443
   313
lp15@68445
   314
theorem (in group) snd_iso_thme:
lp15@68443
   315
  assumes "subgroup H G"
lp15@68443
   316
    and "subgroup N G"
lp15@68443
   317
    and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
lp15@68443
   318
  shows "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))"
lp15@68443
   319
proof-
lp15@68443
   320
  have "G\<lparr>carrier := normalizer G N, carrier := H\<rparr>
lp15@68443
   321
       = G\<lparr>carrier := H\<rparr>"  by simp
lp15@68443
   322
  hence "G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
lp15@68443
   323
         G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
lp15@68443
   324
  moreover have "G\<lparr>carrier := normalizer G N,
lp15@68443
   325
                    carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> =
lp15@68443
   326
                G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr>" by simp
lp15@68443
   327
  hence "G\<lparr>carrier := normalizer G N,
lp15@68443
   328
          carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N =
lp15@68443
   329
          G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N" by auto
lp15@68443
   330
  hence "G\<lparr>carrier := normalizer G N,
lp15@68443
   331
          carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
lp15@68443
   332
         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
lp15@68443
   333
          (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
lp15@68466
   334
         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
lp15@68466
   335
    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
lp15@68452
   336
          subgroup.subset[OF assms(3)]
lp15@68452
   337
          subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
lp15@68443
   338
    by simp
lp15@68443
   339
  ultimately have "G\<lparr>carrier := normalizer G N,
lp15@68443
   340
                    carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
lp15@68443
   341
                  G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
lp15@68443
   342
                 (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
lp15@68443
   343
  moreover have "G\<lparr>carrier := normalizer G N,
lp15@68443
   344
                    carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
lp15@68443
   345
                  G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
lp15@68443
   346
    using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF
lp15@68452
   347
          subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
lp15@68443
   348
    by simp
lp15@68443
   349
  moreover have "H\<inter>N = N\<inter>H" using assms  by auto
lp15@68443
   350
  ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto
lp15@68443
   351
qed
lp15@68466
   352
lp15@68443
   353
lp15@68443
   354
corollary (in group) snd_iso_thme_recip :
lp15@68443
   355
  assumes "subgroup H G"
lp15@68443
   356
    and "subgroup N G"
lp15@68443
   357
    and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
lp15@68443
   358
  shows "(G\<lparr>carrier:= H<#>N\<rparr> Mod N)  \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))"
lp15@68452
   359
  by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset
lp15@68443
   360
      normalizer_imp_subgroup snd_iso_thme)
lp15@68443
   361
lp15@68443
   362
lp15@68443
   363
subsection\<open>The Zassenhaus Lemma\<close>
lp15@68443
   364
lp15@68443
   365
lp15@68445
   366
lemma (in group) distinc:
lp15@68466
   367
  assumes "subgroup  H G"
lp15@68466
   368
    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
lp15@68466
   369
    and  "subgroup K G"
lp15@68443
   370
    and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
lp15@68443
   371
  shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)"
lp15@68443
   372
proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
lp15@68443
   373
  show "subgroup (normalizer G (H1 <#> H \<inter> K1)) G"
lp15@68452
   374
    using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset
lp15@68443
   375
    by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair)
lp15@68443
   376
next
lp15@68443
   377
  show "H \<inter> K \<subseteq> normalizer G (H1 <#> H \<inter> K1)" unfolding normalizer_def stabilizer_def
lp15@68443
   378
  proof
lp15@68443
   379
    fix x assume xHK : "x \<in> H \<inter> K"
lp15@68443
   380
    hence xG : "{x} \<subseteq> carrier G" "{inv x} \<subseteq> carrier G"
lp15@68452
   381
      using subgroup.subset assms inv_closed xHK by auto
lp15@68443
   382
    have allG : "H \<subseteq> carrier G" "K \<subseteq> carrier G" "H1 \<subseteq> carrier G"  "K1 \<subseteq> carrier G"
lp15@68452
   383
      using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
lp15@68443
   384
    have HK1_normal: "H\<inter>K1 \<lhd> (G\<lparr>carrier :=  H \<inter> K\<rparr>)" using normal_inter[OF assms(3)assms(1)assms(4)]
lp15@68443
   385
      by (simp add : inf_commute)
lp15@68443
   386
    have "H \<inter> K \<subseteq> normalizer G (H \<inter> K1)"
lp15@68452
   387
      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
lp15@68443
   388
            assms(1)assms(3)]HK1_normal]] by auto
lp15@68443
   389
    hence "x <# (H \<inter> K1) #> inv x = (H \<inter> K1)"
lp15@68452
   390
      using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
lp15@68443
   391
                                                            normal_imp_subgroup[OF assms(4)]]]]
lp15@68443
   392
      unfolding normalizer_def stabilizer_def by auto
lp15@68443
   393
    moreover have "H \<subseteq>  normalizer G H1"
lp15@68452
   394
      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
lp15@68443
   395
    hence "x <# H1 #> inv x = H1"
lp15@68452
   396
      using xHK subgroup.subset[OF  incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
lp15@68443
   397
      unfolding normalizer_def stabilizer_def by auto
lp15@68443
   398
    ultimately have "H1 <#> H \<inter> K1 = (x <# H1 #> inv x) <#> (x <#  H \<inter> K1 #> inv x)" by auto
lp15@68443
   399
    also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#>  H \<inter> K1 <#> {inv x})"
lp15@68443
   400
      by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult)
lp15@68443
   401
    also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#>  (H \<inter> K1 <#> {inv x})"
lp15@68443
   402
      by (smt Int_lower1 allG xG set_mult_assoc subset_trans setmult_subset_G)
lp15@68443
   403
    also have "... = ({x} <#> H1 <#> {\<one>}) <#>  (H \<inter> K1 <#> {inv x})"
lp15@68443
   404
      using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G)
lp15@68443
   405
    also have "... =({x} <#> H1) <#>  (H \<inter> K1 <#> {inv x})"
lp15@68443
   406
      using coset_mult_one r_coset_eq_set_mult[of G H1 \<one>] set_mult_assoc[OF xG(1) allG(3)] allG
lp15@68443
   407
      by auto
lp15@68443
   408
    also have "... = {x} <#> (H1 <#> H \<inter> K1) <#> {inv x}"
lp15@68443
   409
      using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2)
lp15@68466
   410
    finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x"
lp15@68443
   411
      using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
lp15@68443
   412
    thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H1 <#> H \<inter> K1)
lp15@68443
   413
                                                                       = H1 <#> H \<inter> K1}"
lp15@68443
   414
      using xG allG setmult_subset_G[OF allG(3), where ?K = "H\<inter>K1"] xHK
lp15@68443
   415
      by auto
lp15@68443
   416
  qed
lp15@68443
   417
qed
lp15@68443
   418
lp15@68445
   419
lemma (in group) preliminary1:
lp15@68466
   420
  assumes "subgroup  H G"
lp15@68466
   421
    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
lp15@68466
   422
    and  "subgroup K G"
lp15@68443
   423
    and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
lp15@68443
   424
  shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)"
lp15@68443
   425
proof
lp15@68443
   426
  have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
lp15@68452
   427
    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
lp15@68443
   428
  show "H \<inter> K \<inter> (H1 <#> H \<inter> K1) \<subseteq> H1 \<inter> K <#> H \<inter> K1"
lp15@68443
   429
  proof
lp15@68443
   430
    fix x assume x_def : "x \<in> (H \<inter> K) \<inter> (H1 <#> (H \<inter> K1))"
lp15@68443
   431
    from x_def have x_incl : "x \<in> H" "x \<in> K" "x \<in> (H1 <#> (H \<inter> K1))" by auto
lp15@68443
   432
    then obtain h1 hk1 where h1hk1_def : "h1 \<in> H1" "hk1 \<in> H \<inter> K1" "h1 \<otimes> hk1 = x"
lp15@68443
   433
      using assms unfolding set_mult_def by blast
lp15@68452
   434
    hence "hk1 \<in> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
lp15@68443
   435
    hence "inv hk1 \<in> H \<inter> K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto
lp15@68443
   436
    moreover have "h1 \<otimes> hk1 \<in> H \<inter> K" using x_incl h1hk1_def by auto
lp15@68443
   437
    ultimately have "h1 \<otimes> hk1 \<otimes> inv hk1 \<in> H \<inter> K"
lp15@68443
   438
      using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto
lp15@68452
   439
    hence "h1 \<in> H \<inter> K" using  h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup
lp15@68443
   440
      by (metis Int_iff contra_subsetD inv_solve_right m_closed)
lp15@68443
   441
    hence "h1 \<in> H1 \<inter> H \<inter> K" using h1hk1_def by auto
lp15@68452
   442
    hence "h1 \<in> H1 \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
lp15@68443
   443
    hence "h1 \<otimes> hk1 \<in> (H1\<inter>K)<#>(H\<inter>K1)"
lp15@68443
   444
      using h1hk1_def unfolding set_mult_def by auto
lp15@68443
   445
    thus " x \<in> (H1\<inter>K)<#>(H\<inter>K1)" using h1hk1_def x_def by auto
lp15@68443
   446
  qed
lp15@68443
   447
  show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)"
lp15@68443
   448
  proof-
lp15@68452
   449
    have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
lp15@68443
   450
    moreover have "H \<inter> K1 \<subseteq> H \<inter> K"
lp15@68452
   451
      using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
lp15@68443
   452
    ultimately have "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K" unfolding set_mult_def
lp15@68443
   453
      using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast
lp15@68443
   454
    moreover have "H1 \<inter> K \<subseteq> H1" by auto
lp15@68443
   455
    hence "H1 \<inter> K <#> H \<inter> K1 \<subseteq> (H1 <#> H \<inter> K1)" unfolding set_mult_def by auto
lp15@68443
   456
    ultimately show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)" by auto
lp15@68443
   457
  qed
lp15@68443
   458
qed
lp15@68443
   459
lp15@68445
   460
lemma (in group) preliminary2:
lp15@68466
   461
  assumes "subgroup  H G"
lp15@68443
   462
    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
lp15@68466
   463
    and  "subgroup K G"
lp15@68443
   464
    and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
lp15@68443
   465
  shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>"
lp15@68443
   466
proof-
lp15@68443
   467
  have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
lp15@68452
   468
    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
lp15@68466
   469
  have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)"
lp15@68443
   470
    using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
lp15@68443
   471
          assms(1)]] assms by auto
lp15@68443
   472
  have "Group.group (G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>)"
lp15@68443
   473
    using  subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]].
lp15@68443
   474
  moreover have subH2 : "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := H\<rparr>)"
lp15@68443
   475
    using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF
lp15@68443
   476
           assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto
lp15@68443
   477
  hence "(H\<inter>K1) \<subseteq> (H\<inter>K)"
lp15@68452
   478
    using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme
lp15@68443
   479
    by (metis inf.mono  partial_object.simps(1) partial_object.update_convs(1) subset_refl)
lp15@68452
   480
  hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup.subset normal_imp_subgroup
lp15@68443
   481
    unfolding set_mult_def by blast
lp15@68443
   482
  hence "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := (H1<#>(H\<inter>K))\<rparr>)"
lp15@68443
   483
    using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1)
lp15@68452
   484
          subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast
lp15@68443
   485
  moreover have " (\<And> x. x\<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>) \<Longrightarrow>
lp15@68443
   486
        H1 <#> H\<inter>K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> x = x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1))"
lp15@68443
   487
  proof-
lp15@68443
   488
    fix x assume  "x \<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>)"
lp15@68443
   489
    hence x_def : "x \<in> H1 <#> H \<inter> K" by simp
lp15@68443
   490
    from this obtain h1 hk where h1hk_def :"h1 \<in> H1" "hk \<in> H \<inter> K" "h1 \<otimes> hk = x"
lp15@68443
   491
      unfolding set_mult_def by blast
lp15@68452
   492
    have xH : "x \<in> H" using subgroup.subset[OF subH1] using x_def by auto
lp15@68443
   493
    hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
lp15@68452
   494
      using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
lp15@68443
   495
    hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
lp15@68452
   496
      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
lp15@68443
   497
    also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
lp15@68452
   498
      using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
lp15@68452
   499
      by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
lp15@68443
   500
    also have "... = h1 <# (hk <# H1 <#> H\<inter>K1)"
lp15@68443
   501
      using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
lp15@68443
   502
    also have "... = h1 <# (hk <# H1 #> \<one> <#> H\<inter>K1 #> \<one>)"
lp15@68443
   503
      using coset_mult_one allG all_inclG l_coset_subset_G
lp15@68443
   504
      by (smt inf_le2 setmult_subset_G subset_trans)
lp15@68443
   505
    also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\<inter>K1 #> inv hk #> hk)"
lp15@68443
   506
      using all_inclG allG coset_mult_assoc l_coset_subset_G
lp15@68443
   507
      by (simp add: inf.coboundedI1 setmult_subset_G)
lp15@68443
   508
    finally  have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) =
lp15@68443
   509
                    h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\<inter>K1 #> inv hk) #> hk)"
lp15@68443
   510
      using rcos_assoc_lcos allG all_inclG
lp15@68443
   511
      by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans)
lp15@68443
   512
    moreover have "H \<subseteq>  normalizer G H1"
lp15@68452
   513
      using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
lp15@68443
   514
    hence "\<And>g. g \<in> H \<Longrightarrow>  g \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H1 = H1}"
lp15@68443
   515
      using all_inclG assms unfolding normalizer_def stabilizer_def by auto
lp15@68443
   516
    hence "\<And>g. g \<in> H \<Longrightarrow>  g <# H1 #> inv g = H1" using all_inclG by simp
lp15@68443
   517
    hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp
lp15@68443
   518
    moreover have "H\<inter>K \<subseteq> normalizer G (H\<inter>K1)"
lp15@68443
   519
      using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair
lp15@68452
   520
            subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
lp15@68443
   521
    hence "\<And>g. g\<in>H\<inter>K \<Longrightarrow> g\<in>{g\<in>carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H\<inter>K1) = H\<inter>K1}"
lp15@68443
   522
      using all_inclG assms unfolding normalizer_def stabilizer_def by auto
lp15@68443
   523
    hence "\<And>g. g \<in> H\<inter>K \<Longrightarrow>  g <# (H\<inter>K1) #> inv g = H\<inter>K1"
lp15@68452
   524
      using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
lp15@68443
   525
            assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto
lp15@68443
   526
    hence "(hk <# H\<inter>K1 #> inv hk) = H\<inter>K1" using h1hk_def by simp
lp15@68443
   527
    ultimately have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = h1 <#(H1 <#> (H \<inter> K1)#> hk)"
lp15@68443
   528
      by auto
lp15@68443
   529
    also have "... = h1 <# H1 <#> ((H \<inter> K1)#> hk)"
lp15@68443
   530
      using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H \<inter> K1)#> hk"] allG all_inclG
lp15@68443
   531
      by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc)
lp15@68443
   532
    also have "... = H1 <#> ((H \<inter> K1)#> hk)"
lp15@68443
   533
      using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def
lp15@68443
   534
      by auto
lp15@68443
   535
    finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
lp15@68443
   536
      by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
lp15@68443
   537
    have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
lp15@68452
   538
      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
lp15@68443
   539
    also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
lp15@68443
   540
      using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
lp15@68443
   541
    also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"
lp15@68443
   542
      using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
lp15@68443
   543
           assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
lp15@68443
   544
    also have "... = H \<inter> K1 <#> H1  #> hk"
lp15@68443
   545
      using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup]
lp15@68443
   546
            h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc)
lp15@68443
   547
    finally  have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =H1 <#> H \<inter> K1  #> hk"
lp15@68443
   548
      using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
lp15@68443
   549
           assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
lp15@68466
   550
    thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =
lp15@68443
   551
             x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)" using eq1 by simp
lp15@68443
   552
  qed
lp15@68443
   553
  ultimately show "H1 <#> H \<inter> K1 \<lhd> G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>"
lp15@68443
   554
    unfolding normal_def normal_axioms_def by auto
lp15@68443
   555
qed
lp15@68443
   556
lp15@68443
   557
lp15@68445
   558
proposition (in group)  Zassenhaus_1:
lp15@68466
   559
  assumes "subgroup  H G"
lp15@68466
   560
    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
lp15@68466
   561
    and  "subgroup K G"
lp15@68443
   562
    and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
lp15@68443
   563
  shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>H\<inter>K1)) \<cong> (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
lp15@68443
   564
proof-
lp15@68443
   565
  define N  and N1 where "N = (H\<inter>K)" and "N1 =H1<#>(H\<inter>K1)"
lp15@68443
   566
  have normal_N_N1 : "subgroup N (G\<lparr>carrier:=(normalizer G N1)\<rparr>)"
lp15@68443
   567
    by (simp add: N1_def N_def assms distinc normal_imp_subgroup)
lp15@68443
   568
  have Hp:"(G\<lparr>carrier:= N<#>N1\<rparr> Mod N1)  \<cong> (G\<lparr>carrier:= N\<rparr> Mod (N\<inter>N1))"
lp15@68443
   569
  by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub
lp15@68443
   570
        normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair)
lp15@68443
   571
  have H_simp: "N<#>N1 = H1<#> (H\<inter>K)"
lp15@68443
   572
  proof-
lp15@68443
   573
    have H1_incl_G : "H1 \<subseteq> carrier G"
lp15@68452
   574
      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
lp15@68443
   575
    have K1_incl_G :"K1 \<subseteq> carrier G"
lp15@68452
   576
      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
lp15@68443
   577
    have "N<#>N1=  (H\<inter>K)<#> (H1<#>(H\<inter>K1))" by (auto simp add: N_def N1_def)
lp15@68443
   578
    also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)"
lp15@68443
   579
      using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms
lp15@68452
   580
      by (simp add: inf.coboundedI2 subgroup.subset)
lp15@68466
   581
    also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)"
lp15@68443
   582
      using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
lp15@68443
   583
    also have "... =  H1 <#> ((H\<inter>K)<#>(H\<inter>K1))"
lp15@68443
   584
      using set_mult_assoc K1_incl_G H1_incl_G assms
lp15@68452
   585
      by (simp add: inf.coboundedI2 subgroup.subset)
lp15@68443
   586
    also have " ((H\<inter>K)<#>(H\<inter>K1)) = (H\<inter>K)"
lp15@68443
   587
    proof (intro set_mult_subgroup_idem[where ?H = "H\<inter>K" and ?N="H\<inter>K1",
lp15@68443
   588
             OF subgroups_Inter_pair[OF assms(1) assms(3)]])
lp15@68443
   589
      show "subgroup (H \<inter> K1) (G\<lparr>carrier := H \<inter> K\<rparr>)"
lp15@68443
   590
        using subgroup_incl[where ?I = "H\<inter>K1" and ?J = "H\<inter>K",OF subgroups_Inter_pair[OF assms(1)
lp15@68443
   591
              incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms
lp15@68443
   592
              normal_imp_subgroup by (metis inf_commute normal_inter)
lp15@68443
   593
    qed
lp15@68466
   594
    hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) =  H1 <#> ((H\<inter>K))"
lp15@68443
   595
      by simp
lp15@68443
   596
    thus "N <#> N1 = H1 <#> H \<inter> K"
lp15@68443
   597
      by (simp add: calculation)
lp15@68443
   598
  qed
lp15@68443
   599
lp15@68466
   600
  have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)"
lp15@68466
   601
    using preliminary1 assms N_def N1_def by simp
lp15@68443
   602
  thus  "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod N1)  \<cong> (G\<lparr>carrier:= N\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
lp15@68443
   603
    using H_simp Hp by auto
lp15@68443
   604
qed
lp15@68443
   605
lp15@68443
   606
lp15@68445
   607
theorem (in group) Zassenhaus:
lp15@68466
   608
  assumes "subgroup  H G"
lp15@68466
   609
    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
lp15@68466
   610
    and  "subgroup K G"
lp15@68443
   611
    and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
lp15@68466
   612
  shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1)))  \<cong>
lp15@68443
   613
         (G\<lparr>carrier:= K1 <#> (H\<inter>K)\<rparr> Mod (K1<#>(K\<inter>H1)))"
lp15@68443
   614
proof-
lp15@68443
   615
  define Gmod1 Gmod2 Gmod3 Gmod4
lp15@68443
   616
    where "Gmod1 = (G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1))) "
lp15@68443
   617
      and "Gmod2 = (G\<lparr>carrier:= K1 <#> (K\<inter>H)\<rparr> Mod (K1<#>(K\<inter>H1)))"
lp15@68443
   618
      and "Gmod3 = (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
lp15@68443
   619
      and "Gmod4 = (G\<lparr>carrier:= (K\<inter>H)\<rparr> Mod  ((K1\<inter>H)<#>(K\<inter>H1)))"
lp15@68443
   620
  have Hyp :  "Gmod1  \<cong> Gmod3" "Gmod2  \<cong>  Gmod4"
lp15@68443
   621
    using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto
lp15@68443
   622
  have Hp : "Gmod3 = G\<lparr>carrier:= (K\<inter>H)\<rparr> Mod ((K\<inter>H1)<#>(K1\<inter>H))"
lp15@68443
   623
    by (simp add: Gmod3_def inf_commute)
lp15@68443
   624
  have "(K\<inter>H1)<#>(K1\<inter>H) = (K1\<inter>H)<#>(K\<inter>H1)"
lp15@68443
   625
  proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]])
lp15@68443
   626
    show "K1 \<inter> H \<lhd> G\<lparr>carrier := H \<inter> K\<rparr>"
lp15@68443
   627
      using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute)
lp15@68443
   628
   next
lp15@68466
   629
    show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)"
lp15@68466
   630
      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter)
lp15@68443
   631
  qed
lp15@68443
   632
  hence  "Gmod3  = Gmod4" using Hp Gmod4_def by simp
lp15@68443
   633
  hence "Gmod1 \<cong> Gmod2"
lp15@68443
   634
    using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group
lp15@68443
   635
    by (metis assms Gmod1_def Gmod2_def preliminary2)
lp15@68443
   636
  thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute)
lp15@68443
   637
qed
lp15@68443
   638
lp15@68443
   639
end