# Theory Coset

theory Coset
imports Group
```(*  Title:      HOL/Algebra/Coset.thy
Author:     Florian Kammueller
Author:     L C Paulson
Author:     Stephan Hohe
*)

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 "rcosets⇘G⇙ 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_inv⇘G⇙ H = (⋃h∈H. {inv⇘G⇙ 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"

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) coset_mult_inv1:
"[| M #> (x ⊗ (inv y)) = M;  x ∈ carrier G ; y ∈ carrier G;
M ⊆ carrier G |] ==> M #> x = M #> y"
apply (erule subst [of concl: "%z. M #> x = z #> y"])
done

lemma (in group) coset_mult_inv2:
"[| M #> x = M #> y;  x ∈ carrier G;  y ∈ carrier G;  M ⊆ carrier G |]
==> M #> (x ⊗ (inv y)) = M "
done

lemma (in group) coset_join1:
"[| H #> x = H;  x ∈ carrier G;  subgroup H G |] ==> x ∈ H"
apply (erule subst)
apply (blast intro: l_one subgroup.one_closed sym)
done

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 monoid) 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])

lemma (in group) rcos_self: "[| x ∈ carrier G; subgroup H G |] ==> x ∈ H #> x"
apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
subgroup.one_closed)
done

text (in group) ‹Opposite of @{thm [source] "repr_independence"}›
lemma (in group) repr_independenceD:
assumes "subgroup H G"
assumes ycarr: "y ∈ carrier G"
and repr:  "H #> x = H #> y"
shows "y ∈ H #> x"
proof -
interpret subgroup H G by fact
show ?thesis  apply (subst repr)
apply (intro rcos_self)
apply (rule ycarr)
apply (rule is_subgroup)
done
qed

text ‹Elements of a right coset are in the carrier›
lemma (in subgroup) elemrcos_carrier:
assumes "group G"
assumes acarr: "a ∈ carrier G"
and a': "a' ∈ H #> a"
shows "a' ∈ carrier G"
proof -
interpret group G by fact
from subset and acarr
have "H #> a ⊆ carrier G" by (rule r_coset_subset_G)
from this and a'
show "a' ∈ carrier G"
by fast
qed

lemma (in subgroup) rcos_const:
assumes "group G"
assumes hH: "h ∈ H"
shows "H #> h = H"
proof -
interpret group G by fact
show ?thesis apply (unfold r_coset_def)
apply rule
apply rule
apply clarsimp
apply (intro subgroup.m_closed)
apply (rule is_subgroup)
apply assumption
apply (rule hH)
apply rule
apply simp
proof -
fix h'
assume h'H: "h' ∈ H"
note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
from carr
have a: "h' = (h' ⊗ inv h) ⊗ h" by (simp add: m_assoc)
from h'H hH
have "h' ⊗ inv h ∈ H" by simp
from this and a
show "∃x∈H. h' = x ⊗ h" by fast
qed
qed

text ‹Step one for lemma ‹rcos_module››
lemma (in subgroup) rcos_module_imp:
assumes "group G"
assumes xcarr: "x ∈ carrier G"
and x'cos: "x' ∈ H #> x"
shows "(x' ⊗ inv x) ∈ H"
proof -
interpret group G by fact
from xcarr x'cos
have x'carr: "x' ∈ carrier G"
by (rule elemrcos_carrier[OF is_group])
from xcarr
have ixcarr: "inv x ∈ carrier G"
by simp
from x'cos
have "∃h∈H. x' = h ⊗ x"
unfolding r_coset_def
by fast
from this
obtain h
where hH: "h ∈ H"
and x': "x' = h ⊗ x"
by auto
from hH and subset
have hcarr: "h ∈ carrier G" by fast
note carr = xcarr x'carr hcarr
from x' and carr
have "x' ⊗ (inv x) = (h ⊗ x) ⊗ (inv x)" by fast
also from carr
have "… = h ⊗ (x ⊗ inv x)" by (simp add: m_assoc)
also from carr
have "… = h ⊗ 𝟭" by simp
also from carr
have "… = h" by simp
finally
have "x' ⊗ (inv x) = h" by simp
from hH this
show "x' ⊗ (inv x) ∈ H" by simp
qed

text ‹Step two for lemma ‹rcos_module››
lemma (in subgroup) rcos_module_rev:
assumes "group G"
assumes carr: "x ∈ carrier G" "x' ∈ carrier G"
and xixH: "(x' ⊗ inv x) ∈ H"
shows "x' ∈ H #> x"
proof -
interpret group G by fact
from xixH
have "∃h∈H. x' ⊗ (inv x) = h" by fast
from this
obtain h
where hH: "h ∈ H"
and hsym: "x' ⊗ (inv x) = h"
by fast
from hH subset have hcarr: "h ∈ carrier G" by simp
note carr = carr hcarr
from hsym[symmetric] have "h ⊗ x = x' ⊗ (inv x) ⊗ x" by fast
also from carr
have "… = x' ⊗ ((inv x) ⊗ x)" by (simp add: m_assoc)
also from carr
have "… = x' ⊗ 𝟭" by simp
also from carr
have "… = x'" by simp
finally
have "h ⊗ x = x'" by simp
from this[symmetric] and hH
show "x' ∈ H #> x"
unfolding r_coset_def
by fast
qed

text ‹Module property of right cosets›
lemma (in subgroup) rcos_module:
assumes "group G"
assumes carr: "x ∈ carrier G" "x' ∈ carrier G"
shows "(x' ∈ H #> x) = (x' ⊗ inv x ∈ H)"
proof -
interpret group G by fact
show ?thesis proof  assume "x' ∈ H #> x"
from this and carr
show "x' ⊗ inv x ∈ H"
by (intro rcos_module_imp[OF is_group])
next
assume "x' ⊗ inv x ∈ H"
from this and carr
show "x' ∈ H #> x"
by (intro rcos_module_rev[OF is_group])
qed
qed

text ‹Right cosets are subsets of the carrier.›
lemma (in subgroup) rcosets_carrier:
assumes "group G"
assumes XH: "X ∈ rcosets H"
shows "X ⊆ carrier G"
proof -
interpret group G by fact
from XH have "∃x∈ carrier G. X = H #> x"
unfolding RCOSETS_def
by fast
from this
obtain x
where xcarr: "x∈ carrier G"
and X: "X = H #> x"
by fast
from subset and xcarr
show "X ⊆ carrier G"
unfolding X
by (rule r_coset_subset_G)
qed

text ‹Multiplication of general subsets›
lemma (in monoid) set_mult_closed:
assumes Acarr: "A ⊆ carrier G"
and Bcarr: "B ⊆ carrier G"
shows "A <#> B ⊆ carrier G"
apply rule apply (simp add: set_mult_def, clarsimp)
proof -
fix a b
assume "a ∈ A"
from this and Acarr
have acarr: "a ∈ carrier G" by fast

assume "b ∈ B"
from this and Bcarr
have bcarr: "b ∈ carrier G" by fast

from acarr bcarr
show "a ⊗ b ∈ carrier G" by (rule m_closed)
qed

lemma (in comm_group) mult_subgroups:
assumes subH: "subgroup H G"
and subK: "subgroup K G"
shows "subgroup (H <#> K) G"
apply (rule subgroup.intro)
apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
apply (simp add: set_mult_def) apply clarsimp defer 1
apply (simp add: set_mult_def) defer 1
apply (simp add: set_mult_def, clarsimp) defer 1
proof -
fix ha hb ka kb
assume haH: "ha ∈ H" and hbH: "hb ∈ H" and kaK: "ka ∈ K" and kbK: "kb ∈ K"
note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
from carr
have "(ha ⊗ ka) ⊗ (hb ⊗ kb) = ha ⊗ (ka ⊗ hb) ⊗ kb" by (simp add: m_assoc)
also from carr
have "… = ha ⊗ (hb ⊗ ka) ⊗ kb" by (simp add: m_comm)
also from carr
have "… = (ha ⊗ hb) ⊗ (ka ⊗ kb)" by (simp add: m_assoc)
finally
have eq: "(ha ⊗ ka) ⊗ (hb ⊗ kb) = (ha ⊗ hb) ⊗ (ka ⊗ kb)" .

from haH hbH have hH: "ha ⊗ hb ∈ H" by (simp add: subgroup.m_closed[OF subH])
from kaK kbK have kK: "ka ⊗ kb ∈ K" by (simp add: subgroup.m_closed[OF subK])

from hH and kK and eq
show "∃h'∈H. ∃k'∈K. (ha ⊗ ka) ⊗ (hb ⊗ kb) = h' ⊗ k'" by fast
next
have "𝟭 = 𝟭 ⊗ 𝟭" by simp
from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
show "∃h∈H. ∃k∈K. 𝟭 = h ⊗ k" by fast
next
fix h k
assume hH: "h ∈ H"
and kK: "k ∈ K"

from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
have "inv (h ⊗ k) = inv h ⊗ inv k" by (simp add: inv_mult_group m_comm)

from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
show "∃ha∈H. ∃ka∈K. inv (h ⊗ k) = ha ⊗ ka" by fast
qed

lemma (in subgroup) lcos_module_rev:
assumes "group G"
assumes carr: "x ∈ carrier G" "x' ∈ carrier G"
and xixH: "(inv x ⊗ x') ∈ H"
shows "x' ∈ x <# H"
proof -
interpret group G by fact
from xixH
have "∃h∈H. (inv x) ⊗ x' = h" by fast
from this
obtain h
where hH: "h ∈ H"
and hsym: "(inv x) ⊗ x' = h"
by fast

from hH subset have hcarr: "h ∈ carrier G" by simp
note carr = carr hcarr
from hsym[symmetric] have "x ⊗ h = x ⊗ ((inv x) ⊗ x')" by fast
also from carr
have "… = (x ⊗ (inv x)) ⊗ x'" by (simp add: m_assoc[symmetric])
also from carr
have "… = 𝟭 ⊗ x'" by simp
also from carr
have "… = x'" by simp
finally
have "x ⊗ h = x'" by simp

from this[symmetric] and hH
show "x' ∈ x <# H"
unfolding l_coset_def
by fast
qed

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"
by (simp add: normal_def normal_axioms_def is_group)

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 (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
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

subsection‹More Properties of Cosets›

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"

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 (auto simp add: subgroup.m_closed set_mult_def Sigma_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)
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"
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 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 "rcong⇘G⇙ H = {(x,y). x ∈ carrier G & y ∈ 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 (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)"])
done
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 (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)"
ultimately
have "(inv (a ⊗ c)) ⊗ (b ⊗ c) ∈ H" by simp
from carr and this
have "(b ⊗ c) ∈ (a ⊗ c) <# H"
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"
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)"

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 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])
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:
"⟦c ∈ rcosets H;  H ⊆ carrier G; finite(carrier G)⟧
⟹ card c = card H"
apply (rule card_bij_eq)
apply (rule inj_on_f, assumption+)
apply (force simp add: m_assoc subsetD r_coset_def)
apply (rule inj_on_g, assumption+)
apply (force simp add: m_assoc subsetD r_coset_def)
txt‹The sets @{term "H #> a"} and @{term "H"} are finite.›
apply (simp add: r_coset_subset_G [THEN finite_subset])
apply (blast intro: finite_subset)
done

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⟧
⟹ 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])
done

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 = rcosets⇘G⇙ 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 (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
from _ subgroup_axioms have "H #> 𝟭 = H"
by (rule coset_join2) auto
then show ?thesis
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)
apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
apply (simp add: restrictI setmult_closed rcosets_assoc)
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'"

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

lemma (in group_hom) FactGroup_inj_on:
"inj_on (λX. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
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"
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:
"h ` carrier G = carrier H
⟹ (λX. the_elem (h`X)) ∈ (G Mod (kernel G H h)) ≅ H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)

end
```