Quelle  Group.thy   Sprache: Isabelle

(*  Title:      ZF/ex/Group.thy *)

section ‹Groups›

theory Group imports ZF begin

text‹Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
Markus Wenzel.›


subsection ‹Monoids›

(*First, we must simulate a record declaration:
record monoid =
  carrier :: i
  mult :: "[i,i] \<Rightarrow> i" (infixl "\<cdot>\<index>" 70)
  one :: i ("\<one>\<index>")
*)

definition
  carrier :: "i \ i" where
  "carrier(M) \ fst(M)"

definition
  mmult :: "[i, i, i] \ i" (infixl ‹⋅🍋› 70) where
  "mmult(M,x,y) \ fst(snd(M)) ` \x,y\"

definition
  one :: "i \ i" (‹1🍋›) where
  "one(M) \ fst(snd(snd(M)))"

definition
  update_carrier :: "[i,i] \ i" where
  "update_carrier(M,A) \ "

definition
  m_inv :: "i \ i \ i" (‹inv🍋 _› [81] 80) where
  "inv\<^bsub>G\<^esub> x \ (THE y. y \ carrier(G) \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub> \ x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub>)"

locale monoid = fixes G (structure)
  assumes m_closed [intro, simp]:
         "\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)"
      and m_assoc:
         "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
          ==> (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
      and one_closed [intro, simp]: "\ \ carrier(G)"
      and l_one [simp]: "x \ carrier(G) \ \ \ x = x"
      and r_one [simp]: "x \ carrier(G) \ x \ \ = x"

text‹Simulating the record›
lemma carrier_eq [simp]: "carrier(\A,Z\) = A"
  by (simp add: carrier_def)

lemma mult_eq [simp]: "mmult(, x, y) = M ` \x,y\"
  by (simp add: mmult_def)

lemma one_eq [simp]: "one() = I"
  by (simp add: one_def)

lemma update_carrier_eq [simp]: "update_carrier(\A,Z\,B) = \B,Z\"
  by (simp add: update_carrier_def)

lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
  by (simp add: update_carrier_def)

lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
  by (simp add: update_carrier_def mmult_def)

lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
  by (simp add: update_carrier_def one_def)


lemma (in monoid) inv_unique:
  assumes eq: "y \ x = \"  "x \ y' = \"
    and G: "x \ carrier(G)"  "y \ carrier(G)"  "y' \ carrier(G)"
  shows "y = y'"
proof -
  from G eq have "y = y \ (x \ y')" by simp
  also from G have "... = (y \ x) \ y'" by (simp add: m_assoc)
  also from G eq have "... = y'" by simp
  finally show ?thesis .
qed

text ‹
  A group is a monoid all of whose elements are invertible.
›

locale group = monoid +
  assumes inv_ex:
     "\x. x \ carrier(G) \ \y \ carrier(G). y \ x = \ \ x \ y = \"

lemma (in group) is_group [simp]: "group(G)" by (rule group_axioms)

theorem groupI:
  fixes G (structure)
  assumes m_closed [simp]:
      "\x y. \x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)"
    and one_closed [simp]: "\ \ carrier(G)"
    and m_assoc:
      "\x y z. \x \ carrier(G); y \ carrier(G); z \ carrier(G)\ \
      (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
    and l_one [simp]: "\x. x \ carrier(G) \ \ \ x = x"
    and l_inv_ex: "\x. x \ carrier(G) \ \y \ carrier(G). y \ x = \"
  shows "group(G)"
proof -
  have l_cancel [simp]:
    "\x y z. \x \ carrier(G); y \ carrier(G); z \ carrier(G)\ \
    (x ⋅ y = x ⋅ z) ⟷ (y = z)"
  proof
    fix x y z
    assume G: "x \ carrier(G)"  "y \ carrier(G)"  "z \ carrier(G)"
    {
      assume eq: "x \ y = x \ z"
      with G l_inv_ex obtain x_inv where xG: "x_inv \ carrier(G)"
        and l_inv: "x_inv \ x = \" by fast
      from G eq xG have "(x_inv \ x) \ y = (x_inv \ x) \ z"
        by (simp add: m_assoc)
      with G show "y = z" by (simp add: l_inv)
    next
      assume eq: "y = z"
      with G show "x \ y = x \ z" by simp
    }
  qed
  have r_one:
    "\x. x \ carrier(G) \ x \ \ = x"
  proof -
    fix x
    assume x: "x \ carrier(G)"
    with l_inv_ex obtain x_inv where xG: "x_inv \ carrier(G)"
      and l_inv: "x_inv \ x = \" by fast
    from x xG have "x_inv \ (x \ \) = x_inv \ x"
      by (simp add: m_assoc [symmetric] l_inv)
    with x xG show "x \ \ = x" by simp
  qed
  have inv_ex:
    "\x. x \ carrier(G) \ \y \ carrier(G). y \ x = \ \ x \ y = \"
  proof -
    fix x
    assume x: "x \ carrier(G)"
    with l_inv_ex obtain y where y: "y \ carrier(G)"
      and l_inv: "y \ x = \" by fast
    from x y have "y \ (x \ y) = y \ \"
      by (simp add: m_assoc [symmetric] l_inv r_one)
    with x y have r_inv: "x \ y = \"
      by simp
    from x y show "\y \ carrier(G). y \ x = \ \ x \ y = \"
      by (fast intro: l_inv r_inv)
  qed
  show ?thesis
    by (blast intro: group.intro monoid.intro group_axioms.intro
                     assms r_one inv_ex)
qed

lemma (in group) inv [simp]:
  "x \ carrier(G) \ inv x \ carrier(G) \ inv x \ x = \ \ x \ inv x = \"
  apply (frule inv_ex)
    unfolding Bex_def m_inv_def
  apply (erule exE)
  apply (rule theI)
  apply (rule ex1I, assumption)
   apply (blast intro: inv_unique)
  done

lemma (in group) inv_closed [intro!]:
  "x \ carrier(G) \ inv x \ carrier(G)"
  by simp

lemma (in group) l_inv:
  "x \ carrier(G) \ inv x \ x = \"
  by simp

lemma (in group) r_inv:
  "x \ carrier(G) \ x \ inv x = \"
  by simp


subsection ‹Cancellation Laws and Basic Properties›

lemma (in group) l_cancel [simp]:
  assumes "x \ carrier(G)" "y \ carrier(G)" "z \ carrier(G)"
  shows "(x \ y = x \ z) \ (y = z)"
proof
  assume eq: "x \ y = x \ z"
  hence  "(inv x \ x) \ y = (inv x \ x) \ z"
    by (simp only: m_assoc inv_closed assms)
  thus "y = z" by (simp add: assms)
next
  assume eq: "y = z"
  then show "x \ y = x \ z" by simp
qed

lemma (in group) r_cancel [simp]:
  assumes "x \ carrier(G)" "y \ carrier(G)" "z \ carrier(G)"
  shows "(y \ x = z \ x) \ (y = z)"
proof
  assume eq: "y \ x = z \ x"
  then have "y \ (x \ inv x) = z \ (x \ inv x)"
    by (simp only: m_assoc [symmetric] inv_closed assms)
  thus "y = z" by (simp add: assms)
next
  assume eq: "y = z"
  thus  "y \ x = z \ x" by simp
qed

lemma (in group) inv_comm:
  assumes "x \ y = \"
      and G: "x \ carrier(G)"  "y \ carrier(G)"
  shows "y \ x = \"
proof -
  from G have "x \ y \ x = x \ \" by (auto simp add: assms)
  with G show ?thesis by (simp del: r_one add: m_assoc)
qed

lemma (in group) inv_equality:
     "\y \ x = \; x \ carrier(G); y \ carrier(G)\ \ inv x = y"
apply (simp add: m_inv_def)
apply (rule the_equality)
 apply (simp add: inv_comm [of y x])
apply (rule r_cancel [THEN iffD1], auto)
done

lemma (in group) inv_one [simp]:
  "inv \ = \"
  by (auto intro: inv_equality)

lemma (in group) inv_inv [simp]: "x \ carrier(G) \ inv (inv x) = x"
  by (auto intro: inv_equality)

text‹This proof is by cancellation›
lemma (in group) inv_mult_group:
  "\x \ carrier(G); y \ carrier(G)\ \ inv (x \ y) = inv y \ inv x"
proof -
  assume G: "x \ carrier(G)"  "y \ carrier(G)"
  then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)"
    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
  with G show ?thesis by (simp_all del: inv add: inv_closed)
