SSL Coset.thy Interaktion und
PortierbarkeitIsabelle

(*  Title:      HOL/Algebra/Coset.thy
    Authors:    Florian Kammueller, L C Paulson, Stephan Hohe

With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
*)

theory Coset
imports Group
begin

section \<open>Cosets and Quotient Groups\<close>

definition
  r_coset    :: "[_, 'a set, 'a] \ 'a set" (infixl \#>\\ 60)
  where "H #>\<^bsub>G\<^esub> a = (\h\H. {h \\<^bsub>G\<^esub> a})"

definition
  l_coset    :: "[_, 'a, 'a set] \ 'a set" (infixl \<#\\ 60)
  where "a <#\<^bsub>G\<^esub> H = (\h\H. {a \\<^bsub>G\<^esub> h})"

definition
  RCOSETS  :: "[_, 'a set] \ ('a set)set"
    (\<open>(\<open>open_block notation=\<open>prefix rcosets\<close>\<close>rcosets\<index> _)\<close> [81] 80)
  where "rcosets\<^bsub>G\<^esub> H = (\a\carrier G. {H #>\<^bsub>G\<^esub> a})"

definition
  set_mult  :: "[_, 'a set ,'a set] \ 'a set" (infixl \<#>\\ 60)
  where "H <#>\<^bsub>G\<^esub> K = (\h\H. \k\K. {h \\<^bsub>G\<^esub> k})"

definition
  SET_INV :: "[_,'a set] \ 'a set"
    (\<open>(\<open>open_block notation=\<open>prefix set_inv\<close>\<close>set'_inv\<index> _)\<close> [81] 80)
  where "set_inv\<^bsub>G\<^esub> H = (\h\H. {inv\<^bsub>G\<^esub> h})"

locale normal = subgroup + group +
  assumes coset_eq: "(\x \ carrier G. H #> x = x <# H)"

abbreviation
  normal_rel :: "['a set, ('a, 'b) monoid_scheme] \ bool" (infixl \\\ 60) where
  "H \ G \ normal H G"

lemma (in comm_group) subgroup_imp_normal: "subgroup A G \ A \ G"
  by (simp add: normal_def normal_axioms_def l_coset_def r_coset_def m_comm subgroup.mem_carrier)

lemma l_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  fixes G (structure)
  shows "x <# H = {x} <#> H"
  unfolding l_coset_def set_mult_def by simp

lemma r_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  fixes G (structure)
  shows "H #> x = H <#> {x}"
  unfolding r_coset_def set_mult_def by simp

lemma (in subgroup) rcosets_non_empty: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "R \ rcosets H"
  shows "R \ {}"
proof -
  obtain g where "g \ carrier G" "R = H #> g"
    using assms unfolding RCOSETS_def by blast
  hence "\ \ g \ R"
    using one_closed unfolding r_coset_def by blast
  thus ?thesis by blast
qed

lemma (in group) diff_neutralizes: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "subgroup H G" "R \ rcosets H"
  shows "\r1 r2. \ r1 \ R; r2 \ R \ \ r1 \ (inv r2) \ H"
proof -
  fix r1 r2 assume r1: "r1 \ R" and r2: "r2 \ R"
  obtain g where g: "g \ carrier G" "R = H #> g"
    using assms unfolding RCOSETS_def by blast
  then obtain h1 h2 where h1: "h1 \ H" "r1 = h1 \ g"
                      and h2: "h2 \ H" "r2 = h2 \ g"
    using r1 r2 unfolding r_coset_def by blast
  hence "r1 \ (inv r2) = (h1 \ g) \ ((inv g) \ (inv h2))"
    using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
  also have " ... = (h1 \ (g \ inv g) \ inv h2)"
    using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
          monoid_axioms subgroup.mem_carrier
  proof -
    have "h1 \ carrier G"
      by (meson subgroup.mem_carrier assms(1) h1(1))
    moreover have "h2 \ carrier G"
      by (meson subgroup.mem_carrier assms(1) h2(1))
    ultimately show ?thesis
      using g(1) inv_closed m_assoc m_closed by presburger
  qed
  finally have "r1 \ inv r2 = h1 \ inv h2"
    using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
  thus "r1 \ inv r2 \ H" by (metis assms(1) h1(1) h2(1) subgroup_def)
qed

lemma mono_set_mult: "\ H \ H'; K \ K' \ \ H <#>\<^bsub>G\<^esub> K \ H' <#>\<^bsub>G\<^esub> K'" \<^marker>\contributor \Paulo Emílio de Vilhena\\
  unfolding set_mult_def by (simp add: UN_mono)

subsection \<open>Stable Operations for Subgroups\<close>

lemma set_mult_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "N <#>\<^bsub>(G \ carrier := H \)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
  unfolding set_mult_def by simp

lemma r_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "I #>\<^bsub>G \ carrier := H \\<^esub> h = I #>\<^bsub>G\<^esub> h"
  unfolding r_coset_def by simp

lemma l_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "h <#\<^bsub>G \ carrier := H \\<^esub> I = h <#\<^bsub>G\<^esub> I"
  unfolding l_coset_def by simp

subsection \<open>Basic Properties of set multiplication\<close>

lemma (in group) setmult_subset_G:
  assumes "H \ carrier G" "K \ carrier G"
  shows "H <#> K \ carrier G" using assms
  by (auto simp add: set_mult_def subsetD)

lemma (in monoid) set_mult_closed:
  assumes "H \ carrier G" "K \ carrier G"
  shows "H <#> K \ carrier G"
  using assms by (auto simp add: set_mult_def subsetD)

lemma (in group) set_mult_assoc: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  assumes "M \ carrier G" "H \ carrier G" "K \ carrier G"
  shows "(M <#> H) <#> K = M <#> (H <#> K)"
proof
  show "(M <#> H) <#> K \ M <#> (H <#> K)"
  proof
    fix x assume "x \ (M <#> H) <#> K"
    then obtain m h k where x: "m \ M" "h \ H" "k \ K" "x = (m \ h) \ k"
      unfolding set_mult_def by blast
    hence "x = m \ (h \ k)"
      using assms m_assoc by blast
    thus "x \ M <#> (H <#> K)"
      unfolding set_mult_def using x by blast
  qed
next
  show "M <#> (H <#> K) \ (M <#> H) <#> K"
  proof
    fix x assume "x \ M <#> (H <#> K)"
    then obtain m h k where x: "m \ M" "h \ H" "k \ K" "x = m \ (h \ k)"
      unfolding set_mult_def by blast
    hence "x = (m \ h) \ k"
      using assms m_assoc rev_subsetD by metis
    thus "x \ (M <#> H) <#> K"
      unfolding set_mult_def using x by blast
  qed
qed

subsection \<open>Basic Properties of Cosets\<close>

lemma (in group) coset_mult_assoc:
  assumes "M \ carrier G" "g \ carrier G" "h \ carrier G"
  shows "(M #> g) #> h = M #> (g \ h)"
  using assms by (force simp add: r_coset_def m_assoc)

lemma (in group) coset_assoc:
  assumes "x \ carrier G" "y \ carrier G" "H \ carrier G"
  shows "x <# (H #> y) = (x <# H) #> y"
  using set_mult_assoc[of "{x}" H "{y}"]
  by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms)

lemma (in group) coset_mult_one [simp]: "M \ carrier G ==> M #> \ = M"
by (force simp add: r_coset_def)

lemma (in group) coset_mult_inv1:
  assumes "M #> (x \ (inv y)) = M"
    and "x \ carrier G" "y \ carrier G" "M \ carrier G"
  shows "M #> x = M #> y" using assms
  by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self)

lemma (in group) coset_mult_inv2:
  assumes "M #> x = M #> y"
    and "x \ carrier G" "y \ carrier G" "M \ carrier G"
  shows "M #> (x \ (inv y)) = M " using assms
  by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)

lemma (in group) coset_join1:
  assumes "H #> x = H"
    and "x \ carrier G" "subgroup H G"
  shows "x \ H"
  using assms r_coset_def l_one subgroup.one_closed sym by fastforce

lemma (in group) solve_equation:
  assumes "subgroup H G" "x \ H" "y \ H"
  shows "\h \ H. y = h \ x"
proof -
  have "y = (y \ (inv x)) \ x" using assms
    by (simp add: m_assoc subgroup.mem_carrier)
  moreover have "y \ (inv x) \ H" using assms
    by (simp add: subgroup_def)
  ultimately show ?thesis by blast
qed

lemma (in group_hom) inj_on_one_iff:
   "inj_on h (carrier G) \ (\x. x \ carrier G \ h x = one H \ x = one G)"
using G.solve_equation G.subgroup_self by (force simp: inj_on_def)

lemma inj_on_one_iff':
   "\h \ hom G H; group G; group H\ \ inj_on h (carrier G) \ (\x. x \ carrier G \ h x = one H \ x = one G)"
  using group_hom.inj_on_one_iff group_hom.intro group_hom_axioms.intro by blast

lemma mon_iff_hom_one:
   "\group G; group H\ \ f \ mon G H \ f \ hom G H \ (\x. x \ carrier G \ f x = \\<^bsub>H\<^esub> \ x = \\<^bsub>G\<^esub>)"
  by (auto simp: mon_def inj_on_one_iff')

lemma (in group_hom) iso_iff: "h \ iso G H \ carrier H \ h ` carrier G \ (\x\carrier G. h x = \\<^bsub>H\<^esub> \ x = \)"
  by (auto simp: iso_def bij_betw_def inj_on_one_iff)

lemma (in group) repr_independence:
  assumes "y \ H #> x" "x \ carrier G" "subgroup H G"
  shows "H #> x = H #> y" using assms
by (auto simp add: r_coset_def m_assoc [symmetric]
                   subgroup.subset [THEN subsetD]
                   subgroup.m_closed solve_equation)

lemma (in group) coset_join2:
  assumes "x \ carrier G" "subgroup H G" "x \ H"
  shows "H #> x = H" using assms
  \<comment> \<open>Alternative proof is to put \<^term>\<open>x=\<one>\<close> in \<open>repr_independence\<close>.\<close>
by (force simp add: subgroup.m_closed r_coset_def solve_equation)

lemma (in group) coset_join3:
  assumes "x \ carrier G" "subgroup H G" "x \ H"
  shows "x <# H = H"
proof
  have "\h. h \ H \ x \ h \ H" using assms
    by (simp add: subgroup.m_closed)
  thus "x <# H \ H" unfolding l_coset_def by blast
next
  have "\h. h \ H \ x \ ((inv x) \ h) = h"
    by (metis (no_types, lifting) assms group.inv_closed group.inv_solve_left is_group
              monoid.m_closed monoid_axioms subgroup.mem_carrier)
  moreover have "\h. h \ H \ (inv x) \ h \ H"
    by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)
  ultimately show "H \ x <# H" unfolding l_coset_def by blast
qed

lemma (in monoid) r_coset_subset_G:
  "\ H \ carrier G; x \ carrier G \ \ H #> x \ carrier G"
by (auto simp add: r_coset_def)

lemma (in group) rcosI:
  "\ h \ H; H \ carrier G; x \ carrier G \ \ h \ x \ H #> x"
by (auto simp add: r_coset_def)

lemma (in group) rcosetsI:
     "\H \ carrier G; x \ carrier G\ \ H #> x \ rcosets H"
by (auto simp add: RCOSETS_def)

lemma (in group) rcos_self:
  "\ x \ carrier G; subgroup H G \ \ x \ H #> x"
  by (metis l_one rcosI subgroup_def)

text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
lemma (in group) repr_independenceD:
  assumes "subgroup H G" "y \ carrier G"
    and "H #> x = H #> y"
  shows "y \ H #> x"
  using assms by (simp add: rcos_self)

text \<open>Elements of a right coset are in the carrier\<close>
lemma (in subgroup) elemrcos_carrier:
  assumes "group G" "a \ carrier G"
    and "a' \ H #> a"
  shows "a' \ carrier G"
  by (meson assms group.is_monoid monoid.r_coset_subset_G subset subsetCE)

lemma (in subgroup) rcos_const:
  assumes "group G" "h \ H"
  shows "H #> h = H"
  using group.coset_join2[OF assms(1), of h H]
  by (simp add: assms(2) subgroup_axioms)

lemma (in subgroup) rcos_module_imp:
  assumes "group G" "x \ carrier G"
    and "x' \ H #> x"
  shows "(x' \ inv x) \ H"
proof -
  obtain h where h: "h \ H" "x' = h \ x"
    using assms(3) unfolding r_coset_def by blast
  hence "x' \ inv x = h"
    by (metis assms elemrcos_carrier group.inv_solve_right mem_carrier)
  thus ?thesis using h by blast
qed

lemma (in subgroup) rcos_module_rev:
  assumes "group G" "x \ carrier G" "x' \ carrier G"
    and "(x' \ inv x) \ H"
  shows "x' \ H #> x"
proof -
  obtain h where h: "h \ H" "x' \ inv x = h"
    using assms(4) unfolding r_coset_def by blast
  hence "x' = h \ x"
    by (metis assms group.inv_solve_right mem_carrier)
  thus ?thesis using h unfolding r_coset_def by blast
qed

text \<open>Module property of right cosets\<close>
lemma (in subgroup) rcos_module:
  assumes "group G" "x \ carrier G" "x' \ carrier G"
  shows "(x' \ H #> x) = (x' \ inv x \ H)"
  using rcos_module_rev rcos_module_imp assms by blast

text \<open>Right cosets are subsets of the carrier.\<close>
lemma (in subgroup) rcosets_carrier:
  assumes "group G" "X \ rcosets H"
  shows "X \ carrier G"
  using assms elemrcos_carrier singletonD
  subset_eq unfolding RCOSETS_def by force

text \<open>Multiplication of general subsets\<close>

lemma (in comm_group) mult_subgroups:
  assumes HG: "subgroup H G" and KG: "subgroup K G"
  shows "subgroup (H <#> K) G"
proof (rule subgroup.intro)
  show "H <#> K \ carrier G"
    by (simp add: setmult_subset_G assms subgroup.subset)
next
  have "\ \ \ \ H <#> K"
    unfolding set_mult_def using assms subgroup.one_closed by blast
  thus "\ \ H <#> K" by simp
next
  show "\x. x \ H <#> K \ inv x \ H <#> K"
  proof -
    fix x assume "x \ H <#> K"
    then obtain h k where hk: "h \ H" "k \ K" "x = h \ k"
      unfolding set_mult_def by blast
    hence "inv x = (inv k) \ (inv h)"
      by (meson inv_mult_group assms subgroup.mem_carrier)
    hence "inv x = (inv h) \ (inv k)"
      by (metis hk inv_mult assms subgroup.mem_carrier)
    thus "inv x \ H <#> K"
      unfolding set_mult_def using hk assms
      by (metis (no_types, lifting) UN_iff singletonI subgroup_def)
  qed
next
  show "\x y. x \ H <#> K \ y \ H <#> K \ x \ y \ H <#> K"
  proof -
    fix x y assume "x \ H <#> K" "y \ H <#> K"
    then obtain h1 k1 h2 k2 where h1k1: "h1 \ H" "k1 \ K" "x = h1 \ k1"
                              and h2k2: "h2 \ H" "k2 \ K" "y = h2 \ k2"
      unfolding set_mult_def by blast
    with KG HG have carr: "k1 \ carrier G" "h1 \ carrier G" "k2 \ carrier G" "h2 \ carrier G"
        by (meson subgroup.mem_carrier)+
    have "x \ y = (h1 \ k1) \ (h2 \ k2)"
      using h1k1 h2k2 by simp
    also have " ... = h1 \ (k1 \ h2) \ k2"
        by (simp add: carr comm_groupE(3) comm_group_axioms)
    also have " ... = h1 \ (h2 \ k1) \ k2"
      by (simp add: carr m_comm)
    finally have "x \ y = (h1 \ h2) \ (k1 \ k2)"
      by (simp add: carr comm_groupE(3) comm_group_axioms)
    thus "x \ y \ H <#> K" unfolding set_mult_def
      using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)]
            subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast
  qed
