Theory Coset

theory Coset
imports Group
(*  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 #>G a = (⋃h∈H. {h ⊗G a})"

definition
  l_coset    :: "[_, 'a, 'a set] ⇒ 'a set"    (infixl "<#ı" 60)
  where "a <#G H = (⋃h∈H. {a ⊗G h})"

definition
  RCOSETS  :: "[_, 'a set] ⇒ ('a set)set"   ("rcosetsı _" [81] 80)
  where "rcosetsG H = (⋃a∈carrier G. {H #>G a})"

definition
  set_mult  :: "[_, 'a set ,'a set] ⇒ 'a set" (infixl "<#>ı" 60)
  where "H <#>G K = (⋃h∈H. ⋃k∈K. {h ⊗G k})"

definition
  SET_INV :: "[_,'a set] ⇒ 'a set"  ("set'_invı _" [81] 80)
  where "set_invG H = (⋃h∈H. {invG 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"

(*Next two lemmas contributed by Martin Baillon.*)

lemma l_coset_eq_set_mult:
  fixes G (structure)
  shows "x <# H = {x} <#> H"
  unfolding l_coset_def set_mult_def by simp

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

(* Next five lemmas contributed by Paulo Emílio de Vilhena.                    *)

lemma (in subgroup) rcosets_non_empty:
  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:
  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 <#>G K ⊆ H' <#>G K'"
  unfolding set_mult_def by (simp add: UN_mono)


subsection ‹Stable Operations for Subgroups›

lemma set_mult_consistent [simp]:
  "N <#>(G ⦇ carrier := H ⦈) K = N <#>G K"
  unfolding set_mult_def by simp

lemma r_coset_consistent [simp]:
  "I #>G ⦇ carrier := H ⦈ h = I #>G h"
  unfolding r_coset_def by simp

lemma l_coset_consistent [simp]:
  "h <#G ⦇ carrier := H ⦈ I = h <#G I"
  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)

(* Next lemma contributed by Martin Baillon.*)
lemma (in group) set_mult_assoc:
  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) 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 @{term "x=𝟭"} 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 (simp add: normal_def subgroup_def)

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)


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. 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"
proof(intro normal_invI )
  show "subgroup {𝟭} G"
    by (simp add: subgroup_def)
  show "⋀x h. x ∈ carrier G ⟹ h ∈ {𝟭} ⟹ x ⊗ h ⊗ inv x ∈ {𝟭}" by simp
qed


subsection‹More Properties of Left Cosets›