qed


subsection ‹Substructures›

locale subgroup = fixes H and G (structure)
  assumes subset: "H \ carrier(G)"
    and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H"
    and  one_closed [simp]: "\ \ H"
    and m_inv_closed [intro,simp]: "x \ H \ inv x \ H"


lemma (in subgroup) mem_carrier [simp]:
  "x \ H \ x \ carrier(G)"
  using subset by blast


lemma subgroup_imp_subset:
  "subgroup(H,G) \ H \ carrier(G)"
  by (rule subgroup.subset)

lemma (in subgroup) group_axiomsI [intro]:
  assumes "group(G)"
  shows "group_axioms (update_carrier(G,H))"
proof -
  interpret group G by fact
  show ?thesis by (force intro: group_axioms.intro l_inv r_inv)
qed

lemma (in subgroup) is_group [intro]:
  assumes "group(G)"
  shows "group (update_carrier(G,H))"
proof -
  interpret group G by fact
  show ?thesis
  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
qed

text ‹
  Since 🍋‹H› is nonempty, it contains some element 🍋‹x›.  Since
  it is closed under inverse, it contains ‹inv x›.  Since
  it is closed under product, it contains ‹x ⋅ inv x = 1›.
›

text ‹
  Since 🍋‹H› is nonempty, it contains some element 🍋‹x›.  Since
  it is closed under inverse, it contains ‹inv x›.  Since
  it is closed under product, it contains ‹x ⋅ inv x = 1›.
