# Theory Group

theory Group
imports ZF
(*  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] => i" (infixl "⋅ı" 70)
one :: i ("𝟭ı")
*)

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" ("𝟭ı") where
"one(M) == fst(snd(snd(M)))"

definition
update_carrier :: "[i,i] => i" where
"update_carrier(M,A) == <A,snd(M)>"

definition
m_inv :: "i => i => i" ("invı _" [81] 80) where
"inv⇘G⇙ x == (THE y. y ∈ carrier(G) & y ⋅⇘G⇙ x = 𝟭⇘G⇙ & x ⋅⇘G⇙ y = 𝟭⇘G⇙)"

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"

lemma mult_eq [simp]: "mmult(<A,M,Z>, x, y) = M  <x,y>"

lemma one_eq [simp]: "one(<A,M,I,Z>) = I"

lemma update_carrier_eq [simp]: "update_carrier(<A,Z>,B) = <B,Z>"

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

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

lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"

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"
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)
apply (unfold 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 (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)"
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 @{term H} is nonempty, it contains some element @{term x}.  Since
it is closed under inverse, it contains ‹inv x›.  Since
it is closed under product, it contains ‹x ⋅ inv x = 𝟭›.
›

text ‹
Since @{term H} is nonempty, it contains some element @{term x}.  Since
it is closed under inverse, it contains ‹inv x›.  Since
it is closed under product, it contains ‹x ⋅ inv x = 𝟭›.
›

lemma (in group) one_in_subset:
"⟦H ⊆ carrier(G); H ≠ 0; ∀a ∈ H. inv a ∈ H; ∀a∈H. ∀b∈H. a ⋅ b ∈ H⟧
⟹ 𝟭 ∈ H"

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(G) × carrier(H),
(λ<<g,h>, <g', h'>>
∈ (carrier(G) × carrier(H)) × (carrier(G) × carrier(H)).
<g ⋅⇘G⇙ g', h ⋅⇘H⇙ h'>),
<𝟭⇘G⇙, 𝟭⇘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
qed

lemma carrier_DirProdGroup [simp]:
"carrier (G ⨂ H) = carrier(G) × carrier(H)"

lemma one_DirProdGroup [simp]:
"𝟭⇘G ⨂ H⇙ = <𝟭⇘G⇙, 𝟭⇘H⇙>"

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 ⋅⇘H⇙ h'>"

lemma inv_DirProdGroup [simp]:
assumes "group(G)" and "group(H)"
assumes g: "g ∈ carrier(G)"
and h: "h ∈ carrier(H)"
shows "inv ⇘G ⨂ H⇙ <g, h> = <inv⇘G⇙ g, inv⇘H⇙ h>"
apply (rule group.inv_equality [OF DirProdGroup_group])
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"

lemma hom_closed:
"⟦h ∈ hom(G,H); x ∈ carrier(G)⟧ ⟹ h  x ∈ carrier(H)"

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)"

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)"]
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). <x,<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 @{term G} and
@{term H}, with a homomorphism @{term 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  𝟭 = 𝟭⇘H⇙"
proof -
have "h  𝟭 ⋅⇘H⇙ 𝟭⇘H⇙ = (h  𝟭) ⋅⇘H⇙ (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⇘H⇙ (h  x)"
proof -
assume x: "x ∈ carrier(G)"
then have "h  x ⋅⇘H⇙ h  (inv x) = 𝟭⇘H⇙"
by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
also from x have "... = h  x ⋅⇘H⇙ inv⇘H⇙ (h  x)"
by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
finally have "h  x ⋅⇘H⇙ h  (inv x) = h  x ⋅⇘H⇙ inv⇘H⇙ (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"

lemma (in group) subgroup_self: "subgroup (carrier(G),G)"

lemma (in group) subgroup_imp_group:
"subgroup(H,G) ⟹ group (update_carrier(G,H))"

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)"
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 (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)
left_comp_inverse [OF bij_is_inj])
done

lemma iso_is_bij: "h ∈ G ≅ H ==> h ∈ bij(carrier(G), carrier(H))"

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)"

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 ⋅⇘BijGroup (carrier(G))⇙ y ∈ auto(G)"
by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun
group.hom_compose comp_bij)
next
show "𝟭⇘BijGroup (carrier(G))⇙ ∈ auto(G)" by (simp add:  BijGroup_def id_in_auto)
next
fix x
assume "x ∈ auto(G)"
thus "inv⇘BijGroup (carrier(G))⇙ 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 #>⇘G⇙ a == ⋃h∈H. {h ⋅⇘G⇙ a}"

definition
l_coset  :: "[i,i,i] => i"  (infixl "<#ı" 60) where
"a <#⇘G⇙ H == ⋃h∈H. {a ⋅⇘G⇙ h}"

definition
RCOSETS  :: "[i,i] => i"  ("rcosetsı _" [81] 80) where
"rcosets⇘G⇙ H == ⋃a∈carrier(G). {H #>⇘G⇙ a}"

definition
set_mult :: "[i,i,i] => i"  (infixl "<#>ı" 60) where
"H <#>⇘G⇙ K == ⋃h∈H. ⋃k∈K. {h ⋅⇘G⇙ k}"

definition
SET_INV  :: "[i,i] => i"  ("set'_invı _" [81] 80) where
"set_inv⇘G⇙ H == ⋃h∈H. {inv⇘G⇙ 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"

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 @{term "x=𝟭"} 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)"

lemma (in group) rcosI:
"⟦h ∈ H; H ⊆ carrier(G); x ∈ carrier(G)⟧ ⟹ h ⋅ x ∈ H #> x"

lemma (in group) rcosetsI:
"⟦H ⊆ carrier(G); x ∈ carrier(G)⟧ ⟹ H #> x ∈ rcosets H"

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)"

lemma (in group) normalI:
"subgroup(H,G) ⟹ (∀x ∈ carrier(G). H #> x = x <# H) ⟹ H ⊲ G"

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)
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"
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"
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)"
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⇘G⇙ H == {<x,y> ∈ carrier(G) * carrier(G). inv⇘G⇙ 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 (simp add: equiv_def, intro conjI)
show "rcong H ⊆ carrier(G) × carrier(G)"
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)
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 (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 (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 (simp add: r_coset_subset_G [THEN subset_Finite])
done

text‹More general than the HOL version, which also requires @{term G} to
be finite.›
lemma (in group) card_cosets_equal:
assumes H:   "H ⊆ carrier(G)"
shows "c ∈ rcosets H ⟹ |c| = |H|"
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 (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: card_cosets_equal [OF subgroup.subset])
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 (rule groupI)
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⇘G 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 ∈ 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 = 𝟭⇘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)
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)
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 (hX) ∈ 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 <#>⇘G⇙ X'"

lemma (in normal) FactGroup_m_closed:
"[|X ∈ carrier(G Mod H); X' ∈ carrier(G Mod H)|]
==> X <#>⇘G⇙ X' ∈ carrier(G Mod H)"

lemma (in group_hom) FactGroup_hom:
"(λX ∈ carrier(G Mod (kernel(G,H,h))). contents (hX))
∈ 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 ⋅⇘H⇙ 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) ⋅⇘H⇙ 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)
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 @{term h} is onto @{term 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"
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 @{term "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 @{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:
"h ∈ surj(carrier(G), carrier(H))
⟹ (λX∈carrier (G Mod kernel(G,H,h)). contents (hX)) ∈ (G Mod (kernel(G,H,h))) ≅ H"
by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)

end