lemma (in group) l_repr_independence:
  assumes "y ∈ x <# H" "x ∈ carrier G" "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 f3: "h' ∈ carrier G"
      by (meson assms(3) h'(1) subgroup.mem_carrier)
    have f4: "h ∈ carrier G"
      by (meson assms(3) subgroup.mem_carrier that)
    then show ?thesis
      by (metis assms(2) f3 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 assms(3) h'(1) subgroup_def)
  moreover have "⋀ h. h ∈ H ⟹ y ⊗ h = x ⊗ (h' ⊗ h)"
    using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
  hence "⋀ yh. yh ∈ y <# H ⟹ yh ∈ x <# H"
    unfolding l_coset_def using subgroup.m_closed[OF assms(3) 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 ∈ (⋃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 ‹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 "rcongG H = {(x,y). x ∈ carrier G ∧ y ∈ carrier G ∧ invG x ⊗G 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 "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 ∈ (⋃h∈H. {h ⊗ b})"
proof -
  interpret subgroup H G by fact
  from p show ?thesis apply (rule_tac UN_I [of "hb ⊗ ((inv ha) ⊗ h)"])
    apply blast by (simp add: inv_solve_left m_assoc)
qed

lemma (in group) rcos_disjoint:
  assumes "subgroup H G"
  assumes p: "a ∈ rcosets H" "b ∈ rcosets H" "a≠b"
  shows "a ∩ b = {}"
proof -
  interpret subgroup H G by fact
  from p show ?thesis
    apply (simp add: RCOSETS_def r_coset_def)
    apply (blast intro: rcos_equation assms sym)
    done
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 (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) rcosets_part_G:
  assumes "subgroup H G"
  shows "⋃(rcosets H) = carrier G"
proof -
  interpret subgroup H G by fact
  show ?thesis
    apply (rule equalityI)
    apply (force simp add: RCOSETS_def r_coset_def)
    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
    done
qed

lemma (in group) cosets_finite:
     "⟦c ∈ rcosets H;  H ⊆ carrier G;  finite (carrier G)⟧ ⟹ finite c"
apply (auto simp add: RCOSETS_def)
apply (simp add: r_coset_subset_G [THEN finite_subset])
done

text‹The next two lemmas support the proof of ‹card_cosets_equal›.›
lemma (in group) inj_on_f:
    "⟦H ⊆ carrier G;  a ∈ carrier G⟧ ⟹ inj_on (λy. y ⊗ inv a) (H #> a)"
apply (rule inj_onI)
apply (subgoal_tac "x ∈ carrier G ∧ y ∈ carrier G")
 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
apply (simp add: subsetD)
done

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:
     "⟦finite(carrier G); subgroup H G⟧
      ⟹ card(rcosets H) * card(H) = order(G)"
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
apply (subst mult.commute)
apply (rule card_partition)
   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
  apply (simp add: rcosets_part_G)
  apply (simp add: card_rcosets_equal subgroup.subset)
apply (simp add: rcos_disjoint)
done

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 note inf_G = this
  thus ?thesis
  proof (cases "finite H")
    case False thus ?thesis using inf_G  by (simp add: order_def)
  next
    case True note finite_H = this
    have "infinite (rcosets H)"
    proof (rule ccontr)
      assume "¬ infinite (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 inf_G order_gt_0_iff_finite by blast
    qed
    thus ?thesis using inf_G by (simp add: order_def)
  qed
qed


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 = rcosetsG 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⟧
      ⟹ 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)"
apply (simp add: FactGroup_def)
apply (rule groupI)
    apply (simp add: setmult_closed)
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
  apply (simp add: restrictI setmult_closed rcosets_assoc)
 apply (simp add: normal_imp_subgroup
                  subgroup_in_rcosets rcosets_mult_eq)
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
done

lemma mult_FactGroup [simp]: "X ⊗(G Mod H) X' = X <#>G X'"
  by (simp add: FactGroup_def)

lemma (in normal) inv_FactGroup:
     "X ∈ carrier (G Mod H) ⟹ invG Mod H X = set_inv X"
apply (rule group.inv_equality [OF factorgroup_is_group])
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
done

text‹The coset map is a homomorphism from @{term G} to the quotient group
  @{term "G Mod H"}›
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)


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"
apply (rule subgroup.intro)
apply (auto simp add: kernel_def group.intro is_group)
done

text‹The kernel of a homomorphism is a normal subgroup›
lemma (in group_hom) normal_kernel: "(kernel G H h) ⊲ G"
apply (simp add: G.normal_inv_iff subgroup_kernel)
apply (simp add: kernel_def)
done

lemma (in group_hom) FactGroup_nonempty:
  assumes X: "X ∈ carrier (G Mod kernel G H h)"
  shows "X ≠ {}"
proof -
  from X
  obtain g where "g ∈ carrier G"
             and "X = kernel G H h #> g"
    by (auto simp add: FactGroup_def RCOSETS_def)
  thus ?thesis
   by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
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"
apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
proof (intro ballI)
  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 "g ∈ carrier G" and "g' ∈ carrier G"
             and "X = kernel G H h #> g" and "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'"
    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 ⊗H 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) ⊗H the_elem (h ` X')"
    by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
qed


text‹Lemma for the following injectivity result›
lemma (in group_hom) FactGroup_subset:
     "⟦g ∈ carrier G; g' ∈ carrier G; h g = h g'⟧
      ⟹  kernel G H h #> g ⊆ kernel G H h #> g'"
apply (clarsimp simp add: kernel_def r_coset_def)
apply (rename_tac y)
apply (rule_tac x="y ⊗ g ⊗ inv g'" in exI)
apply (simp add: G.m_assoc)
done

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: "∀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‹If the homomorphism @{term h} is onto @{term H}, 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 "(⋃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‹If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
 quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.›
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


(* Next two lemmas contributed by Paulo Emílio de Vilhena. *)

lemma (in group_hom) trivial_hom_iff:
  "(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:
  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


(* Next subsection contributed by Martin Baillon. *)

subsection ‹Theorems about Factor Groups and Direct product›

lemma (in group) DirProd_normal :
  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 ⊗G××K h ⊗G××K invG××K x ∈ H×N"
  proof-
    fix x h assume xGK : "x ∈ carrier (G ×× K)" and hHN : " h ∈ H × N"
    hence hGK : "h ∈ carrier (G ×× K)" using subgroup.subset[OF sub] by auto
    from xGK obtain x1 x2 where x1x2 :"x1 ∈ carrier G" "x2 ∈ carrier K" "x = (x1,x2)"
      unfolding DirProd_def by fastforce
    from hHN obtain h1 h2 where h1h2 : "h1 ∈ H" "h2 ∈ N" "h = (h1,h2)"
      unfolding DirProd_def by fastforce
    hence h1h2GK : "h1 ∈ carrier G" "h2 ∈ carrier K"
      using normal_imp_subgroup subgroup.subset assms apply blast+.
    have "invG ×× K x = (invG x1,invK x2)"
      using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
    hence "x ⊗G ×× K h ⊗G ×× K invG ×× K x = (x1 ⊗ h1 ⊗ inv x1,x2 ⊗K h2 ⊗K invK x2)"
      using h1h2 x1x2 h1h2GK by auto
    moreover have "x1 ⊗ h1 ⊗ inv x1 ∈ H" "x2 ⊗K h2 ⊗K invK x2 ∈ N"
      using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
    hence "(x1 ⊗ h1 ⊗ inv x1, x2 ⊗K h2 ⊗K invK x2)∈ H × N" by auto
    ultimately show " x ⊗G ×× K h ⊗G ×× K invG ×× K x ∈ H × N" by auto
  qed
qed

lemma (in group) FactGroup_DirProd_multiplication_iso_set :
  assumes "group K"
    and "H ⊲ G"
    and "N ⊲ K"
  shows "(λ (X, Y). X × Y) ∈ iso  ((G Mod H) ×× (K Mod N)) (G ×× K Mod H × N)"

proof-
  have R :"(λ(X, Y). X × Y) ∈ carrier (G Mod H) × carrier (K Mod N) → carrier (G ×× K Mod H × N)"
    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
  moreover have "(∀x∈carrier (G Mod H). ∀y∈carrier (K Mod N). ∀xa∈carrier (G Mod H).
                ∀ya∈carrier (K Mod N). (x <#> xa) × (y <#>K ya) =  x × y <#>G ×× K xa × ya)"
    unfolding set_mult_def by force
  moreover have "(∀x∈carrier (G Mod H). ∀y∈carrier (K Mod N). ∀xa∈carrier (G Mod H).
                 ∀ya∈carrier (K Mod N).  x × y = xa × ya ⟶ x = xa ∧ y = ya)"
    unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
    by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
  moreover have "(λ(X, Y). X × Y) ` (carrier (G Mod H) × carrier (K Mod N)) =
                                     carrier (G ×× K Mod H × N)"
    unfolding image_def  apply auto using R apply force
    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
  ultimately show ?thesis
    unfolding iso_def hom_def bij_betw_def inj_on_def by simp
qed

corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
  assumes "group K"
    and "H ⊲ G"
    and "N ⊲ K"
  shows "  ((G Mod H) ×× (K Mod N)) ≅ (G ×× K Mod H × N)"
  unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto

corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
  assumes "group K"
    and "H ⊲ G"
    and "N ⊲ K"
  shows "(G ×× K Mod H × N) ≅ ((G Mod H) ×× (K Mod N))"
  using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms
        DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
  by blast

subsubsection "More Lemmas about set multiplication"

(*A group multiplied by a subgroup stays the same*)
lemma (in group) set_mult_carrier_idem:
  assumes "subgroup H G"
  shows "(carrier G) <#> H = carrier G"
proof
  show "(carrier G)<#>H ⊆ carrier G"
    unfolding set_mult_def using subgroup.subset assms by blast
next
  have " (carrier G) #>  𝟭 = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
  moreover have "(carrier G) #>  𝟭 ⊆ (carrier G) <#> H" unfolding set_mult_def r_coset_def
    using assms subgroup.one_closed[OF assms] by blast
  ultimately show "carrier G ⊆ (carrier G) <#> H" by simp
qed

(*Same lemma as above, but everything is included in a subgroup*)
lemma (in group) set_mult_subgroup_idem:
  assumes HG: "subgroup H G" and NG: "subgroup N (G ⦇ carrier := H ⦈)"
  shows "H <#> N = H"
  using group.set_mult_carrier_idem[OF subgroup.subgroup_is_group[OF HG group_axioms] NG] by simp

(*A normal subgroup is commutative with set_mult*)
lemma (in group) commut_normal:
  assumes "subgroup H G" and "N⊲G"
  shows "H<#>N = N<#>H"
proof-
  have aux1: "{H <#> N} = {⋃h∈H. h <# N }" unfolding set_mult_def l_coset_def by auto
  also have "... = {⋃h∈H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
  moreover have aux2: "{N <#> H} = {⋃h∈H. N #> h }"unfolding set_mult_def r_coset_def by auto
  ultimately show "H<#>N = N<#>H" by simp
qed

(*Same lemma as above, but everything is included in a subgroup*)
lemma (in group) commut_normal_subgroup:
  assumes "subgroup H G" and "N ⊲ (G⦇ carrier := H ⦈)"
    and "subgroup K (G ⦇ carrier := H ⦈)"
  shows "K <#> N = N <#> K"
  using group.commut_normal[OF subgroup.subgroup_is_group[OF assms(1) group_axioms] assms(3,2)] by simp



subsubsection "Lemmas about intersection and normal subgroups"

lemma (in group) normal_inter:
  assumes "subgroup H G"
    and "subgroup K G"
    and "H1⊲G⦇carrier := H⦈"
  shows " (H1∩K)⊲(G⦇carrier:= (H∩K)⦈)"
proof-
  define HK and H1K and GH and GHK
    where "HK = H∩K" and "H1K=H1∩K" and "GH =G⦇carrier := H⦈" and "GHK = (G⦇carrier:= (H∩K)⦈)"
  show "H1K⊲GHK"
  proof (intro group.normal_invI[of GHK H1K])
    show "Group.group GHK"
      using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast

  next
    have  H1K_incl:"subgroup H1K (G⦇carrier:= (H∩K)⦈)"
    proof(intro subgroup_incl)
      show "subgroup H1K G"
        using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
    next
      show "subgroup (H∩K) G" using HK_def subgroups_Inter_pair assms by auto
    next
      have "H1 ⊆ (carrier (G⦇carrier:=H⦈))"
        using  assms(3) normal_imp_subgroup subgroup.subset by blast
      also have "... ⊆ H" by simp
      thus "H1K ⊆H∩K"
        using H1K_def calculation by auto
    qed
    thus "subgroup H1K GHK" using GHK_def by simp
  next
    show "⋀ x h. x∈carrier GHK ⟹ h∈H1K ⟹ x ⊗GHK h ⊗GHK invGHK x∈ H1K"
    proof-
      have invHK: "⟦y∈HK⟧ ⟹ invGHK y = invGH y"
        using m_inv_consistent assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
      have multHK : "⟦x∈HK;y∈HK⟧ ⟹  x ⊗(G⦇carrier:=HK⦈) y =  x ⊗ y"
        using HK_def by simp
      fix x assume p: "x∈carrier GHK"
      fix h assume p2 : "h:H1K"
      have "carrier(GHK)⊆HK"
        using GHK_def HK_def by simp
      hence xHK:"x∈HK" using p by auto
      hence invx:"invGHK x = invGH x"
        using invHK assms GHK_def HK_def GH_def m_inv_consistent subgroups_Inter_pair by simp
      have "H1⊆carrier(GH)"
        using assms GH_def normal_imp_subgroup subgroup.subset by blast
      hence hHK:"h∈HK"
        using p2 H1K_def HK_def GH_def by auto
      hence xhx_egal : "x ⊗GHK h ⊗GHK invGHKx =  x ⊗GH h ⊗GH invGH x"
        using invx invHK multHK GHK_def GH_def by auto
      have xH:"x∈carrier(GH)"
        using xHK HK_def GH_def by auto
      have hH:"h∈carrier(GH)"
        using hHK HK_def GH_def by auto
      have  "(∀x∈carrier (GH). ∀h∈H1.  x ⊗GH h ⊗GH invGH x ∈ H1)"
        using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
      hence INCL_1 : "x ⊗GH h ⊗GH invGH x ∈ H1"
        using  xH H1K_def p2 by blast
      have " x ⊗GH h ⊗GH invGH x ∈ HK"
        using assms HK_def subgroups_Inter_pair hHK xHK
        by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
      hence " x ⊗GH h ⊗GH invGH x ∈ K" using HK_def by simp
      hence " x ⊗GH h ⊗GH invGH x ∈ H1K" using INCL_1 H1K_def by auto
      thus  "x ⊗GHK h ⊗GHK invGHK x ∈ H1K" using xhx_egal by simp
    qed
  qed
qed


lemma (in group) normal_inter_subgroup:
  assumes "subgroup H G"
    and "N ⊲ G"
  shows "(N∩H) ⊲ (G⦇carrier := H⦈)"
proof -
  define K where "K = carrier G"
  have "G⦇carrier := K⦈ =  G" using K_def by auto
  moreover have "subgroup K G" using K_def subgroup_self by blast
  moreover have "normal N (G ⦇carrier :=K⦈)" using assms K_def by simp
  ultimately have "N ∩ H ⊲ G⦇carrier := K ∩ H⦈"
    using normal_inter[of K H N] assms(1) by blast
  moreover have "K ∩ H = H" using K_def assms subgroup.subset by blast
  ultimately show "normal (N∩H) (G⦇carrier := H⦈)" by auto
qed


end