›

lemma (in group) one_in_subset:
  "\H \ carrier(G); H \ 0; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H\
   ==> 1 ∈ H"
by (force simp add: l_inv)

text ‹A characterization of subgroups: closed, non-empty subset.›

declare monoid.one_closed [simp] group.inv_closed [simp]
  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]

lemma subgroup_nonempty:
  "\ subgroup(0,G)"
  by (blast dest: subgroup.one_closed)


subsection ‹Direct Products›

definition
  DirProdGroup :: "[i,i] \ i"  (infixr ‹⨂› 80) where
  "G \ H \ carrier(H),
              (λ<⟨g,h⟩, <g', h'>>
                   ∈ (carrier(G) × carrier(H)) × (carrier(G) × carrier(H)).
                <g ⋅🚫G🚫 g', h \\<^bsub>H\<^esub> h'>),
              <1🚫G🚫, 1🚫H🚫>, 0>"

lemma DirProdGroup_group:
  assumes "group(G)" and "group(H)"
  shows "group (G \ H)"
proof -
  interpret G: group G by fact
  interpret H: group H by fact
  show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
          simp add: DirProdGroup_def)
qed

lemma carrier_DirProdGroup [simp]:
     "carrier (G \ H) = carrier(G) \ carrier(H)"
  by (simp add: DirProdGroup_def)

lemma one_DirProdGroup [simp]:
     "\\<^bsub>G \ H\<^esub> = <\\<^bsub>G\<^esub>, \\<^bsub>H\<^esub>>"
  by (simp add: DirProdGroup_def)

lemma mult_DirProdGroup [simp]:
     "\g \ carrier(G); h \ carrier(H); g' \ carrier(G); h' \ carrier(H)\
      ==> ⟨g, h⟩ ⋅🚫G ⨂ H🚫 <g', h'> = <g ⋅🚫G🚫 g', h \\<^bsub>H\<^esub> h'>"
  by (simp add: DirProdGroup_def)

lemma inv_DirProdGroup [simp]:
  assumes "group(G)" and "group(H)"
  assumes g: "g \ carrier(G)"
      and h: "h \ carrier(H)"
  shows "inv \<^bsub>G \ H\<^esub> \g, h\ = G\<^esub> g, inv\<^bsub>H\<^esub> h>"
  apply (rule group.inv_equality [OF DirProdGroup_group])
  apply (simp_all add: assms group.l_inv)
  done

subsection ‹Isomorphisms›

definition
  hom :: "[i,i] \ i" where
  "hom(G,H) \
    {h ∈ carrier(G) -> carrier(H).
      (∀x ∈ carrier(G). ∀y ∈ carrier(G). h ` (x ⋅🚫G🚫 y) = (h ` x) ⋅🚫H🚫 (h ` y))}"

lemma hom_mult:
  "\h \ hom(G,H); x \ carrier(G); y \ carrier(G)\
   ==> h ` (x ⋅🚫G🚫 y) = h ` x ⋅🚫H🚫 h ` y"
  by (simp add: hom_def)

lemma hom_closed:
  "\h \ hom(G,H); x \ carrier(G)\ \ h ` x \ carrier(H)"
  by (auto simp add: hom_def)

lemma (in group) hom_compose:
     "\h \ hom(G,H); i \ hom(H,I)\ \ i O h \ hom(G,I)"
by (force simp add: hom_def comp_fun)

lemma hom_is_fun:
  "h \ hom(G,H) \ h \ carrier(G) -> carrier(H)"
  by (simp add: hom_def)


subsection ‹Isomorphisms›

definition
  iso :: "[i,i] \ i"  (infixr ‹≅› 60) where
  "G \ H \ hom(G,H) \ bij(carrier(G), carrier(H))"

lemma (in group) iso_refl: "id(carrier(G)) \ G \ G"
  by (simp add: iso_def hom_def id_type id_bij)


lemma (in group) iso_sym:
     "h \ G \ H \ converse(h) \ H \ G"
apply (simp add: iso_def bij_converse_bij, clarify)
apply (subgoal_tac "converse(h) \ carrier(H) \ carrier(G)")
 prefer 2 apply (simp add: bij_converse_bij bij_is_fun)
apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"]
            simp add: hom_def bij_is_inj right_inverse_bij)