qed

lemma (in subgroup) lcos_module_rev:
  assumes "group G" "x \ carrier G" "x' \ carrier G"
    and "(inv x \ x') \ H"
  shows "x' \ x <# H"
proof -
  obtain h where h: "h \ H" "inv x \ x' = h"
    using assms(4) unfolding l_coset_def by blast
  hence "x' = x \ h"
    by (metis assms group.inv_solve_left mem_carrier)
  thus ?thesis using h unfolding l_coset_def by blast
qed

subsection \<open>Normal subgroups\<close>

lemma normal_imp_subgroup: "H \ G \ subgroup H G"
  by (rule normal.axioms(1))

lemma (in group) normalI:
  "subgroup H G \ (\x \ carrier G. H #> x = x <# H) \ H \ G"
  by (simp add: normal_def normal_axioms_def is_group)

lemma (in normal) inv_op_closed1:
  assumes "x \ carrier G" and "h \ H"
  shows "(inv x) \ h \ x \ H"
proof -
  have "h \ x \ x <# H"
    using assms coset_eq assms(1) unfolding r_coset_def by blast
  then obtain h' where "h' \<in> H" "h \<otimes> x = x \<otimes> h'"
    unfolding l_coset_def by blast
  thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier)
qed

lemma (in normal) inv_op_closed2:
  assumes "x \ carrier G" and "h \ H"
  shows "x \ h \ (inv x) \ H"
  using assms inv_op_closed1 by (metis inv_closed inv_inv)

