Theory HOL-Algebra.Coset

(*  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 ‹Cosets and Quotient Groups›

definition
  r_coset    :: "[_, 'a set, 'a]  'a set"    (infixl #>ı› 60)
  where "H #>Ga = (hH. {h Ga})"

definition
  l_coset    :: "[_, 'a, 'a set]  'a set"    (infixl <#ı› 60)
  where "a <#GH = (hH. {a Gh})"

definition
  RCOSETS  :: "[_, 'a set]  ('a set)set"   (rcosetsı _› [81] 80)
  where "rcosetsGH = (acarrier G. {H #>Ga})"

definition
  set_mult  :: "[_, 'a set ,'a set]  'a set" (infixl <#>ı› 60)
  where "H <#>GK = (hH. kK. {h Gk})"

definition
  SET_INV :: "[_,'a set]  'a set"  (set'_invı _› [81] 80)
  where "set_invGH = (hH. {invGh})"


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: contributor ‹Martin Baillon›
  fixes G (structure)
  shows "x <# H = {x} <#> H"
  unfolding l_coset_def set_mult_def by simp

lemma r_coset_eq_set_mult: contributor ‹Martin Baillon›
  fixes G (structure)
  shows "H #> x = H <#> {x}"
  unfolding r_coset_def set_mult_def by simp

lemma (in subgroup) rcosets_non_empty: contributor ‹Paulo Emílio de Vilhena›
  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: contributor ‹Paulo Emílio de Vilhena›
  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 <#>GK  H' <#>GK'" contributor ‹Paulo Emílio de Vilhena›
  unfolding set_mult_def by (simp add: UN_mono)


subsection ‹Stable Operations for Subgroups›

lemma set_mult_consistent [simp]: contributor ‹Paulo Emílio de Vilhena›
  "N <#>(G  carrier := H )K = N <#>GK"
  unfolding set_mult_def by simp

lemma r_coset_consistent [simp]: contributor ‹Paulo Emílio de Vilhena›
  "I #>G  carrier := H h = I #>Gh"
  unfolding r_coset_def by simp

lemma l_coset_consistent [simp]: contributor ‹Paulo Emílio de Vilhena›
  "h <#G  carrier := H I = h <#GI"
  unfolding l_coset_def by simp


subsection ‹Basic Properties of set multiplication›

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: contributor ‹Martin Baillon›
  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 ‹Basic Properties of Cosets›

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 = 𝟭H x = 𝟭G)"
  by (auto simp: mon_def inj_on_one_iff')

lemma (in group_hom) iso_iff: "h  iso G H  carrier H  h ` carrier G  (xcarrier G. h x = 𝟭H 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
  ― ‹Alternative proof is to put termx=𝟭 in repr_independence›.›
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) ‹Opposite of @{thm [source] "repr_independence"}
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 ‹Elements of a right coset are in the carrier›
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 ‹Module property of right cosets›
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 ‹Right cosets are subsets of the carrier.›
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 ‹Multiplication of general subsets›

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 ‹Normal subgroups›

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'  H" "h  x = x  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‹Alternative characterization of normal subgroups›
lemma (in group) normal_inv_iff:
     "(N  G) =
      (subgroup N G  (x  carrier G. h  N. x  h  (inv x)  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. xcarrier G  hN. 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 "(hN. {h  x}) = (hN. {x  h})"
    proof
      show "(hN. {h  x})  (hN. {x  h})"
      proof clarify
        fix n
        assume n: "n  N"
        show "n  x  (hN. {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 "(hN. {x  h})  (hN. {h  x})"
      proof clarify
        fix n
        assume n: "n  N"
        show "x  n  (hN. {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 ‹The intersection of two normal subgroups is, again, a normal subgroup.›
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 ‹Being a normal subgroup is preserved by surjective homomorphisms.›

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

text ‹Being a normal subgroup is preserved by group isomorphisms.›
lemma iso_normal_subgroup:
  assumes φ: "φ  iso G F" "group G" "group F" "H  G"
  shows "(φ ` H)  F"
  by (meson assms Group.iso_iff group_hom_axioms_def group_hom_def normal.surj_hom_normal_subgroup)

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

subsection‹More Properties of Left Cosets›

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 ‹Set of Inverses of an r_coset›.›

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  (jH. {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  (jH. {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 ‹Theorems for <#>› with #>› or <#›.›

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
       (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
       (H <#> (H #> x)) #> y = H #> (x  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
       (H #> x) <#> (H #> y) = H #> (x  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"
  ― ‹generalizes subgroup_mult_id›
  by (auto simp add: RCOSETS_def subset
        setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)


subsubsection‹An Equivalence Relation›

definition
  r_congruent :: "[('a,'b)monoid_scheme, 'a set]  ('a*'a)set"  (rcongı _›)
  where "rcongGH = {(x,y). x  carrier G  y  carrier G  invGx Gy  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)
    have "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‹Equivalence classes of rcong› correspond to left cosets.
  Was there a mistake in the definitions? I'd have expected them to
  correspond to right cosets.›

(* 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' ⟹ 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‹Two Distinct Right Cosets are Disjoint›

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  (hH. {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 ‹Further lemmas for r_congruent›

text ‹The relation is a congruence›

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 ‹Order of a Group and Lagrange's Theorem›

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‹The next two lemmas support the proof of card_cosets_equal›.›
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 infinite (carrier G)  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"] finite H 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 infinite (carrier G) order_gt_0_iff_finite by blast
    qed
    thus ?thesis using infinite (carrier G) by (simp add: order_def)
  qed
qed

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

subsection ‹Quotient Groups: Factorization of a Group›

definition
  FactGroup :: "[('a,'b) monoid_scheme, 'a set]  ('a set) monoid" (infixl Mod 65)
    ― ‹Actually defined for groups rather than monoids›
   where "FactGroup G H = carrier = rcosetsGH, 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
       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  yrcosets 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 "invG Mod HX = 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‹The coset map is a homomorphism from termG to the quotient group
  termG Mod H
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 G Mod Ny = y G Mod Nx"
    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 G Mod Nv) = g u Hg 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 Gy) = h x Hh y"
           by (metis hom_mult [OF h  hom G H])
        then show ?thesis
          by (metis Coset.mult_FactGroup xy N  G g group.subgroup_self normal.axioms(2) normal.rcos_sum subgroup_def)
      qed
    qed (use h  hom G H in auto simp: carrier_FactGroup Pi_iff hom_def simp flip: g)
  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‹The First Isomorphism Theorem›

text‹The quotient by the kernel of a homomorphism is isomorphic to the
  range of that homomorphism.›

definition
  kernel :: "('a, 'm) monoid_scheme  ('b, 'n) monoid_scheme   ('a  'b)  'a set"
    ― ‹the kernel of a homomorphism›
  where "kernel G H h = {x. x  carrier G  h x = 𝟭H}"

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

text‹The kernel of a homomorphism is a normal subgroup›
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 = {𝟭G}  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 = {𝟭G}"
    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 GinvGy  N"
      using N  G group.rcos_self normal.axioms(2) normal_imp_subgroup
         subgroup.rcos_module_imp that by metis 
    with h have xy: "x GinvGy  kernel G H h"
      by blast
    have "h x HinvH(h y) = h (x GinvGy)"
      by (simp add: that)
    also have " = 𝟭H⇙"
      using xy by (simp add: kernel_def)
    finally have "h x HinvH(h y) = 𝟭H⇙" .
    then show ?thesis
      using H.inv_equality that by fastforce
  qed
  with FactGroup_universal [OF homh N  G] 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) Hthe_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: "xX. h x = h g" "xX'. 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 Hh 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) Hthe_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‹Lemma for the following injectivity result›
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 = 𝟭H⇙"
  with assms show "x. x  carrier G  h x = 𝟭H 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'  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: "xX. h x = h g" "xX'. 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‹If the homomorphism termh is onto termH, then so is the
homomorphism from the quotient group›
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 "(xkernel 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‹If termh is a homomorphism from termG onto termH, then the
 quotient group termG Mod (kernel G H h) is isomorphic to termH.›
theorem (in group_hom) FactGroup_iso_set:
  "h ` carrier G = carrier H
    (λX. the_elem (h`X))  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
    (G Mod (kernel G H h)) H"
  using FactGroup_iso_set unfolding is_iso_def by auto


lemma (in group_hom) trivial_hom_iff: contributor ‹Paulo Emílio de Vilhena›
  "h ` (carrier G) = { 𝟭H}  kernel G H h = carrier G"
  unfolding kernel_def using one_closed by force

lemma (in group_hom) trivial_ker_imp_inj: contributor ‹Paulo Emílio de Vilhena›
  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)) = 𝟭H⇙" 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 = 𝟭H⇙" 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 <#>GJ) = (h ` I) <#>H(h ` J)"
proof
  show "h ` (I <#>GJ)  (h ` I) <#>H(h ` J)"
  proof
    fix a assume "a  h ` (I <#>GJ)"
    then obtain i j where i: "i  I" and j: "j  J" and "a = h (i Gj)"
      unfolding set_mult_def by auto
    hence "a = (h i) H(h j)"
      using assms unfolding hom_def by blast
    thus "a  (h ` I) <#>H(h ` J)"
      using i and j unfolding set_mult_def by auto
  qed
next
  show "(h ` I) <#>H(h ` J)  h ` (I <#>GJ)"
  proof
    fix a assume "a  (h ` I) <#>H(h ` J)"
    then obtain i j where i: "i  I" and j: "j  J" and "a = (h i) H(h j)"
      unfolding set_mult_def by auto
    hence "a = h (i Gj)"
      using assms unfolding hom_def by fastforce
    thus "a  h ` (I <#>GJ)"
      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 <#GI) = h a <#H(h ` I)" and "h ` (I #>Ga) = (h ` I) #>Hh 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) = { 𝟭H}"
    unfolding kernel_def by force
  moreover have "h ` I  carrier H"
    using assms by auto
  hence "(h ` I) <#>H{ 𝟭H} = h ` I" and "{ 𝟭H} <#>H(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‹Trivial homomorphisms›

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 ‹Image kernel theorems›

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) = {𝟭H}"
proof -
  have "(f ` carrier G)  (kernel H K g)  {𝟭H}"
    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 group G group H 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 group H group K 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 group H f group.is_monoid hom_in_carrier monoid.m_closed)
  have "xcarrier G. z. z  carrier H  g z = 𝟭K y = f x Hz"
    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: "invHf x Hy  carrier H"
      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
    moreover
    have "g (invHf x Hy) = 𝟭K⇙"
    proof -
      have "invHf x  carrier H"
        by (meson group H f group.inv_closed hom_carrier image_subset_iff x(1))
      then have "g (invHf x Hy) = g (invHf x) Kg y"
        by (simp add: hom_mult [OF g] y)
      also have " = invK(g (f x)) Kg 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 " = 𝟭K⇙"
        using g y  carrier K assms(6) group.l_inv x(2) by fastforce
      finally show ?thesis .
    qed
    moreover
    have "y = f x H(invHf x Hy)"
      using x y
      by (meson group H 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 group H f group.is_monoid hom_in_carrier monoid.m_closed)
  have "wcarrier H. x  carrier G. g w = 𝟭K y = w Hf 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 HinvHf x)  carrier H"
      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
    moreover
    have "g (y HinvHf x) = 𝟭K⇙"
    proof -
      have "invHf x  carrier H"
        by (meson group H f group.inv_closed hom_carrier image_subset_iff x(1))
      then have "g (y HinvHf x) = g y Kg (invHf x)"
        by (simp add: hom_mult [OF g] y)
      also have " = g y KinvK(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 " = 𝟭K⇙"
        using g y  carrier K assms(6) group.l_inv x(2)
        by (simp add: group.r_inv)
      finally show ?thesis .
    qed
    moreover
    have "y = (y HinvHf x) Hf x"
      using x y by (meson group H 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) = {𝟭H}"
        "kernel H K g <#>H(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) = {𝟭H}"
          "f ` carrier G <#>H(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 ‹Factor Groups and Direct product›

lemma (in group) DirProd_normal : contributor ‹Martin Baillon›
  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)<