src/HOL/Algebra/Coset.thy

 
 theory Coset
 imports Group
 begin
 
-section {*Cosets and Quotient Groups*}
+section \<open>Cosets and Quotient Groups\<close>
 
 definition
   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
   where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
 

 abbreviation
   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
   "H \<lhd> G \<equiv> normal H G"
 
 
-subsection {*Basic Properties of Cosets*}
+subsection \<open>Basic Properties of Cosets\<close>
 
 lemma (in group) coset_mult_assoc:
      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
       ==> (M #> g) #> h = M #> (g \<otimes> h)"
 by (force simp add: r_coset_def m_assoc)

                    subgroup.subset [THEN subsetD]
                    subgroup.m_closed solve_equation)
 
 lemma (in group) coset_join2:
      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
-  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
+  --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
 
 lemma (in monoid) r_coset_subset_G:
      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
 by (auto simp add: r_coset_def)

 
 lemma (in group) rcosetsI:
      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
 by (auto simp add: RCOSETS_def)
 
-text{*Really needed?*}
+text\<open>Really needed?\<close>
 lemma (in group) transpose_inv:
      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
       ==> (inv x) \<otimes> z = y"
 by (force simp add: m_assoc [symmetric])
 

 apply (simp add: r_coset_def)
 apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
                     subgroup.one_closed)
 done
 
-text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
+text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
 lemma (in group) repr_independenceD:
   assumes "subgroup H G"
   assumes ycarr: "y \<in> carrier G"
       and repr:  "H #> x = H #> y"
   shows "y \<in> H #> x"

    apply (rule ycarr)
    apply (rule is_subgroup)
   done
 qed
 
-text {* Elements of a right coset are in the carrier *}
+text \<open>Elements of a right coset are in the carrier\<close>
 lemma (in subgroup) elemrcos_carrier:
   assumes "group G"
   assumes acarr: "a \<in> carrier G"
     and a': "a' \<in> H #> a"
   shows "a' \<in> carrier G"

     from this and a
     show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
   qed
 qed
 
-text {* Step one for lemma @{text "rcos_module"} *}
+text \<open>Step one for lemma @{text "rcos_module"}\<close>
 lemma (in subgroup) rcos_module_imp:
   assumes "group G"
   assumes xcarr: "x \<in> carrier G"
       and x'cos: "x' \<in> H #> x"
   shows "(x' \<otimes> inv x) \<in> H"

       have "x' \<otimes> (inv x) = h" by simp
   from hH this
       show "x' \<otimes> (inv x) \<in> H" by simp
 qed
 
-text {* Step two for lemma @{text "rcos_module"} *}
+text \<open>Step two for lemma @{text "rcos_module"}\<close>
 lemma (in subgroup) rcos_module_rev:
   assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
       and xixH: "(x' \<otimes> inv x) \<in> H"
   shows "x' \<in> H #> x"

       show "x' \<in> H #> x"
       unfolding r_coset_def
       by fast
 qed
 
-text {* Module property of right cosets *}
+text \<open>Module property of right cosets\<close>
 lemma (in subgroup) rcos_module:
   assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
 proof -

     show "x' \<in> H #> x"
       by (intro rcos_module_rev[OF is_group])
   qed
 qed
 
-text {* Right cosets are subsets of the carrier. *} 
+text \<open>Right cosets are subsets of the carrier.\<close> 
 lemma (in subgroup) rcosets_carrier:
   assumes "group G"
   assumes XH: "X \<in> rcosets H"
   shows "X \<subseteq> carrier G"
 proof -

       show "X \<subseteq> carrier G"
       unfolding X
       by (rule r_coset_subset_G)
 qed
 
-text {* Multiplication of general subsets *}
+text \<open>Multiplication of general subsets\<close>
 lemma (in monoid) set_mult_closed:
   assumes Acarr: "A \<subseteq> carrier G"
       and Bcarr: "B \<subseteq> carrier G"
   shows "A <#> B \<subseteq> carrier G"
 apply rule apply (simp add: set_mult_def, clarsimp)

       unfolding l_coset_def
       by fast
 qed
 
 
-subsection {* Normal subgroups *}
+subsection \<open>Normal subgroups\<close>
 
 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   by (simp add: normal_def subgroup_def)
 
 lemma (in group) normalI: 

 apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 
 apply (simp add: ) 
 apply (blast intro: inv_op_closed1) 
 done
 
-text{*Alternative characterization of normal subgroups*}
+text\<open>Alternative characterization of normal subgroups\<close>
 lemma (in group) normal_inv_iff:
      "(N \<lhd> G) = 
       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
       (is "_ = ?rhs")
 proof

     qed
   qed
 qed
 
 
-subsection{*More Properties of Cosets*}
+subsection\<open>More Properties of Cosets\<close>
 
 lemma (in group) lcos_m_assoc:
      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
       ==> g <# (h <# M) = (g \<otimes> h) <# M"
 by (force simp add: l_coset_def m_assoc)

 apply (rule bexI [of _ "\<one>"])
 apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
 done
 
 
-subsubsection {* Set of Inverses of an @{text r_coset}. *}
+subsubsection \<open>Set of Inverses of an @{text r_coset}.\<close>
 
 lemma (in normal) rcos_inv:
   assumes x:     "x \<in> carrier G"
   shows "set_inv (H #> x) = H #> (inv x)" 
 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)

       by (simp add: h x m_assoc [symmetric] inv_mult_group)
   qed
 qed
 
 
-subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
+subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
 
 lemma (in group) setmult_rcos_assoc:
      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
 by (force simp add: r_coset_def set_mult_def m_assoc)

      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
 
 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
-  -- {* generalizes @{text subgroup_mult_id} *}
+  -- \<open>generalizes @{text subgroup_mult_id}\<close>
   by (auto simp add: RCOSETS_def subset
         setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
 
 
-subsubsection{*An Equivalence Relation*}
+subsubsection\<open>An Equivalence Relation\<close>
 
 definition
   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
   where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
 

       thus "inv x \<otimes> z \<in> H" by simp
     qed
   qed
 qed
 
-text{*Equivalence classes of @{text rcong} correspond to left cosets.
+text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
   Was there a mistake in the definitions? I'd have expected them to
-  correspond to right cosets.*}
+  correspond to right cosets.\<close>
 
 (* CB: This is correct, but subtle.
    We call H #> a the right coset of a relative to H.  According to
    Jacobson, this is what the majority of group theory literature does.
    He then defines the notion of congruence relation ~ over monoids as

   interpret group G by fact
   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
 qed
 
 
-subsubsection{*Two Distinct Right Cosets are Disjoint*}
+subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
 
 lemma (in group) rcos_equation:
   assumes "subgroup H G"
   assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"

     apply (blast intro: rcos_equation assms sym)
     done
 qed
 
 
-subsection {* Further lemmas for @{text "r_congruent"} *}
-
-text {* The relation is a congruence *}
+subsection \<open>Further lemmas for @{text "r_congruent"}\<close>
+
+text \<open>The relation is a congruence\<close>
 
 lemma (in normal) congruent_rcong:
   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
 proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
   fix a b c

   from carr and this and is_subgroup
      show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
 qed
 
 
-subsection {*Order of a Group and Lagrange's Theorem*}
+subsection \<open>Order of a Group and Lagrange's Theorem\<close>
 
 definition
   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   where "order S = card (carrier S)"
 

      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
 apply (auto simp add: RCOSETS_def)
 apply (simp add: r_coset_subset_G [THEN finite_subset])
 done
 
-text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
+text\<open>The next two lemmas support the proof of @{text card_cosets_equal}.\<close>
 lemma (in group) inj_on_f:
     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
 apply (rule inj_onI)
 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])

 apply (rule card_bij_eq)
      apply (rule inj_on_f, assumption+)
     apply (force simp add: m_assoc subsetD r_coset_def)
    apply (rule inj_on_g, assumption+)
   apply (force simp add: m_assoc subsetD r_coset_def)
- txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
+ txt\<open>The sets @{term "H #> a"} and @{term "H"} are finite.\<close>
  apply (simp add: r_coset_subset_G [THEN finite_subset])
 apply (blast intro: finite_subset)
 done
 
 lemma (in group) rcosets_subset_PowG:

  apply (simp add: card_cosets_equal subgroup.subset)
 apply (simp add: rcos_disjoint)
 done
 
 
-subsection {*Quotient Groups: Factorization of a Group*}
+subsection \<open>Quotient Groups: Factorization of a Group\<close>
 
 definition
   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
-    --{*Actually defined for groups rather than monoids*}
+    --\<open>Actually defined for groups rather than monoids\<close>
    where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
 
 lemma (in normal) setmult_closed:
      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
 by (auto simp add: rcos_sum RCOSETS_def)

      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
 apply (rule group.inv_equality [OF factorgroup_is_group]) 
 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
 done
 
-text{*The coset map is a homomorphism from @{term G} to the quotient group
-  @{term "G Mod H"}*}
+text\<open>The coset map is a homomorphism from @{term G} to the quotient group
+  @{term "G Mod H"}\<close>
 lemma (in normal) r_coset_hom_Mod:
   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
 
  
-subsection{*The First Isomorphism Theorem*}
-
-text{*The quotient by the kernel of a homomorphism is isomorphic to the 
-  range of that homomorphism.*}
+subsection\<open>The First Isomorphism Theorem\<close>
+
+text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
+  range of that homomorphism.\<close>
 
 definition
   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
-    --{*the kernel of a homomorphism*}
+    --\<open>the kernel of a homomorphism\<close>
   where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
 apply (rule subgroup.intro) 
 apply (auto simp add: kernel_def group.intro is_group) 
 done
 
-text{*The kernel of a homomorphism is a normal subgroup*}
+text\<open>The kernel of a homomorphism is a normal subgroup\<close>
 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
 apply (simp add: G.normal_inv_iff subgroup_kernel)
 apply (simp add: kernel_def)
 done
 

   thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
     by (simp add: all image_eq_UN FactGroup_nonempty X X')
 qed
 
 
-text{*Lemma for the following injectivity result*}
+text\<open>Lemma for the following injectivity result\<close>
 lemma (in group_hom) FactGroup_subset:
      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
 apply (clarsimp simp add: kernel_def r_coset_def image_def)
 apply (rename_tac y)  

   hence h: "h g = h g'"
     by (simp add: image_eq_UN all FactGroup_nonempty X X') 
   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
 qed
 
-text{*If the homomorphism @{term h} is onto @{term H}, then so is the
-homomorphism from the quotient group*}
+text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
+homomorphism from the quotient group\<close>
 lemma (in group_hom) FactGroup_onto:
   assumes h: "h ` carrier G = carrier H"
   shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
 proof
   show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"

       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
   qed
 qed
 
 
-text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
- quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
+text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
+ quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
 theorem (in group_hom) FactGroup_iso:
   "h ` carrier G = carrier H
    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
               FactGroup_onto)