lemma (in comm_group) normal_iff_subgroup:
  "N \ G \ subgroup N G"
proof
  assume "subgroup N G"
  then show "N \ G"
    by unfold_locales (auto simp: subgroupE subgroup.one_closed l_coset_def r_coset_def m_comm subgroup.mem_carrier)
qed (simp add: normal_imp_subgroup)

text\<open>Alternative characterization of normal subgroups\<close>
lemma (in group) normal_inv_iff:
     "(N \ G) =
      (subgroup N G \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
      (is "_ = ?rhs")
proof
  assume N: "N \ G"
  show ?rhs
    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
next
  assume ?rhs
  hence sg: "subgroup N G"
    and closed: "\x. x\carrier G \ \h\N. x \ h \ inv x \ N" by auto
  hence sb: "N \ carrier G" by (simp add: subgroup.subset)
  show "N \ G"
  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
    fix x
    assume x: "x \ carrier G"
    show "(\h\N. {h \ x}) = (\h\N. {x \ h})"
    proof
      show "(\h\N. {h \ x}) \ (\h\N. {x \ h})"
      proof clarify
        fix n
        assume n: "n \ N"
        show "n \ x \ (\h\N. {x \ h})"
        proof
          from closed [of "inv x"]
          show "inv x \ n \ x \ N" by (simp add: x n)
          show "n \ x \ {x \ (inv x \ n \ x)}"
            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
        qed
      qed
    next
      show "(\h\N. {x \ h}) \ (\h\N. {h \ x})"
      proof clarify
        fix n
        assume n: "n \ N"
        show "x \ n \ (\h\N. {h \ x})"
        proof
          show "x \ n \ inv x \ N" by (simp add: x n closed)
          show "x \ n \ {x \ n \ inv x \ x}"
            by (simp add: x n m_assoc sb [THEN subsetD])
        qed
      qed
    qed
  qed
qed

corollary (in group) normal_invI:
  assumes "subgroup N G" and "\x h. \ x \ carrier G; h \ N \ \ x \ h \ inv x \ N"
  shows "N \ G"
  using assms normal_inv_iff by blast

corollary (in group) normal_invE:
  assumes "N \ G"
  shows "subgroup N G" and "\x h. \ x \ carrier G; h \ N \ \ x \ h \ inv x \ N"
  using assms normal_inv_iff apply blast
  by (simp add: assms normal.inv_op_closed2)

lemma (in group) one_is_normal: "{\} \ G"
  using normal_invI triv_subgroup by force

text \<open>The intersection of two normal subgroups is, again, a normal subgroup.\<close>
lemma (in group) normal_subgroup_intersect:
  assumes "M \ G" and "N \ G" shows "M \ N \ G"
  using  assms normal_inv_iff subgroups_Inter_pair by force

text \<open>Being a normal subgroup is preserved by surjective homomorphisms.\<close>

lemma (in normal) surj_hom_normal_subgroup:
  assumes \<phi>: "group_hom G F \<phi>"
  assumes \<phi>surj: "\<phi> ` (carrier G) = carrier F"
  shows "(\ ` H) \ F"
proof (rule group.normalI)
  show "group F"
    using \<phi> group_hom.axioms(2) by blast
next
  show "subgroup (\ ` H) F"
    using \<phi> group_hom.subgroup_img_is_subgroup subgroup_axioms by blast
next
  show "\x\carrier F. \ ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \ ` H"
  proof
    fix f
    assume f: "f \ carrier F"
    with \<phi>surj obtain g where g: "g \<in> carrier G" "f = \<phi> g" by auto
    hence "\ ` H #>\<^bsub>F\<^esub> f = \ ` H #>\<^bsub>F\<^esub> \ g" by simp
    also have "... = (\x. (\ x) \\<^bsub>F\<^esub> (\ g)) ` H"
      unfolding r_coset_def image_def by auto
    also have "... = (\x. \ (x \ g)) ` H"
      using subset g \<phi> group_hom.hom_mult unfolding image_def by fastforce
    also have "... = \ ` (H #> g)"
      using \<phi> unfolding r_coset_def by auto
    also have "... = \ ` (g <# H)"
      by (metis coset_eq g(1))
    also have "... = (\x. \ (g \ x)) ` H"
      using \<phi> unfolding l_coset_def by auto
    also have "... = (\x. (\ g) \\<^bsub>F\<^esub> (\ x)) ` H"
      using subset g \<phi> group_hom.hom_mult by fastforce
    also have "... = \ g <#\<^bsub>F\<^esub> \ ` H"
      unfolding l_coset_def image_def by auto
    also have "... = f <#\<^bsub>F\<^esub> \ ` H"
      using g by simp
    finally show "\ ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \ ` H".
  qed
qed

text \<open>Being a normal subgroup is preserved by group isomorphisms.\<close>
lemma iso_normal_subgroup:
  assumes \<phi>: "\<phi> \<in> iso G F" "group G" "group F" "H \<lhd> G"
  shows "(\ ` H) \ F"
  by (meson assms Group.iso_iff group_hom_axioms_def group_hom_def normal.surj_hom_normal_subgroup)

text \<open>The set product of two normal subgroups is a normal subgroup.\<close>
lemma (in group) setmult_lcos_assoc:
  "\H \ carrier G; K \ carrier G; x \ carrier G\
      \<Longrightarrow> (x <# H) <#> K = x <# (H <#> K)"
  by (force simp add: l_coset_def set_mult_def m_assoc)

subsection\<open>More Properties of Left Cosets\<close>

lemma (in group) l_repr_independence:
  assumes "y \ x <# H" "x \ carrier G" and HG: "subgroup H G"
  shows "x <# H = y <# H"
proof -
  obtain h' where h': "h' \ H" "y = x \ h'"
    using assms(1) unfolding l_coset_def by blast
  hence "x \ h = y \ ((inv h') \ h)" if "h \ H" for h
  proof -
    have "h' \ carrier G"
      by (meson HG h'(1) subgroup.mem_carrier)
    moreover have "h \ carrier G"
      by (meson HG subgroup.mem_carrier that)
    ultimately show ?thesis
      by (metis assms(2) h'(2) inv_closed inv_solve_right m_assoc m_closed)
  qed
  hence "\xh. xh \ x <# H \ xh \ y <# H"
    unfolding l_coset_def by (metis (no_types, lifting) UN_iff HG h'(1) subgroup_def)
  moreover have "\h. h \ H \ y \ h = x \ (h' \ h)"
    using h' by (meson assms(2) HG m_assoc subgroup.mem_carrier)
  hence "\yh. yh \ y <# H \ yh \ x <# H"
    unfolding l_coset_def using subgroup.m_closed[OF HG h'(1)] by blast
  ultimately show ?thesis by blast
qed

lemma (in group) lcos_m_assoc:
  "\ M \ carrier G; g \ carrier G; h \ carrier G \ \ g <# (h <# M) = (g \ h) <# M"
by (force simp add: l_coset_def m_assoc)

lemma (in group) lcos_mult_one: "M \ carrier G \ \ <# M = M"
by (force simp add: l_coset_def)

lemma (in group) l_coset_subset_G:
  "\ H \ carrier G; x \ carrier G \ \ x <# H \ carrier G"
by (auto simp add: l_coset_def subsetD)

lemma (in group) l_coset_carrier:
  "\ y \ x <# H; x \ carrier G; subgroup H G \ \ y \ carrier G"
  by (auto simp add: l_coset_def m_assoc  subgroup.subset [THEN subsetD] subgroup.m_closed)

lemma (in group) l_coset_swap:
  assumes "y \ x <# H" "x \ carrier G" "subgroup H G"
  shows "x \ y <# H"
  using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
  unfolding l_coset_def by fastforce

lemma (in group) subgroup_mult_id:
  assumes "subgroup H G"
  shows "H <#> H = H"
proof
  show "H <#> H \ H"
    unfolding set_mult_def using subgroup.m_closed[OF assms] by (simp add: UN_subset_iff)
  show "H \ H <#> H"
  proof
    fix x assume x: "x \ H" thus "x \ H <#> H" unfolding set_mult_def
      using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms]
      using assms subgroup.mem_carrier by force
  qed
qed

subsubsection \<open>Set of Inverses of an \<open>r_coset\<close>.\<close>

lemma (in normal) rcos_inv:
  assumes x:     "x \ carrier G"
  shows "set_inv (H #> x) = H #> (inv x)"
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
  fix h
  assume h: "h \ H"
  show "inv x \ inv h \ (\j\H. {j \ inv x})"
  proof
    show "inv x \ inv h \ x \ H"
      by (simp add: inv_op_closed1 h x)
    show "inv x \ inv h \ {inv x \ inv h \ x \ inv x}"
      by (simp add: h x m_assoc)
  qed
  show "h \ inv x \ (\j\H. {inv x \ inv j})"
  proof
    show "x \ inv h \ inv x \ H"
      by (simp add: inv_op_closed2 h x)
    show "h \ inv x \ {inv x \ inv (x \ inv h \ inv x)}"
      by (simp add: h x m_assoc [symmetric] inv_mult_group)
  qed
qed

subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>

lemma (in group) setmult_rcos_assoc:
  "\H \ carrier G; K \ carrier G; x \ carrier G\ \
    H <#> (K #> x) = (H <#> K) #> x"
  using set_mult_assoc[of H K "{x}"] by (simp add: r_coset_eq_set_mult)

lemma (in group) rcos_assoc_lcos:
  "\H \ carrier G; K \ carrier G; x \ carrier G\ \
   (H #> x) <#> K = H <#> (x <# K)"
  using set_mult_assoc[of H "{x}" K]
  by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)

lemma (in normal) rcos_mult_step1:
  "\x \ carrier G; y \ carrier G\ \
   (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
  by (simp add: setmult_rcos_assoc r_coset_subset_G
                subset l_coset_subset_G rcos_assoc_lcos)

lemma (in normal) rcos_mult_step2:
     "\x \ carrier G; y \ carrier G\
      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
by (insert coset_eq, simp add: normal_def)

lemma (in normal) rcos_mult_step3:
     "\x \ carrier G; y \ carrier G\
      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
by (simp add: setmult_rcos_assoc coset_mult_assoc
              subgroup_mult_id normal.axioms subset normal_axioms)

lemma (in normal) rcos_sum:
     "\x \ carrier G; y \ carrier G\
      \<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 \ rcosets H \ H <#> M = M"
  \<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
  by (auto simp add: RCOSETS_def subset
        setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)

subsubsection\<open>An Equivalence Relation\<close>

definition
  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \ ('a*'a)set"
    (\<open>(\<open>open_block notation=\<open>prefix rcong\<close>\<close>rcong\<index> _)\<close>)
  where "rcong\<^bsub>G\<^esub> H = {(x,y). x \ carrier G \ y \ carrier G \ inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ H}"

lemma (in subgroup) equiv_rcong:
   assumes "group G"
   shows "equiv (carrier G) (rcong H)"
proof -
  interpret group G by fact
  show ?thesis
  proof (intro equivI)
    show "rcong H \ carrier G \ carrier G"
      by (auto simp add: r_congruent_def)
    thus "refl_on (carrier G) (rcong H)"
      by (auto simp add: r_congruent_def refl_on_def)
  next
    show "sym (rcong H)"
    proof (simp add: r_congruent_def sym_def, clarify)
      fix x y
      assume [simp]: "x \ carrier G" "y \ carrier G"
         and "inv x \ y \ H"
      hence "inv (inv x \ y) \ H" by simp
      thus "inv y \ x \ H" by (simp add: inv_mult_group)
    qed
  next
    show "trans (rcong H)"
    proof (simp add: r_congruent_def trans_def, clarify)
      fix x y z
      assume [simp]: "x \ carrier G" "y \ carrier G" "z \ carrier G"
         and "inv x \ y \ H" and "inv y \ z \ H"
      hence "(inv x \ y) \ (inv y \ z) \ H" by simp
      hence "inv x \ (y \ inv y) \ z \ H"
        by (simp add: m_assoc del: r_inv Units_r_inv)
      thus "inv x \ z \ H" by simp
    qed
  qed
qed

text\<open>Equivalence classes of \<open>rcong\<close> correspond to left cosets.
  Was there a mistake in the definitions? I'd have expected them to
  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
   equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
   Our notion of right congruence induced by K: rcong K appears only in
   the context where K is a normal subgroup.  Jacobson doesn't name it.
   But in this context left and right cosets are identical.
*)

lemma (in subgroup) l_coset_eq_rcong:
  assumes "group G"
  assumes a: "a \ carrier G"
  shows "a <# H = (rcong H) `` {a}"
proof -
  interpret group G by fact
  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
qed

subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>

lemma (in group) rcos_equation:
  assumes "subgroup H G"
  assumes p: "ha \ a = h \ b" "a \ carrier G" "b \ carrier G" "h \ H" "ha \ H" "hb \ H"
  shows "hb \ a \ (\h\H. {h \ b})"
proof -
  interpret subgroup H G by fact
  from p show ?thesis
    by (rule_tac UN_I [of "hb \ ((inv ha) \ h)"]) (auto simp: inv_solve_left m_assoc)
qed

lemma (in group) rcos_disjoint:
  assumes "subgroup H G"
  shows "pairwise disjnt (rcosets H)"
proof -
  interpret subgroup H G by fact
  show ?thesis
    unfolding RCOSETS_def r_coset_def pairwise_def disjnt_def
    by (blast intro: rcos_equation assms sym)
qed

subsection \<open>Further lemmas for \<open>r_congruent\<close>\<close>

text \<open>The relation is a congruence\<close>

lemma (in normal) congruent_rcong:
  shows "congruent2 (rcong H) (rcong H) (\a b. a \ b <# H)"
proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
  fix a b c
  assume abrcong: "(a, b) \ rcong H"
    and ccarr: "c \ carrier G"

  from abrcong
      have acarr: "a \ carrier G"
        and bcarr: "b \ carrier G"
        and abH: "inv a \ b \ H"
      unfolding r_congruent_def
      by fast+

  note carr = acarr bcarr ccarr

  from ccarr and abH
      have "inv c \ (inv a \ b) \ c \ H" by (rule inv_op_closed1)
  moreover
      from carr and inv_closed
      have "inv c \ (inv a \ b) \ c = (inv c \ inv a) \ (b \ c)"
      by (force cong: m_assoc)
  moreover
      from carr and inv_closed
      have "\ = (inv (a \ c)) \ (b \ c)"
      by (simp add: inv_mult_group)
  ultimately
      have "(inv (a \ c)) \ (b \ c) \ H" by simp
  from carr and this
     have "(b \ c) \ (a \ c) <# H"
     by (simp add: lcos_module_rev[OF is_group])
  from carr and this and is_subgroup
     show "(a \ c) <# H = (b \ c) <# H" by (intro l_repr_independence, simp+)
next
  fix a b c
  assume abrcong: "(a, b) \ rcong H"
    and ccarr: "c \ carrier G"

  from ccarr have "c \ Units G" by simp
  hence cinvc_one: "inv c \ c = \" by (rule Units_l_inv)

  from abrcong
      have acarr: "a \ carrier G"
       and bcarr: "b \ carrier G"
       and abH: "inv a \ b \ H"
      by (unfold r_congruent_def, fast+)

  note carr = acarr bcarr ccarr

  from carr and inv_closed
     have "inv a \ b = inv a \ (\ \ b)" by simp
  also from carr and inv_closed
      have "\ = inv a \ (inv c \ c) \ b" by simp
  also from carr and inv_closed
      have "\ = (inv a \ inv c) \ (c \ b)" by (force cong: m_assoc)
  also from carr and inv_closed
      have "\ = inv (c \ a) \ (c \ b)" by (simp add: inv_mult_group)
  finally
      have "inv a \ b = inv (c \ a) \ (c \ b)" .
  from abH and this
      have "inv (c \ a) \ (c \ b) \ H" by simp

  from carr and this
     have "(c \ b) \ (c \ a) <# H"
     by (simp add: lcos_module_rev[OF is_group])
  from carr and this and is_subgroup
     show "(c \ a) <# H = (c \ b) <# H" by (intro l_repr_independence, simp+)
qed

subsection \<open>Order of a Group and Lagrange's Theorem\<close>

definition
  order :: "('a, 'b) monoid_scheme \ nat"
  where "order S = card (carrier S)"

lemma iso_same_order:
  assumes "\ \ iso G H"
  shows "order G = order H"
  by (metis assms is_isoI iso_same_card order_def order_def)

lemma (in monoid) order_gt_0_iff_finite: "0 < order G \ finite (carrier G)"
  by(auto simp add: order_def card_gt_0_iff)

lemma (in group) order_one_triv_iff:
  shows "(order G = 1) = (carrier G = {\})"
  by (metis One_nat_def card.empty card_Suc_eq empty_iff one_closed order_def singleton_iff)

lemma (in group) rcosets_part_G:
  assumes "subgroup H G"
  shows "\(rcosets H) = carrier G"
proof -
  interpret subgroup H G by fact
  show ?thesis
    unfolding RCOSETS_def r_coset_def by auto
qed

lemma (in group) cosets_finite:
     "\c \ rcosets H; H \ carrier G; finite (carrier G)\ \ finite c"
  unfolding RCOSETS_def
  by (auto simp add: r_coset_subset_G [THEN finite_subset])

text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
lemma (in group) inj_on_f:
  assumes "H \ carrier G" and a: "a \ carrier G"
  shows "inj_on (\y. y \ inv a) (H #> a)"
proof
  fix x y
  assume "x \ H #> a" "y \ H #> a" and xy: "x \ inv a = y \ inv a"
  then have "x \ carrier G" "y \ carrier G"
    using assms r_coset_subset_G by blast+
  with xy a show "x = y"
    by auto
qed

lemma (in group) inj_on_g:
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. y \ a) H"
by (force simp add: inj_on_def subsetD)

(* ************************************************************************** *)

lemma (in group) card_cosets_equal:
  assumes "R \ rcosets H" "H \ carrier G"
  shows "\f. bij_betw f H R"
proof -
  obtain g where g: "g \ carrier G" "R = H #> g"
    using assms(1) unfolding RCOSETS_def by blast

  let ?f = "\h. h \ g"
  have "\r. r \ R \ \h \ H. ?f h = r"
  proof -
    fix r assume "r \ R"
    then obtain h where "h \ H" "r = h \ g"
      using g unfolding r_coset_def by blast
    thus "\h \ H. ?f h = r" by blast
  qed
  hence "R \ ?f ` H" by blast
  moreover have "?f ` H \ R"
    using g unfolding r_coset_def by blast
  ultimately show ?thesis using inj_on_g unfolding bij_betw_def
    using assms(2) g(1) by auto
qed

corollary (in group) card_rcosets_equal:
  assumes "R \ rcosets H" "H \ carrier G"
  shows "card H = card R"
  using card_cosets_equal assms bij_betw_same_card by blast

corollary (in group) rcosets_finite:
  assumes "R \ rcosets H" "H \ carrier G" "finite H"
  shows "finite R"
  using card_cosets_equal assms bij_betw_finite is_group by blast

(* ************************************************************************** *)

lemma (in group) rcosets_subset_PowG:
     "subgroup H G \ rcosets H \ Pow(carrier G)"
  using rcosets_part_G by auto

proposition (in group) lagrange_finite:
  assumes "finite(carrier G)" and HG: "subgroup H G"
  shows "card(rcosets H) * card(H) = order(G)"
proof -
  have "card H * card (rcosets H) = card (\(rcosets H))"
  proof (rule card_partition)
    show "\c1 c2. \c1 \ rcosets H; c2 \ rcosets H; c1 \ c2\ \ c1 \ c2 = {}"
      using HG rcos_disjoint by (auto simp: pairwise_def disjnt_def)
  qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
  then show ?thesis
    by (simp add: HG mult.commute order_def rcosets_part_G)
qed

theorem (in group) lagrange:
  assumes "subgroup H G"
  shows "card (rcosets H) * card H = order G"
proof (cases "finite (carrier G)")
  case True thus ?thesis using lagrange_finite assms by simp
next
  case False
  thus ?thesis
  proof (cases "finite H")
    case False thus ?thesis using \<open>infinite (carrier G)\<close>  by (simp add: order_def)
  next
    case True
    have "infinite (rcosets H)"
    proof
      assume "finite (rcosets H)"
      hence finite_rcos: "finite (rcosets H)" by simp
      hence "card (\(rcosets H)) = (\R\(rcosets H). card R)"
        using card_Union_disjoint[of "rcosets H"] \<open>finite H\<close> rcos_disjoint[OF assms(1)]
              rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
      hence "order G = (\R\(rcosets H). card R)"
        by (simp add: assms order_def rcosets_part_G)
      hence "order G = (\R\(rcosets H). card H)"
        using card_rcosets_equal by (simp add: assms subgroup.subset)
      hence "order G = (card H) * (card (rcosets H))" by simp
      hence "order G \ 0" using finite_rcos \finite H\ assms ex_in_conv
                                rcosets_part_G subgroup.one_closed by fastforce
      thus False using \<open>infinite (carrier G)\<close> order_gt_0_iff_finite by blast
    qed
    thus ?thesis using \<open>infinite (carrier G)\<close> by (simp add: order_def)
  qed
qed

text \<open>The cardinality of the right cosets of the trivial subgroup is the cardinality of the group itself:\<close>
corollary (in group) card_rcosets_triv:
  assumes "finite (carrier G)"
  shows "card (rcosets {\}) = order G"
  using lagrange triv_subgroup by fastforce

subsection \<open>Quotient Groups: Factorization of a Group\<close>

definition
  FactGroup :: "[('a,'b) monoid_scheme, 'a set] \ ('a set) monoid" (infixl \Mod\ 65)
    \<comment> \<open>Actually defined for groups rather than monoids\<close>
   where "FactGroup G H = \carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\"

lemma (in normal) setmult_closed:
     "\K1 \ rcosets H; K2 \ rcosets H\ \ K1 <#> K2 \ rcosets H"
by (auto simp add: rcos_sum RCOSETS_def)

lemma (in normal) setinv_closed:
     "K \ rcosets H \ set_inv K \ rcosets H"
by (auto simp add: rcos_inv RCOSETS_def)

lemma (in normal) rcosets_assoc:
     "\M1 \ rcosets H; M2 \ rcosets H; M3 \ rcosets H\
      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
  by (simp add: group.set_mult_assoc is_group rcosets_carrier)

lemma (in subgroup) subgroup_in_rcosets:
  assumes "group G"
  shows "H \ rcosets H"
proof -
  interpret group G by fact
  from _ subgroup_axioms have "H #> \ = H"
    by (rule coset_join2) auto
  then show ?thesis
    by (auto simp add: RCOSETS_def)
qed

lemma (in normal) rcosets_inv_mult_group_eq:
     "M \ rcosets H \ set_inv M <#> M = H"
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)

theorem (in normal) factorgroup_is_group: "group (G Mod H)"
proof -
  have "\x. x \ rcosets H \ \y\rcosets H. y <#> x = H"
    using rcosets_inv_mult_group_eq setinv_closed by blast
  then show ?thesis
    unfolding FactGroup_def
    by (intro groupI)
      (auto simp: setmult_closed subgroup_in_rcosets rcosets_assoc rcosets_mult_eq)
qed

lemma carrier_FactGroup: "carrier(G Mod N) = (\x. r_coset G N x) ` carrier G"
  by (auto simp: FactGroup_def RCOSETS_def)

lemma one_FactGroup [simp]: "one(G Mod N) = N"
  by (auto simp: FactGroup_def)

lemma mult_FactGroup [simp]: "monoid.mult (G Mod N) = set_mult G"
  by (auto simp: FactGroup_def)

lemma (in normal) inv_FactGroup:
  assumes "X \ carrier (G Mod H)"
  shows "inv\<^bsub>G Mod H\<^esub> X = set_inv X"
proof -
  have X: "X \ rcosets H"
    using assms by (simp add: FactGroup_def)
  moreover have "set_inv X <#> X = H"
    using X by (simp add: normal.rcosets_inv_mult_group_eq normal_axioms)
  moreover have "Group.group (G Mod H)"
    using normal.factorgroup_is_group normal_axioms by blast
  ultimately show ?thesis
    by (simp add: FactGroup_def group.inv_equality normal.setinv_closed normal_axioms)
qed

text\<open>The coset map is a homomorphism from \<^term>\<open>G\<close> to the quotient group
  \<^term>\<open>G Mod H\<close>\<close>
lemma (in normal) r_coset_hom_Mod:
  "(\a. H #> a) \ hom G (G Mod H)"
  by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)

lemma (in comm_group) set_mult_commute:
  assumes "N \ carrier G" "x \ rcosets N" "y \ rcosets N"
  shows "x <#> y = y <#> x"
  using assms unfolding set_mult_def RCOSETS_def
  by auto (metis m_comm r_coset_subset_G subsetCE)+

lemma (in comm_group) abelian_FactGroup:
  assumes "subgroup N G" shows "comm_group(G Mod N)"
proof (rule group.group_comm_groupI)
  have "N \ G"
    by (simp add: assms normal_iff_subgroup)
  then show "Group.group (G Mod N)"
    by (simp add: normal.factorgroup_is_group)
  fix x :: "'a set" and y :: "'a set"
  assume "x \ carrier (G Mod N)" "y \ carrier (G Mod N)"
  then show "x \\<^bsub>G Mod N\<^esub> y = y \\<^bsub>G Mod N\<^esub> x"
    by (metis FactGroup_def assms mult_FactGroup partial_object.simps(1) set_mult_commute subgroup_def)
qed

lemma FactGroup_universal:
  assumes "h \ hom G H" "N \ G"
    and h: "\x y. \x \ carrier G; y \ carrier G; r_coset G N x = r_coset G N y\ \ h x = h y"
  obtains g
  where "g \ hom (G Mod N) H" "\x. x \ carrier G \ g(r_coset G N x) = h x"
proof -
  obtain g where g: "\x. x \ carrier G \ h x = g(r_coset G N x)"
    using h function_factors_left_gen [of "\x. x \ carrier G" "r_coset G N" h] by blast
  show thesis
  proof
    show "g \ hom (G Mod N) H"
    proof (rule homI)
      show "g (u \\<^bsub>G Mod N\<^esub> v) = g u \\<^bsub>H\<^esub> g v"
        if "u \ carrier (G Mod N)" "v \ carrier (G Mod N)" for u v
      proof -
        from that
        obtain x y where xy: "x \ carrier G" "u = r_coset G N x" "y \ carrier G" "v = r_coset G N y"
          by (auto simp: carrier_FactGroup)
        then have "h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"
           by (metis hom_mult [OF \<open>h \<in> hom G H\<close>])
        then show ?thesis
          by (metis Coset.mult_FactGroup xy \<open>N \<lhd> G\<close> g group.subgroup_self normal.axioms(2) normal.rcos_sum subgroup_def)
      qed
    qed (use \<open>h \<in> hom G H\<close> in \<open>auto simp: carrier_FactGroup Pi_iff hom_def simp flip: g\<close>)
  qed (auto simp flip: g)
qed

lemma (in normal) FactGroup_pow:
  fixes k::nat
  assumes "a \ carrier G"
  shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
proof (induction k)
  case 0
  then show ?case
    by (simp add: r_coset_def)
next
  case (Suc k)
  then show ?case
    by (simp add: assms rcos_sum)
qed

lemma (in normal) FactGroup_int_pow:
  fixes k::int
  assumes "a \ carrier G"
  shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
  by (metis Group.group.axioms(1) image_eqI is_group monoid.nat_pow_closed int_pow_def2 assms
         FactGroup_pow carrier_FactGroup inv_FactGroup rcos_inv)

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 \ ('b, 'n) monoid_scheme \ ('a \ 'b) \ 'a set"
    \<comment> \<open>the kernel of a homomorphism\<close>
  where "kernel G H h = {x. x \ carrier G \ h x = \\<^bsub>H\<^esub>}"

lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
  by (auto simp add: kernel_def group.intro intro: subgroup.intro)

text\<open>The kernel of a homomorphism is a normal subgroup\<close>
lemma (in group_hom) normal_kernel: "(kernel G H h) \ G"
  apply (simp only: G.normal_inv_iff subgroup_kernel)
  apply (simp add: kernel_def)
  done

lemma iso_kernel_image:
  assumes "group G" "group H"
  shows "f \ iso G H \ f \ hom G H \ kernel G H f = {\\<^bsub>G\<^esub>} \ f ` carrier G = carrier H"
    (is "?lhs = ?rhs")
proof (intro iffI conjI)
  assume f: ?lhs
  show "f \ hom G H"
    using Group.iso_iff f by blast
  show "kernel G H f = {\\<^bsub>G\<^esub>}"
    using assms f Group.group_def hom_one
    by (fastforce simp add: kernel_def iso_iff_mon_epi mon_iff_hom_one set_eq_iff)
  show "f ` carrier G = carrier H"
    by (meson Group.iso_iff f)
next
  assume ?rhs
  with assms show ?lhs
    by (auto simp: kernel_def iso_def bij_betw_def inj_on_one_iff')
qed

lemma (in group_hom) FactGroup_nonempty:
  assumes "X \ carrier (G Mod kernel G H h)"
  shows "X \ {}"
  using assms unfolding FactGroup_def
  by (metis group_hom.subgroup_kernel group_hom_axioms partial_object.simps(1) subgroup.rcosets_non_empty)

lemma (in group_hom) FactGroup_universal_kernel:
  assumes "N \ G" and h: "N \ kernel G H h"
  obtains g where "g \ hom (G Mod N) H" "\x. x \ carrier G \ g(r_coset G N x) = h x"
proof -
  have "h x = h y"
    if "x \ carrier G" "y \ carrier G" "r_coset G N x = r_coset G N y" for x y
  proof -
    have "x \\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \ N"
      using \<open>N \<lhd> G\<close> group.rcos_self normal.axioms(2) normal_imp_subgroup
         subgroup.rcos_module_imp that by metis
    with h have xy: "x \\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \ kernel G H h"
      by blast
    have "h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = h (x \\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
      by (simp add: that)
    also have "\ = \\<^bsub>H\<^esub>"
      using xy by (simp add: kernel_def)
    finally have "h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = \\<^bsub>H\<^esub>" .
    then show ?thesis
      using H.inv_equality that by fastforce
  qed
  with FactGroup_universal [OF homh \<open>N \<lhd> G\<close>] that show thesis
    by metis
qed

lemma (in group_hom) FactGroup_the_elem_mem:
  assumes X: "X \ carrier (G Mod (kernel G H h))"
  shows "the_elem (h`X) \ carrier H"
proof -
  from X
  obtain g where g: "g \ carrier G"
             and "X = kernel G H h #> g"
    by (auto simp add: FactGroup_def RCOSETS_def)
  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
  thus ?thesis by (auto simp add: g)
qed

lemma (in group_hom) FactGroup_hom:
     "(\X. the_elem (h`X)) \ hom (G Mod (kernel G H h)) H"
proof -
  have "the_elem (h ` (X <#> X')) = the_elem (h ` X) \\<^bsub>H\<^esub> the_elem (h ` X')"
    if X: "X \ carrier (G Mod kernel G H h)" and X': "X' \ carrier (G Mod kernel G H h)" for X X'
  proof -
    obtain g and g'
      where "g \ carrier G" and "g' \ carrier G"
        and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
      using X X' by (auto simp add: FactGroup_def RCOSETS_def)
    hence all: "\x\X. h x = h g" "\x\X'. h x = h g'"
      and Xsub: "X \ carrier G" and X'sub: "X' \ carrier G"
      by (force simp add: kernel_def r_coset_def image_def)+
    hence "h ` (X <#> X') = {h g \\<^bsub>H\<^esub> h g'}" using X X'
      by (auto dest!: FactGroup_nonempty intro!: image_eqI
          simp add: set_mult_def
          subsetD [OF Xsub] subsetD [OF X'sub])
    then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \\<^bsub>H\<^esub> the_elem (h ` X')"
      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
  qed
  then show ?thesis
    by (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
qed

text\<open>Lemma for the following injectivity result\<close>
lemma (in group_hom) FactGroup_subset:
  assumes "g \ carrier G" "g' \ carrier G" "h g = h g'"
  shows "kernel G H h #> g \ kernel G H h #> g'"
  unfolding kernel_def r_coset_def
proof clarsimp
  fix y
  assume "y \ carrier G" "h y = \\<^bsub>H\<^esub>"
  with assms show "\x. x \ carrier G \ h x = \\<^bsub>H\<^esub> \ y \ g = x \ g'"
    by (rule_tac x="y \ g \ inv g'" in exI) (auto simp: G.m_assoc)
qed

lemma (in group_hom) FactGroup_inj_on:
     "inj_on (\X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
proof (simp add: inj_on_def, clarify)
  fix X and X'
  assume X:  "X \ carrier (G Mod kernel G H h)"
     and X': "X' \<in> carrier (G Mod kernel G H h)"
  then
  obtain g and g'
           where gX: "g \ carrier G" "g' \ carrier G"
              "X = kernel G H h #> g" "X' = kernel G H h #> g'"
    by (auto simp add: FactGroup_def RCOSETS_def)
  hence all: "\x\X. h x = h g" "\x\X'. h x = h g'"
    by (force simp add: kernel_def r_coset_def image_def)+
  assume "the_elem (h ` X) = the_elem (h ` X')"
  hence h: "h g = h g'"
    by (simp add: all FactGroup_nonempty X X' the_elem_image_unique)
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
qed

text\<open>If the homomorphism \<^term>\<open>h\<close> is onto \<^term>\<open>H\<close>, then so is the
homomorphism from the quotient group\<close>
lemma (in group_hom) FactGroup_onto:
  assumes h: "h ` carrier G = carrier H"
  shows "(\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
proof
  show "(\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \ carrier H"
    by (auto simp add: FactGroup_the_elem_mem)
  show "carrier H \ (\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
  proof
    fix y
    assume y: "y \ carrier H"
    with h obtain g where g: "g \ carrier G" "h g = y"
      by (blast elim: equalityE)
    hence "(\x\kernel G H h #> g. {h x}) = {y}"
      by (auto simp add: y kernel_def r_coset_def)
    with g show "y \ (\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
      apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
      apply (subst the_elem_image_unique)
      apply auto
      done
  qed
qed

text\<open>If \<^term>\<open>h\<close> is a homomorphism from \<^term>\<open>G\<close> onto \<^term>\<open>H\<close>, then the
quotient group \<^term>\<open>G Mod (kernel G H h)\<close> is isomorphic to \<^term>\<open>H\<close>.\<close>
theorem (in group_hom) FactGroup_iso_set:
  "h ` carrier G = carrier H
   \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G Mod (kernel G H h)) H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
              FactGroup_onto)

corollary (in group_hom) FactGroup_iso :
  "h ` carrier G = carrier H
   \<Longrightarrow> (G Mod (kernel G H h))\<cong> H"
  using FactGroup_iso_set unfolding is_iso_def by auto

lemma (in group_hom) trivial_hom_iff: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "h ` (carrier G) = { \\<^bsub>H\<^esub> } \ kernel G H h = carrier G"
  unfolding kernel_def using one_closed by force

lemma (in group_hom) trivial_ker_imp_inj: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "kernel G H h = { \ }"
  shows "inj_on h (carrier G)"
proof (rule inj_onI)
  fix g1 g2 assume A: "g1 \ carrier G" "g2 \ carrier G" "h g1 = h g2"
  hence "h (g1 \ (inv g2)) = \\<^bsub>H\<^esub>" by simp
  hence "g1 \ (inv g2) = \"
    using A assms unfolding kernel_def by blast
  thus "g1 = g2"
    using A G.inv_equality G.inv_inv by blast
qed

lemma (in group_hom) inj_iff_trivial_ker:
  shows "inj_on h (carrier G) \ kernel G H h = { \ }"
proof
  assume inj: "inj_on h (carrier G)" show "kernel G H h = { \ }"
    unfolding kernel_def
  proof (auto)
    fix a assume "a \ carrier G" "h a = \\<^bsub>H\<^esub>" thus "a = \"
      using inj hom_one unfolding inj_on_def by force
  qed
next
  show "kernel G H h = { \ } \ inj_on h (carrier G)"
    using trivial_ker_imp_inj by simp
qed

lemma (in group_hom) induced_group_hom':
  assumes "subgroup I G" shows "group_hom (G \ carrier := I \) H h"
proof -
  have "h \ hom (G \ carrier := I \) H"
    using homh subgroup.subset[OF assms] unfolding hom_def by (auto, meson hom_mult subsetCE)
  thus ?thesis
    using subgroup.subgroup_is_group[OF assms G.group_axioms] group_axioms
    unfolding group_hom_def group_hom_axioms_def by auto
qed

lemma (in group_hom) inj_on_subgroup_iff_trivial_ker:
  assumes "subgroup I G"
  shows "inj_on h I \ kernel (G \ carrier := I \) H h = { \ }"
  using group_hom.inj_iff_trivial_ker[OF induced_group_hom'[OF assms]] by simp

lemma set_mult_hom:
  assumes "h \ hom G H" "I \ carrier G" and "J \ carrier G"
  shows "h ` (I <#>\<^bsub>G\<^esub> J) = (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
proof
  show "h ` (I <#>\<^bsub>G\<^esub> J) \ (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
  proof
    fix a assume "a \ h ` (I <#>\<^bsub>G\<^esub> J)"
    then obtain i j where i: "i \ I" and j: "j \ J" and "a = h (i \\<^bsub>G\<^esub> j)"
      unfolding set_mult_def by auto
    hence "a = (h i) \\<^bsub>H\<^esub> (h j)"
      using assms unfolding hom_def by blast
    thus "a \ (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
      using i and j unfolding set_mult_def by auto
  qed
next
  show "(h ` I) <#>\<^bsub>H\<^esub> (h ` J) \ h ` (I <#>\<^bsub>G\<^esub> J)"
  proof
    fix a assume "a \ (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
    then obtain i j where i: "i \ I" and j: "j \ J" and "a = (h i) \\<^bsub>H\<^esub> (h j)"
      unfolding set_mult_def by auto
    hence "a = h (i \\<^bsub>G\<^esub> j)"
      using assms unfolding hom_def by fastforce
    thus "a \ h ` (I <#>\<^bsub>G\<^esub> J)"
      using i and j unfolding set_mult_def by auto
  qed
qed

corollary coset_hom:
  assumes "h \ hom G H" "I \ carrier G" "a \ carrier G"
  shows "h ` (a <#\<^bsub>G\<^esub> I) = h a <#\<^bsub>H\<^esub> (h ` I)" and "h ` (I #>\<^bsub>G\<^esub> a) = (h ` I) #>\<^bsub>H\<^esub> h a"
  unfolding l_coset_eq_set_mult r_coset_eq_set_mult using assms set_mult_hom[OF assms(1)] by auto

corollary (in group_hom) set_mult_ker_hom:
  assumes "I \ carrier G"
  shows "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
proof -
  have ker_in_carrier: "kernel G H h \ carrier G"
    unfolding kernel_def by auto

  have "h ` (kernel G H h) = { \\<^bsub>H\<^esub> }"
    unfolding kernel_def by force
  moreover have "h ` I \ carrier H"
    using assms by auto
  hence "(h ` I) <#>\<^bsub>H\<^esub> { \\<^bsub>H\<^esub> } = h ` I" and "{ \\<^bsub>H\<^esub> } <#>\<^bsub>H\<^esub> (h ` I) = h ` I"
    unfolding set_mult_def by force+
  ultimately show "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
    using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+
qed

subsubsection\<open>Trivial homomorphisms\<close>

definition trivial_homomorphism where
"trivial_homomorphism G H f \ f \ hom G H \ (\x \ carrier G. f x = one H)"

lemma trivial_homomorphism_kernel:
   "trivial_homomorphism G H f \ f \ hom G H \ kernel G H f = carrier G"
  by (auto simp: trivial_homomorphism_def kernel_def)

lemma (in group) trivial_homomorphism_image:
   "trivial_homomorphism G H f \ f \ hom G H \ f ` carrier G = {one H}"
  by (auto simp: trivial_homomorphism_def) (metis one_closed rev_image_eqI)

subsection \<open>Image kernel theorems\<close>

lemma group_Int_image_ker:
  assumes f: "f \ hom G H" and g: "g \ hom H K"
    and "inj_on (g \ f) (carrier G)" "group G" "group H" "group K"
  shows "(f ` carrier G) \ (kernel H K g) = {\\<^bsub>H\<^esub>}"
proof -
  have "(f ` carrier G) \ (kernel H K g) \ {\\<^bsub>H\<^esub>}"
    using assms
    apply (clarsimp simp: kernel_def o_def)
    by (metis group.is_monoid hom_one inj_on_eq_iff monoid.one_closed)
  moreover have "one H \ f ` carrier G"
    by (metis f \<open>group G\<close> \<open>group H\<close> group.is_monoid hom_one image_iff monoid.one_closed)
  moreover have "one H \ kernel H K g"
    unfolding kernel_def using Group.group_def \<open>group H\<close> \<open>group K\<close> g hom_one by blast
  ultimately show ?thesis
    by blast
qed

lemma group_sum_image_ker:
  assumes f: "f \ hom G H" and g: "g \ hom H K" and eq: "(g \ f) ` (carrier G) = carrier K"
     and "group G" "group H" "group K"
  shows "set_mult H (f ` carrier G) (kernel H K g) = carrier H" (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    apply (clarsimp simp: kernel_def set_mult_def)
    by (meson \<open>group H\<close> f group.is_monoid hom_in_carrier monoid.m_closed)
  have "\x\carrier G. \z. z \ carrier H \ g z = \\<^bsub>K\<^esub> \ y = f x \\<^bsub>H\<^esub> z"
    if y: "y \ carrier H" for y
  proof -
    have "g y \ carrier K"
      using g hom_carrier that by blast
    with assms obtain x where x: "x \ carrier G" "(g \ f) x = g y"
      by (metis image_iff)
    with assms have invf: "inv\<^bsub>H\<^esub> f x \\<^bsub>H\<^esub> y \ carrier H"
      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
    moreover
    have "g (inv\<^bsub>H\<^esub> f x \\<^bsub>H\<^esub> y) = \\<^bsub>K\<^esub>"
    proof -
      have "inv\<^bsub>H\<^esub> f x \ carrier H"
        by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
      then have "g (inv\<^bsub>H\<^esub> f x \\<^bsub>H\<^esub> y) = g (inv\<^bsub>H\<^esub> f x) \\<^bsub>K\<^esub> g y"
        by (simp add: hom_mult [OF g] y)
      also have "\ = inv\<^bsub>K\<^esub> (g (f x)) \\<^bsub>K\<^esub> g y"
        using assms x(1)
        by (metis (mono_tags, lifting) group_hom.hom_inv group_hom.intro group_hom_axioms.intro hom_carrier image_subset_iff)
      also have "\ = \\<^bsub>K\<^esub>"
        using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2) by fastforce
      finally show ?thesis .
    qed
    moreover
    have "y = f x \\<^bsub>H\<^esub> (inv\<^bsub>H\<^esub> f x \\<^bsub>H\<^esub> y)"
      using x y
      by (meson \<open>group H\<close> invf f group.inv_solve_left' hom_in_carrier)
    ultimately
    show ?thesis
      using x y by force
  qed
  then show "?rhs \ ?lhs"
    by (auto simp: kernel_def set_mult_def)
qed

lemma group_sum_ker_image:
  assumes f: "f \ hom G H" and g: "g \ hom H K" and eq: "(g \ f) ` (carrier G) = carrier K"
     and "group G" "group H" "group K"
   shows "set_mult H (kernel H K g) (f ` carrier G) = carrier H" (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    apply (clarsimp simp: kernel_def set_mult_def)
    by (meson \<open>group H\<close> f group.is_monoid hom_in_carrier monoid.m_closed)
  have "\w\carrier H. \x \ carrier G. g w = \\<^bsub>K\<^esub> \ y = w \\<^bsub>H\<^esub> f x"
    if y: "y \ carrier H" for y
  proof -
    have "g y \ carrier K"
      using g hom_carrier that by blast
    with assms obtain x where x: "x \ carrier G" "(g \ f) x = g y"
      by (metis image_iff)
    with assms have carr: "(y \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \ carrier H"
      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
    moreover
    have "g (y \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = \\<^bsub>K\<^esub>"
    proof -
      have "inv\<^bsub>H\<^esub> f x \ carrier H"
        by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
      then have "g (y \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = g y \\<^bsub>K\<^esub> g (inv\<^bsub>H\<^esub> f x)"
        by (simp add: hom_mult [OF g] y)
      also have "\ = g y \\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> (g (f x))"
        using assms x(1)
        by (metis group_hom.hom_inv group_hom_axioms.intro group_hom_def hom_in_carrier)
      also have "\ = \\<^bsub>K\<^esub>"
        using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2)
        by (simp add: group.r_inv)
      finally show ?thesis .
    qed
    moreover
    have "y = (y \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \\<^bsub>H\<^esub> f x"
      using x y by (meson \<open>group H\<close> carr f group.inv_solve_right hom_carrier image_subset_iff)
    ultimately
    show ?thesis
      using x y by force
  qed
  then show "?rhs \ ?lhs"
    by (force simp: kernel_def set_mult_def)
qed

lemma group_semidirect_sum_ker_image:
  assumes "(g \ f) \ iso G K" "f \ hom G H" "g \ hom H K" "group G" "group H" "group K"
  shows "(kernel H K g) \ (f ` carrier G) = {\\<^bsub>H\<^esub>}"
        "kernel H K g <#>\<^bsub>H\<^esub> (f ` carrier G) = carrier H"
  using assms
  by (simp_all add: iso_iff_mon_epi group_Int_image_ker group_sum_ker_image epi_def mon_def Int_commute [of "kernel H K g"])

lemma group_semidirect_sum_image_ker:
  assumes f: "f \ hom G H" and g: "g \ hom H K" and iso: "(g \ f) \ iso G K"
     and "group G" "group H" "group K"
   shows "(f ` carrier G) \ (kernel H K g) = {\\<^bsub>H\<^esub>}"
          "f ` carrier G <#>\<^bsub>H\<^esub> (kernel H K g) = carrier H"
  using group_Int_image_ker [OF f g] group_sum_image_ker [OF f g] assms
  by (simp_all add: iso_def bij_betw_def)

subsection \<open>Factor Groups and Direct product\<close>

lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  assumes "group K"
    and "H \ G"
    and "N \ K"
  shows "H \ N \ G \\ K"
proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]])
  show sub : "subgroup (H \ N) (G \\ K)"
    using DirProd_subgroups[OF group_axioms normal_imp_subgroup[OF assms(2)]assms(1)
         normal_imp_subgroup[OF assms(3)]].
  show "\x h. x \ carrier (G\\K) \ h \ H\N \ x \\<^bsub>G\\K\<^esub> h \\<^bsub>G\\K\<^esub> inv\<^bsub>G\\K\<^esub> x \ H\N"
  proof-
    fix x h assume xGK : "x \ carrier (G \\ K)" and hHN : " h \ H \ N"
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.40Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

SSL Coset.thy Interaktion und PortierbarkeitIsabelle

Haftungshinweis

Bemerkung:

SSL Coset.thy Interaktion und
PortierbarkeitIsabelle