done

lemma (in group) iso_trans:
     "\h \ G \ H; i \ H \ I\ \ i O h \ G \ I"
  by (auto simp add: iso_def hom_compose comp_bij)

lemma DirProdGroup_commute_iso:
  assumes "group(G)" and "group(H)"
  shows "(\\x,y\ \ carrier(G \ H). \y,x\) \ (G \ H) \ (H \ G)"
proof -
  interpret group G by fact
  interpret group H by fact
  show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
qed

lemma DirProdGroup_assoc_iso:
  assumes "group(G)" and "group(H)" and "group(I)"
  shows "(\<\x,y\,z> \ carrier((G \ H) \ I). y,z\>)
          ∈ ((G ⨂ H) ⨂ I) ≅ (G ⨂ (H ⨂ I))"
proof -
  interpret group G by fact
  interpret group H by fact
  interpret group I by fact
  show ?thesis
    by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
qed

text‹Basis for homomorphism proofs: we assume two groups 🍋‹G› and
  🍋‹H›, with a homomorphism 🍋‹h› between them›
locale group_hom = G: group G + H: group H
  for G (structure) and H (structure) and h +
  assumes homh: "h \ hom(G,H)"
  notes hom_mult [simp] = hom_mult [OF homh]
    and hom_closed [simp] = hom_closed [OF homh]
    and hom_is_fun [simp] = hom_is_fun [OF homh]

lemma (in group_hom) one_closed [simp]:
  "h ` \ \ carrier(H)"
  by simp

lemma (in group_hom) hom_one [simp]:
  "h ` \ = \\<^bsub>H\<^esub>"
proof -
  have "h ` \ \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = (h ` \) \\<^bsub>H\<^esub> (h ` \)"
    by (simp add: hom_mult [symmetric] del: hom_mult)
  then show ?thesis by (simp del: H.r_one)
qed

lemma (in group_hom) inv_closed [simp]:
  "x \ carrier(G) \ h ` (inv x) \ carrier(H)"
  by simp

lemma (in group_hom) hom_inv [simp]:
  "x \ carrier(G) \ h ` (inv x) = inv\<^bsub>H\<^esub> (h ` x)"
proof -
  assume x: "x \ carrier(G)"
  then have "h ` x \\<^bsub>H\<^esub> h ` (inv x) = \\<^bsub>H\<^esub>"
    by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
  also from x have "... = h ` x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
    by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
  finally have "h ` x \\<^bsub>H\<^esub> h ` (inv x) = h ` x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
  with x show ?thesis by (simp del: H.inv)
qed

subsection ‹Commutative Structures›

text ‹
  Naming convention: multiplicative structures that are commutative
  are called \emph{commutative}, additive structures are called
  \emph{Abelian}.
›

subsection ‹Definition›

locale comm_monoid = monoid +
  assumes m_comm: "\x \ carrier(G); y \ carrier(G)\ \ x \ y = y \ x"

lemma (in comm_monoid) m_lcomm:
  "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\ \
   x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
proof -
  assume xyz: "x \ carrier(G)"  "y \ carrier(G)"  "z \ carrier(G)"
  from xyz have "x \ (y \ z) = (x \ y) \ z" by (simp add: m_assoc)
  also from xyz have "... = (y \ x) \ z" by (simp add: m_comm)
  also from xyz have "... = y \ (x \ z)" by (simp add: m_assoc)
  finally show ?thesis .
qed

lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm

locale comm_group = comm_monoid + group

lemma (in comm_group) inv_mult:
  "\x \ carrier(G); y \ carrier(G)\ \ inv (x \ y) = inv x \ inv y"
  by (simp add: m_ac inv_mult_group)


lemma (in group) subgroup_self: "subgroup (carrier(G),G)"
by (simp add: subgroup_def)

lemma (in group) subgroup_imp_group:
  "subgroup(H,G) \ group (update_carrier(G,H))"
by (simp add: subgroup.is_group)

lemma (in group) subgroupI:
  assumes subset: "H \ carrier(G)" and non_empty: "H \ 0"
    and "\a. a \ H \ inv a \ H"
    and "\a b. \a \ H; b \ H\ \ a \ b \ H"
  shows "subgroup(H,G)"
proof (simp add: subgroup_def assms)
  show "\ \ H"
    by (rule one_in_subset) (auto simp only: assms)
qed


subsection ‹Bijections of a Set, Permutation Groups, Automorphism Groups›

definition
  BijGroup :: "i\i" where
  "BijGroup(S) \
    <bij(S,S),
     λ⟨g,f⟩ ∈ bij(S,S) × bij(S,S). g O f,
     id(S), 0>"


subsection ‹Bijections Form a Group›

theorem group_BijGroup: "group(BijGroup(S))"
apply (simp add: BijGroup_def)
apply (rule groupI)
    apply (simp_all add: id_bij comp_bij comp_assoc)
 apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel)
apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij)
done


subsection‹Automorphisms Form a Group›

lemma Bij_Inv_mem: "\f \ bij(S,S); x \ S\ \ converse(f) ` x \ S"
by (blast intro: apply_funtype bij_is_fun bij_converse_bij)

lemma inv_BijGroup: "f \ bij(S,S) \ m_inv (BijGroup(S), f) = converse(f)"
apply (rule group.inv_equality)
apply (rule group_BijGroup)
apply (simp_all add: BijGroup_def bij_converse_bij
          left_comp_inverse [OF bij_is_inj])
done

lemma iso_is_bij: "h \ G \ H \ h \ bij(carrier(G), carrier(H))"
by (simp add: iso_def)


definition
  auto :: "i\i" where
  "auto(G) \ iso(G,G)"

definition
  AutoGroup :: "i\i" where
  "AutoGroup(G) \ update_carrier(BijGroup(carrier(G)), auto(G))"


lemma (in group) id_in_auto: "id(carrier(G)) \ auto(G)"
  by (simp add: iso_refl auto_def)

lemma (in group) subgroup_auto:
      "subgroup (auto(G)) (BijGroup (carrier(G)))"
proof (rule subgroup.intro)
  show "auto(G) \ carrier (BijGroup (carrier(G)))"
    by (auto simp add: auto_def BijGroup_def iso_def)
next
  fix x y
  assume "x \ auto(G)" "y \ auto(G)"
  thus "x \\<^bsub>BijGroup (carrier(G))\<^esub> y \ auto(G)"
    by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun
                       group.hom_compose comp_bij)
next
  show "\\<^bsub>BijGroup (carrier(G))\<^esub> \ auto(G)" by (simp add:  BijGroup_def id_in_auto)
next
  fix x
  assume "x \ auto(G)"
  thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \ auto(G)"
    by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym)
qed

theorem (in group) AutoGroup: "group (AutoGroup(G))"
by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)



subsection‹Cosets and Quotient Groups›

definition
  r_coset  :: "[i,i,i] \ i"  (infixl ‹#>🍋› 60) where
  "H #>\<^bsub>G\<^esub> a \ \h\H. {h \\<^bsub>G\<^esub> a}"

definition
  l_coset  :: "[i,i,i] \ i"  (infixl ‹<#🍋› 60) where
  "a <#\<^bsub>G\<^esub> H \ \h\H. {a \\<^bsub>G\<^esub> h}"

definition
  RCOSETS  :: "[i,i] \ i"  (‹rcosets🍋 _› [81] 80) where
  "rcosets\<^bsub>G\<^esub> H \ \a\carrier(G). {H #>\<^bsub>G\<^esub> a}"

definition
  set_mult :: "[i,i,i] \ i"  (infixl ‹<#>🍋› 60) where
  "H <#>\<^bsub>G\<^esub> K \ \h\H. \k\K. {h \\<^bsub>G\<^esub> k}"

definition
  SET_INV  :: "[i,i] \ i"  (‹set'_inv\ _\ [81] 80) where
  "set_inv\<^bsub>G\<^esub> H \ \h\H. {inv\<^bsub>G\<^esub> h}"


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

notation
  normal  (infixl ‹⊲› 60)


subsection ‹Basic Properties of Cosets›

lemma (in group) coset_mult_assoc:
     "\M \ carrier(G); g \ carrier(G); h \ carrier(G)\
      ==> (M #> g) #> h = M #> (g ⋅ h)"
by (force simp add: r_coset_def m_assoc)

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

lemma (in group) solve_equation:
    "\subgroup(H,G); x \ H; y \ H\ \ \h\H. y = h \ x"
apply (rule bexI [of _ "y \ (inv x)"])
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
                      subgroup.subset [THEN subsetD])
done

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

lemma (in group) coset_join2:
     "\x \ carrier(G); subgroup(H,G); x\H\ \ H #> x = H"
  🍋 ‹Alternative proof is to put 🍋‹x=1› in ‹repr_independence›.›
by (force simp add: subgroup.m_closed r_coset_def solve_equation)

lemma (in group) 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)


text‹Really needed?›
lemma (in group) transpose_inv:
     "\x \ y = z; x \ carrier(G); y \ carrier(G); z \ carrier(G)\
      ==> (inv x) ⋅ z = y"
by (force simp add: m_assoc [symmetric])



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)

lemma (in normal) inv_op_closed1:
     "\x \ carrier(G); h \ H\ \ (inv x) \ h \ x \ H"
apply (insert coset_eq)
apply (auto simp add: l_coset_def r_coset_def)
apply (drule bspec, assumption)
apply (drule equalityD1 [THEN subsetD], blast, clarify)
apply (simp add: m_assoc)
apply (simp add: m_assoc [symmetric])
done

lemma (in normal) inv_op_closed2:
     "\x \ carrier(G); h \ H\ \ x \ h \ (inv x) \ H"
apply (subgoal_tac "inv (inv x) \ h \ (inv x) \ H")
apply simp
apply (blast intro: inv_op_closed1)
done

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 (rule UN_I)
          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 (rule UN_I)
          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


subsection‹More Properties of Cosets›

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_swap:
     "\y \ x <# H; x \ carrier(G); subgroup(H,G)\ \ x \ y <# H"
proof (simp add: l_coset_def)
  assume "\h\H. y = x \ h"
    and x: "x \ carrier(G)"
    and sb: "subgroup(H,G)"
  then obtain h' where h': "h' \ H \ x \ h' = y" by blast
  show "\h\H. x = y \ h"
  proof
    show "x = y \ inv h'" using h' x sb
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
    show "inv h' \ H" using h' sb
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
  qed
qed

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_repr_imp_subset:
  assumes y: "y \ x <# H" and x: "x \ carrier(G)" and sb: "subgroup(H,G)"
  shows "y <# H \ x <# H"
proof -
  from y
  obtain h' where "h' ∈ H" "x ⋅ h' = y" by (auto simp add: l_coset_def)
  thus ?thesis using x sb
    by (auto simp add: l_coset_def m_assoc
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
qed

lemma (in group) l_repr_independence:
  assumes y: "y \ x <# H" and x: "x \ carrier(G)" and sb: "subgroup(H,G)"
  shows "x <# H = y <# H"
proof
  show "x <# H \ y <# H"
    by (rule l_repr_imp_subset,
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
  show "y <# H \ x <# H" by (rule l_repr_imp_subset [OF y x sb])
qed

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

lemma (in group) subgroup_mult_id: "subgroup(H,G) \ H <#> H = H"
apply (rule equalityI)
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\"])
apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
done


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 intro!: equalityI)
  fix h
  assume h: "h \ H"
  {
    show "inv x \ inv h \ (\j\H. {j \ inv x})"
    proof (rule UN_I)
      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
  next
    show "h \ inv x \ (\j\H. {inv x \ inv j})"
    proof (rule UN_I)
      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"
by (force simp add: r_coset_def set_mult_def m_assoc)

lemma (in group) rcos_assoc_lcos:
     "\H \ carrier(G); K \ carrier(G); x \ carrier(G)\
      ==> (H #> x) <#> K = H <#> (x <# K)"
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)

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 subset
              r_coset_subset_G 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 subset normal_axioms 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‹Two distinct right cosets are disjoint›

definition
  r_congruent :: "[i,i] \ i" (‹rcong🍋 _› [60] 60) where
  "rcong\<^bsub>G\<^esub> H \ {\x,y\ \ carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ H}"


lemma (in subgroup) equiv_rcong:
   assumes "group(G)"
   shows "equiv (carrier(G), rcong H)"
proof -
  interpret group G by fact
  show ?thesis proof (simp add: equiv_def, intro conjI)
    show "rcong H \ carrier(G) \ carrier(G)"
      by (auto simp add: r_congruent_def)
  next
    show "refl (carrier(G), rcong H)"
      by (auto simp add: r_congruent_def refl_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: 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.›
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
      Collect_image_eq)
qed

lemma (in group) rcos_equation:
  assumes "subgroup(H, G)"
  shows
     "\ha \ a = h \ b; a \ carrier(G); b \ carrier(G);
        h ∈ H;  ha ∈ H;  hb ∈ H]
      ==> hb ⋅ a ∈ (∪h∈H. {h ⋅ b})" (is "PROP ?P")
proof -
  interpret subgroup H G by fact
  show "PROP ?P"
    apply (rule UN_I [of "hb \ ((inv ha) \ h)"], simp)
    apply (simp add: m_assoc transpose_inv)
    done
qed

lemma (in group) rcos_disjoint:
  assumes "subgroup(H, G)"
  shows "\a \ rcosets H; b \ rcosets H; a\b\ \ a \ b = 0" (is "PROP ?P")
proof -
  interpret subgroup H G by fact
  show "PROP ?P"
    apply (simp add: RCOSETS_def r_coset_def)
    apply (blast intro: rcos_equation assms sym)
    done
qed


subsection ‹Order of a Group and Lagrange's Theorem\

definition
  order :: "i \ i" where
  "order(S) \ |carrier(S)|"

lemma (in group) rcos_self:
  assumes "subgroup(H, G)"
  shows "x \ carrier(G) \ x \ H #> x" (is "PROP ?P")
proof -
  interpret subgroup H G by fact
  show "PROP ?P"
    apply (simp add: r_coset_def)
    apply (rule_tac x="\" in bexI) apply (auto)
    done
qed

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 subset_Finite])
done

text‹More general than the HOL version, which also requires 🍋‹G› to
      be finite.›
lemma (in group) card_cosets_equal:
  assumes H:   "H \ carrier(G)"
  shows "c \ rcosets H \ |c| = |H|"
proof (simp add: RCOSETS_def, clarify)
  fix a
  assume a: "a \ carrier(G)"
  show "|H #> a| = |H|"
  proof (rule eqpollI [THEN cardinal_cong])
    show "H #> a \ H"
    proof (simp add: lepoll_def, intro exI)
      show "(\y \ H#>a. y \ inv a) \ inj(H #> a, H)"
        by (auto intro: lam_type
                 simp add: inj_def r_coset_def m_assoc subsetD [OF H] a)
    qed
    show "H \ H #> a"
    proof (simp add: lepoll_def, intro exI)
      show "(\y\ H. y \ a) \ inj(H, H #> a)"
        by (auto intro: lam_type
                 simp add: inj_def r_coset_def  subsetD [OF H] a)
    qed
  qed
qed


lemma (in group) rcosets_subset_PowG:
     "subgroup(H,G) \ rcosets H \ Pow(carrier(G))"
apply (simp add: RCOSETS_def)
apply (blast dest: r_coset_subset_G subgroup.subset)
done

theorem (in group) lagrange:
     "\Finite(carrier(G)); subgroup(H,G)\
      ==> |rcosets H| #* |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 subset_Finite])
  apply (simp add: rcosets_part_G)
 apply (simp add: card_cosets_equal [OF subgroup.subset])
apply (simp add: rcos_disjoint)
done


subsection ‹Quotient Groups: Factorization of a Group›

definition
  FactGroup :: "[i,i] \ i" (infixl ‹Mod› 65) where
    🍋 ‹Actually defined for groups rather than monoids›
  "G Mod H \
     <rcosets🚫G🚫 H, λ⟨K1,K2⟩ ∈ (rcosets🚫G🚫 H) × (rcosets🚫G🚫 H). K1 <#>🚫G🚫 K2, H, 0>"

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 (auto simp add: RCOSETS_def rcos_sum m_assoc)

lemma (in subgroup) subgroup_in_rcosets:
  assumes "group(G)"
  shows "H \ rcosets H"
proof -
  interpret group G by fact
  have "H #> \ = H"
    using _ subgroup_axioms by (rule coset_join2) simp_all
  then show ?thesis
    by (auto simp add: RCOSETS_def intro: sym)
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)
  apply (simp add: 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 (in normal) inv_FactGroup:
     "X \ carrier (G Mod H) \ inv\<^bsub>G Mod H\<^esub> X = set_inv X"
apply (rule group.inv_equality [OF factorgroup_is_group])
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
done

text‹The coset map is a homomorphism from 🍋‹G› to the quotient group
  🍋‹G Mod H››
lemma (in normal) r_coset_hom_Mod:
  "(\a \ carrier(G). H #> a) \ hom(G, G Mod H)"
by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type)


subsection‹The First Isomorphism Theorem›

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

definition
  kernel :: "[i,i,i] \ i" where
    🍋 ‹the kernel of a homomorphism›
  "kernel(G,H,h) \ {x \ carrier(G). h ` x = \\<^bsub>H\<^esub>}"

lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
apply (rule subgroup.intro)
apply (auto simp add: kernel_def group.intro)
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: group.normal_inv_iff subgroup_kernel group.intro)
apply (simp add: kernel_def)
done

lemma (in group_hom) FactGroup_nonempty:
  assumes X: "X \ carrier (G Mod kernel(G,H,h))"
  shows "X \ 0"
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_contents_mem:
  assumes X: "X \ carrier (G Mod (kernel(G,H,h)))"
  shows "contents (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 image_UN
                       image_eq_UN [OF hom_is_fun] g)
  thus ?thesis by (auto simp add: g)
qed

lemma mult_FactGroup:
     "\X \ carrier(G Mod H); X' \ carrier(G Mod H)\
      ==> X ⋅🚫(G Mod H)🚫 X' = X <#>\<^bsub>G\<^esub> X'"
by (simp add: FactGroup_def)

lemma (in normal) FactGroup_m_closed:
     "\X \ carrier(G Mod H); X' \ carrier(G Mod H)\
      ==> X <#>🚫G🚫 X' \ carrier(G Mod H)"
by (simp add: FactGroup_def setmult_closed)

lemma (in group_hom) FactGroup_hom:
     "(\X \ carrier(G Mod (kernel(G,H,h))). contents (h``X))
      ∈ hom (G Mod (kernel(G,H,h)), H)"
proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], 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 \\<^bsub>H\<^esub> h ` g'}" using X X'
    by (auto dest!: FactGroup_nonempty
             simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN
                       subsetD [OF Xsub] subsetD [OF X'sub])
  thus "contents (h `` (X <#> X')) = contents (h `` X) \\<^bsub>H\<^esub> contents (h `` X')"
    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty
                  X X' Xsub X'sub)
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 image_def)
apply (rename_tac y)
apply (rule_tac x="y \ g \ inv g'" in bexI)
apply (simp_all add: G.m_assoc)
done

lemma (in group_hom) FactGroup_inj:
     "(\X\carrier (G Mod kernel(G,H,h)). contents (h `` X))
      ∈ inj(carrier (G Mod kernel(G,H,h)), carrier(H))"
proof (simp add: inj_def FactGroup_contents_mem lam_type, 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'"
    and Xsub: "X \ carrier(G)" and X'sub: "X' ⊆ carrier(G)"
    by (force simp add: kernel_def r_coset_def image_def)+
  assume "contents (h `` X) = contents (h `` X')"
  hence h: "h ` g = h ` g'"
    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty
                  X X' Xsub X'sub)
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
qed


lemma (in group_hom) kernel_rcoset_subset:
  assumes g: "g \ carrier(G)"
  shows "kernel(G,H,h) #> g \ carrier (G)"
    by (auto simp add: g kernel_def r_coset_def)



text‹If the homomorphism 🍋‹h› is onto 🍋‹H›, then so is the
homomorphism from the quotient group›
lemma (in group_hom) FactGroup_surj:
  assumes h: "h \ surj(carrier(G), carrier(H))"
  shows "(\X\carrier (G Mod kernel(G,H,h)). contents (h `` X))
         ∈ surj(carrier (G Mod kernel(G,H,h)), carrier(H))"
proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify)
  fix y
  assume y: "y \ carrier(H)"
  with h obtain g where g: "g \ carrier(G)" "h ` g = y"
    by (auto simp add: surj_def)
  hence "(\x\kernel(G,H,h) #> g. {h ` x}) = {y}"
    by (auto simp add: y kernel_def r_coset_def)
  with g show "\x\carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
        🍋 ‹The witness is 🍋‹kernel(G,H,h) #> g››
    by (force simp add: FactGroup_def RCOSETS_def
           image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
qed


text‹If 🍋‹h› is a homomorphism from 🍋‹G› onto 🍋‹H›, then the
 quotient group 🍋‹G Mod (kernel(G,H,h))› is isomorphic to 🍋‹H›.›
theorem (in group_hom) FactGroup_iso:
  "h \ surj(carrier(G), carrier(H))
   ==> (λX∈carrier (G Mod kernel(G,H,h)). contents (h``X)) ∈ (G Mod (kernel(G,H,h))) ≅ H"
by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)

end