more results about isomorphisms
authorpaulson
Wed May 19 11:30:18 2004 +0200 (2004-05-19)
changeset 1476128b5eb4a867f
parent 14760 a08e916f4946
child 14762 bd349ff7907a
more results about isomorphisms
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
     1.1 --- a/src/HOL/Algebra/Bij.thy	Wed May 19 11:29:47 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Wed May 19 11:30:18 2004 +0200
     1.3 @@ -133,7 +133,8 @@
     1.4    apply (blast intro: dest: id_in_auto)
     1.5   apply (simp del: restrict_apply
     1.6               add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
     1.7 -apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
     1.8 +apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
     1.9 +                      compose_Bij)
    1.10  done
    1.11  
    1.12  theorem AutoGroup: "group G ==> group (AutoGroup G)"
     2.1 --- a/src/HOL/Algebra/Coset.thy	Wed May 19 11:29:47 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Wed May 19 11:30:18 2004 +0200
     2.3 @@ -502,8 +502,7 @@
     2.4  lemma (in group) inv_FactGroup:
     2.5       "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
     2.6  apply (rule group.inv_equality [OF factorgroup_is_group]) 
     2.7 -apply (simp_all add: FactGroup_def setinv_closed 
     2.8 -    setrcos_inv_mult_group_eq group.intro [OF prems])
     2.9 +apply (simp_all add: FactGroup_def setinv_closed setrcos_inv_mult_group_eq)
    2.10  done
    2.11  
    2.12  text{*The coset map is a homomorphism from @{term G} to the quotient group
    2.13 @@ -511,7 +510,6 @@
    2.14  lemma (in group) r_coset_hom_Mod:
    2.15    assumes N: "N <| G"
    2.16    shows "(r_coset G N) \<in> hom G (G Mod N)"
    2.17 -by (simp add: FactGroup_def rcosets_def Pi_def hom_def
    2.18 -           rcos_sum group.intro prems) 
    2.19 +by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N) 
    2.20  
    2.21  end
     3.1 --- a/src/HOL/Algebra/Group.thy	Wed May 19 11:29:47 2004 +0200
     3.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 19 11:30:18 2004 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4  
     3.5  theory Group = FuncSet + Lattice:
     3.6  
     3.7 +
     3.8  section {* From Magmas to Groups *}
     3.9  
    3.10  text {*
    3.11 @@ -195,6 +196,10 @@
    3.12  locale group = monoid +
    3.13    assumes Units: "carrier G <= Units G"
    3.14  
    3.15 +
    3.16 +lemma (in group) is_group: "group G"
    3.17 +  by (rule group.intro [OF prems]) 
    3.18 +
    3.19  theorem groupI:
    3.20    includes struct G
    3.21    assumes m_closed [simp]:
    3.22 @@ -552,7 +557,7 @@
    3.23    apply (simp_all add: prems group_def group.l_inv)
    3.24    done
    3.25  
    3.26 -subsection {* Homomorphisms *}
    3.27 +subsection {* Isomorphisms *}
    3.28  
    3.29  constdefs (structure G and H)
    3.30    hom :: "_ => _ => ('a => 'b) set"
    3.31 @@ -561,8 +566,7 @@
    3.32        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
    3.33  
    3.34  lemma (in semigroup) hom:
    3.35 -  includes semigroup G
    3.36 -  shows "semigroup (| carrier = hom G G, mult = op o |)"
    3.37 +     "semigroup (| carrier = hom G G, mult = op o |)"
    3.38  proof (rule semigroup.intro)
    3.39    show "magma (| carrier = hom G G, mult = op o |)"
    3.40      by (rule magma.intro) (simp add: Pi_def hom_def)
    3.41 @@ -580,15 +584,43 @@
    3.42    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
    3.43    by (auto simp add: hom_def funcset_mem)
    3.44  
    3.45 -lemma compose_hom:
    3.46 -     "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
    3.47 -      ==> compose (carrier G) h h' \<in> hom G G"
    3.48 -apply (simp (no_asm_simp) add: hom_def)
    3.49 -apply (intro conjI)
    3.50 - apply (force simp add: funcset_compose hom_def)
    3.51 -apply (simp add: compose_def group.axioms hom_mult funcset_mem)
    3.52 +lemma (in group) hom_compose:
    3.53 +     "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
    3.54 +apply (auto simp add: hom_def funcset_compose) 
    3.55 +apply (simp add: compose_def funcset_mem)
    3.56  done
    3.57  
    3.58 +
    3.59 +subsection {* Isomorphisms *}
    3.60 +
    3.61 +constdefs (structure G and H)
    3.62 +  iso :: "_ => _ => ('a => 'b) set"
    3.63 +  "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    3.64 +
    3.65 +lemma iso_refl: "(%x. x) \<in> iso G G"
    3.66 +by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    3.67 +
    3.68 +lemma (in group) iso_sym:
    3.69 +     "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
    3.70 +apply (simp add: iso_def bij_betw_Inv) 
    3.71 +apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    3.72 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
    3.73 +apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f) 
    3.74 +done
    3.75 +
    3.76 +lemma (in group) iso_trans: 
    3.77 +     "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
    3.78 +by (auto simp add: iso_def hom_compose bij_betw_compose)
    3.79 +
    3.80 +lemma DirProdGroup_commute_iso:
    3.81 +  shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
    3.82 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    3.83 +
    3.84 +lemma DirProdGroup_assoc_iso:
    3.85 +  shows "(%(x,y,z). (x,(y,z))) \<in> iso (G \<times>\<^sub>g H \<times>\<^sub>g I) (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
    3.86 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    3.87 +
    3.88 +
    3.89  locale group_hom = group G + group H + var h +
    3.90    assumes homh: "h \<in> hom G H"
    3.91    notes hom_mult [simp] = hom_mult [OF homh]
    3.92 @@ -692,7 +724,7 @@
    3.93        x \<otimes> y = y \<otimes> x"
    3.94    shows "comm_group G"
    3.95    by (fast intro: comm_group.intro comm_semigroup_axioms.intro
    3.96 -    group.axioms prems)
    3.97 +                  is_group prems)
    3.98  
    3.99  lemma comm_groupI:
   3.100    includes struct G
   3.101 @@ -736,14 +768,10 @@
   3.102  lemma (in group) subgroup_inv_equality:
   3.103    "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
   3.104  apply (rule_tac inv_equality [THEN sym])
   3.105 -  apply (rule group.l_inv [OF subgroup_imp_group, simplified])
   3.106 -   apply assumption+
   3.107 - apply (rule subsetD [OF subgroup.subset])
   3.108 -  apply assumption+
   3.109 -apply (rule subsetD [OF subgroup.subset])
   3.110 - apply assumption
   3.111 -apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified])
   3.112 -  apply assumption+
   3.113 +  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
   3.114 + apply (rule subsetD [OF subgroup.subset], assumption+)
   3.115 +apply (rule subsetD [OF subgroup.subset], assumption)
   3.116 +apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
   3.117  done
   3.118  
   3.119  theorem (in group) subgroups_Inter: