# Theory HOL-Algebra.Coset

```(*  Title:      HOL/Algebra/Coset.thy
Authors:    Florian Kammueller, L C Paulson, Stephan Hohe

With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
*)

theory Coset
imports Group
begin

section ‹Cosets and Quotient Groups›

definition
r_coset    :: "[_, 'a set, 'a] ⇒ 'a set"    (infixl "#>ı" 60)
where "H #>⇘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"

lemma (in comm_group) subgroup_imp_normal: "subgroup A G ⟹ A ⊲ G"
by (simp add: normal_def normal_axioms_def l_coset_def r_coset_def m_comm subgroup.mem_carrier)

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

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

lemma (in subgroup) rcosets_non_empty: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "R ∈ rcosets H"
shows "R ≠ {}"
proof -
obtain g where "g ∈ carrier G" "R = H #> g"
using assms unfolding RCOSETS_def by blast
hence "𝟭 ⊗ g ∈ R"
using one_closed unfolding r_coset_def by blast
thus ?thesis by blast
qed

lemma (in group) diff_neutralizes: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "subgroup H G" "R ∈ rcosets H"
shows "⋀r1 r2. ⟦ r1 ∈ R; r2 ∈ R ⟧ ⟹ r1 ⊗ (inv r2) ∈ H"
proof -
fix r1 r2 assume r1: "r1 ∈ R" and r2: "r2 ∈ R"
obtain g where g: "g ∈ carrier G" "R = H #> g"
using assms unfolding RCOSETS_def by blast
then obtain h1 h2 where h1: "h1 ∈ H" "r1 = h1 ⊗ g"
and h2: "h2 ∈ H" "r2 = h2 ⊗ g"
using r1 r2 unfolding r_coset_def by blast
hence "r1 ⊗ (inv r2) = (h1 ⊗ g) ⊗ ((inv g) ⊗ (inv h2))"
using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
also have " ... =  (h1 ⊗ (g ⊗ inv g) ⊗ inv h2)"
using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
monoid_axioms subgroup.mem_carrier
proof -
have "h1 ∈ carrier G"
by (meson subgroup.mem_carrier assms(1) h1(1))
moreover have "h2 ∈ carrier G"
by (meson subgroup.mem_carrier assms(1) h2(1))
ultimately show ?thesis
using g(1) inv_closed m_assoc m_closed by presburger
qed
finally have "r1 ⊗ inv r2 = h1 ⊗ inv h2"
using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
thus "r1 ⊗ inv r2 ∈ H" by (metis assms(1) h1(1) h2(1) subgroup_def)
qed

lemma mono_set_mult: "⟦ H ⊆ H'; K ⊆ K' ⟧ ⟹ H <#>⇘G⇙ K ⊆ H' <#>⇘G⇙ K'" ✐‹contributor ‹Paulo Emílio de Vilhena››
unfolding set_mult_def by (simp add: UN_mono)

subsection ‹Stable Operations for Subgroups›

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

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

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

subsection ‹Basic Properties of set multiplication›

lemma (in group) setmult_subset_G:
assumes "H ⊆ carrier G" "K ⊆ carrier G"
shows "H <#> K ⊆ carrier G" using assms
by (auto simp add: set_mult_def subsetD)

lemma (in monoid) set_mult_closed:
assumes "H ⊆ carrier G" "K ⊆ carrier G"
shows "H <#> K ⊆ carrier G"
using assms by (auto simp add: set_mult_def subsetD)

lemma (in group) set_mult_assoc: ✐‹contributor ‹Martin Baillon››
assumes "M ⊆ carrier G" "H ⊆ carrier G" "K ⊆ carrier G"
shows "(M <#> H) <#> K = M <#> (H <#> K)"
proof
show "(M <#> H) <#> K ⊆ M <#> (H <#> K)"
proof
fix x assume "x ∈ (M <#> H) <#> K"
then obtain m h k where x: "m ∈ M" "h ∈ H" "k ∈ K" "x = (m ⊗ h) ⊗ k"
unfolding set_mult_def by blast
hence "x = m ⊗ (h ⊗ k)"
using assms m_assoc by blast
thus "x ∈ M <#> (H <#> K)"
unfolding set_mult_def using x by blast
qed
next
show "M <#> (H <#> K) ⊆ (M <#> H) <#> K"
proof
fix x assume "x ∈ M <#> (H <#> K)"
then obtain m h k where x: "m ∈ M" "h ∈ H" "k ∈ K" "x = m ⊗ (h ⊗ k)"
unfolding set_mult_def by blast
hence "x = (m ⊗ h) ⊗ k"
using assms m_assoc rev_subsetD by metis
thus "x ∈ (M <#> H) <#> K"
unfolding set_mult_def using x by blast
qed
qed

subsection ‹Basic Properties of Cosets›

lemma (in group) coset_mult_assoc:
assumes "M ⊆ carrier G" "g ∈ carrier G" "h ∈ carrier G"
shows "(M #> g) #> h = M #> (g ⊗ h)"
using assms by (force simp add: r_coset_def m_assoc)

lemma (in group) coset_assoc:
assumes "x ∈ carrier G" "y ∈ carrier G" "H ⊆ carrier G"
shows "x <# (H #> y) = (x <# H) #> y"
using set_mult_assoc[of "{x}" H "{y}"]
by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms)

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

lemma (in group) coset_mult_inv1:
assumes "M #> (x ⊗ (inv y)) = M"
and "x ∈ carrier G" "y ∈ carrier G" "M ⊆ carrier G"
shows "M #> x = M #> y" using assms
by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self)

lemma (in group) coset_mult_inv2:
assumes "M #> x = M #> y"
and "x ∈ carrier G"  "y ∈ carrier G" "M ⊆ carrier G"
shows "M #> (x ⊗ (inv y)) = M " using assms
by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)

lemma (in group) coset_join1:
assumes "H #> x = H"
and "x ∈ carrier G" "subgroup H G"
shows "x ∈ H"
using assms r_coset_def l_one subgroup.one_closed sym by fastforce

lemma (in group) solve_equation:
assumes "subgroup H G" "x ∈ H" "y ∈ H"
shows "∃h ∈ H. y = h ⊗ x"
proof -
have "y = (y ⊗ (inv x)) ⊗ x" using assms
by (simp add: m_assoc subgroup.mem_carrier)
moreover have "y ⊗ (inv x) ∈ H" using assms
by (simp add: subgroup_def)
ultimately show ?thesis by blast
qed

lemma (in group_hom) inj_on_one_iff:
"inj_on h (carrier G) ⟷ (∀x. x ∈ carrier G ⟶ h x = one H ⟶ x = one G)"
using G.solve_equation G.subgroup_self by (force simp: inj_on_def)

lemma inj_on_one_iff':
"⟦h ∈ hom G H; group G; group H⟧ ⟹ inj_on h (carrier G) ⟷ (∀x. x ∈ carrier G ⟶ h x = one H ⟶ x = one G)"
using group_hom.inj_on_one_iff group_hom.intro group_hom_axioms.intro by blast

lemma mon_iff_hom_one:
"⟦group G; group H⟧ ⟹ f ∈ mon G H ⟷ f ∈ hom G H ∧ (∀x. x ∈ carrier G ∧ f x = 𝟭⇘H⇙ ⟶ x = 𝟭⇘G⇙)"
by (auto simp: mon_def inj_on_one_iff')

lemma (in group_hom) iso_iff: "h ∈ iso G H ⟷ carrier H ⊆ h ` carrier G ∧ (∀x∈carrier G. h x = 𝟭⇘H⇙ ⟶ x = 𝟭)"
by (auto simp: iso_def bij_betw_def inj_on_one_iff)

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

lemma (in group) coset_join2:
assumes "x ∈ carrier G" "subgroup H G" "x ∈ H"
shows "H #> x = H" using assms
― ‹Alternative proof is to put \<^term>‹x=𝟭› in ‹repr_independence›.›
by (force simp add: subgroup.m_closed r_coset_def solve_equation)

lemma (in group) coset_join3:
assumes "x ∈ carrier G" "subgroup H G" "x ∈ H"
shows "x <# H = H"
proof
have "⋀h. h ∈ H ⟹ x ⊗ h ∈ H" using assms
by (simp add: subgroup.m_closed)
thus "x <# H ⊆ H" unfolding l_coset_def by blast
next
have "⋀h. h ∈ H ⟹ x ⊗ ((inv x) ⊗ h) = h"
by (metis (no_types, lifting) assms group.inv_closed group.inv_solve_left is_group
monoid.m_closed monoid_axioms subgroup.mem_carrier)
moreover have "⋀h. h ∈ H ⟹ (inv x) ⊗ h ∈ H"
by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)
ultimately show "H ⊆ x <# H" unfolding l_coset_def by blast
qed

lemma (in monoid) r_coset_subset_G:
"⟦ H ⊆ carrier G; x ∈ carrier G ⟧ ⟹ H #> x ⊆ carrier G"
by (auto simp add: r_coset_def)

lemma (in group) rcosI:
"⟦ h ∈ H; H ⊆ carrier G; x ∈ carrier G ⟧ ⟹ h ⊗ x ∈ H #> x"
by (auto simp add: r_coset_def)

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

lemma (in group) rcos_self:
"⟦ x ∈ carrier G; subgroup H G ⟧ ⟹ x ∈ H #> x"
by (metis l_one rcosI subgroup_def)

text (in group) ‹Opposite of @{thm [source] "repr_independence"}›
lemma (in group) repr_independenceD:
assumes "subgroup H G" "y ∈ carrier G"
and "H #> x = H #> y"
shows "y ∈ H #> x"
using assms by (simp add: rcos_self)

text ‹Elements of a right coset are in the carrier›
lemma (in subgroup) elemrcos_carrier:
assumes "group G" "a ∈ carrier G"
and "a' ∈ H #> a"
shows "a' ∈ carrier G"
by (meson assms group.is_monoid monoid.r_coset_subset_G subset subsetCE)

lemma (in subgroup) rcos_const:
assumes "group G" "h ∈ H"
shows "H #> h = H"
using group.coset_join2[OF assms(1), of h H]
by (simp add: assms(2) subgroup_axioms)

lemma (in subgroup) rcos_module_imp:
assumes "group G" "x ∈ carrier G"
and "x' ∈ H #> x"
shows "(x' ⊗ inv x) ∈ H"
proof -
obtain h where h: "h ∈ H" "x' = h ⊗ x"
using assms(3) unfolding r_coset_def by blast
hence "x' ⊗ inv x = h"
by (metis assms elemrcos_carrier group.inv_solve_right mem_carrier)
thus ?thesis using h by blast
qed

lemma (in subgroup) rcos_module_rev:
assumes "group G" "x ∈ carrier G" "x' ∈ carrier G"
and "(x' ⊗ inv x) ∈ H"
shows "x' ∈ H #> x"
proof -
obtain h where h: "h ∈ H" "x' ⊗ inv x = h"
using assms(4) unfolding r_coset_def by blast
hence "x' = h ⊗ x"
by (metis assms group.inv_solve_right mem_carrier)
thus ?thesis using h unfolding r_coset_def by blast
qed

text ‹Module property of right cosets›
lemma (in subgroup) rcos_module:
assumes "group G" "x ∈ carrier G" "x' ∈ carrier G"
shows "(x' ∈ H #> x) = (x' ⊗ inv x ∈ H)"
using rcos_module_rev rcos_module_imp assms by blast

text ‹Right cosets are subsets of the carrier.›
lemma (in subgroup) rcosets_carrier:
assumes "group G" "X ∈ rcosets H"
shows "X ⊆ carrier G"
using assms elemrcos_carrier singletonD
subset_eq unfolding RCOSETS_def by force

text ‹Multiplication of general subsets›

lemma (in comm_group) mult_subgroups:
assumes HG: "subgroup H G" and KG: "subgroup K G"
shows "subgroup (H <#> K) G"
proof (rule subgroup.intro)
show "H <#> K ⊆ carrier G"
by (simp add: setmult_subset_G assms subgroup.subset)
next
have "𝟭 ⊗ 𝟭 ∈ H <#> K"
unfolding set_mult_def using assms subgroup.one_closed by blast
thus "𝟭 ∈ H <#> K" by simp
next
show "⋀x. x ∈ H <#> K ⟹ inv x ∈ H <#> K"
proof -
fix x assume "x ∈ H <#> K"
then obtain h k where hk: "h ∈ H" "k ∈ K" "x = h ⊗ k"
unfolding set_mult_def by blast
hence "inv x = (inv k) ⊗ (inv h)"
by (meson inv_mult_group assms subgroup.mem_carrier)
hence "inv x = (inv h) ⊗ (inv k)"
by (metis hk inv_mult assms subgroup.mem_carrier)
thus "inv x ∈ H <#> K"
unfolding set_mult_def using hk assms
by (metis (no_types, lifting) UN_iff singletonI subgroup_def)
qed
next
show "⋀x y. x ∈ H <#> K ⟹ y ∈ H <#> K ⟹ x ⊗ y ∈ H <#> K"
proof -
fix x y assume "x ∈ H <#> K" "y ∈ H <#> K"
then obtain h1 k1 h2 k2 where h1k1: "h1 ∈ H" "k1 ∈ K" "x = h1 ⊗ k1"
and h2k2: "h2 ∈ H" "k2 ∈ K" "y = h2 ⊗ k2"
unfolding set_mult_def by blast
with KG HG have carr: "k1 ∈ carrier G" "h1 ∈ carrier G" "k2 ∈ carrier G" "h2 ∈ carrier G"
by (meson subgroup.mem_carrier)+
have "x ⊗ y = (h1 ⊗ k1) ⊗ (h2 ⊗ k2)"
using h1k1 h2k2 by simp
also have " ... = h1 ⊗ (k1 ⊗ h2) ⊗ k2"
by (simp add: carr comm_groupE(3) comm_group_axioms)
also have " ... = h1 ⊗ (h2 ⊗ k1) ⊗ k2"
by (simp add: carr m_comm)
finally have "x ⊗ y  = (h1 ⊗ h2) ⊗ (k1 ⊗ k2)"
by (simp add: carr comm_groupE(3) comm_group_axioms)
thus "x ⊗ y ∈ H <#> K" unfolding set_mult_def
using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)]
subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast
qed
qed

lemma (in subgroup) lcos_module_rev:
assumes "group G" "x ∈ carrier G" "x' ∈ carrier G"
and "(inv x ⊗ x') ∈ H"
shows "x' ∈ x <# H"
proof -
obtain h where h: "h ∈ H" "inv x ⊗ x' = h"
using assms(4) unfolding l_coset_def by blast
hence "x' = x ⊗ h"
by (metis assms group.inv_solve_left mem_carrier)
thus ?thesis using h unfolding l_coset_def by blast
qed

subsection ‹Normal subgroups›

lemma normal_imp_subgroup: "H ⊲ G ⟹ subgroup H G"
by (rule normal.axioms(1))

lemma (in group) normalI:
"subgroup H G ⟹ (∀x ∈ carrier G. H #> x = x <# H) ⟹ H ⊲ G"
by (simp add: normal_def normal_axioms_def is_group)

lemma (in normal) inv_op_closed1:
assumes "x ∈ carrier G" and "h ∈ H"
shows "(inv x) ⊗ h ⊗ x ∈ H"
proof -
have "h ⊗ x ∈ x <# H"
using assms coset_eq assms(1) unfolding r_coset_def by blast
then obtain h' where "h' ∈ H" "h ⊗ x = x ⊗ h'"
unfolding l_coset_def by blast
thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier)
qed

lemma (in normal) inv_op_closed2:
assumes "x ∈ carrier G" and "h ∈ H"
shows "x ⊗ h ⊗ (inv x) ∈ H"
using assms inv_op_closed1 by (metis inv_closed inv_inv)

lemma (in comm_group) normal_iff_subgroup:
"N ⊲ G ⟷ subgroup N G"
proof
assume "subgroup N G"
then show "N ⊲ G"
by unfold_locales (auto simp: subgroupE subgroup.one_closed l_coset_def r_coset_def m_comm subgroup.mem_carrier)
qed (simp add: normal_imp_subgroup)

text‹Alternative characterization of normal subgroups›
lemma (in group) normal_inv_iff:
"(N ⊲ G) =
(subgroup N G ∧ (∀x ∈ carrier G. ∀h ∈ N. x ⊗ h ⊗ (inv x) ∈ N))"
(is "_ = ?rhs")
proof
assume N: "N ⊲ G"
show ?rhs
by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
next
assume ?rhs
hence sg: "subgroup N G"
and closed: "⋀x. x∈carrier G ⟹ ∀h∈N. x ⊗ h ⊗ inv x ∈ N" by auto
hence sb: "N ⊆ carrier G" by (simp add: subgroup.subset)
show "N ⊲ G"
proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
fix x
assume x: "x ∈ carrier G"
show "(⋃h∈N. {h ⊗ x}) = (⋃h∈N. {x ⊗ h})"
proof
show "(⋃h∈N. {h ⊗ x}) ⊆ (⋃h∈N. {x ⊗ h})"
proof clarify
fix n
assume n: "n ∈ N"
show "n ⊗ x ∈ (⋃h∈N. {x ⊗ h})"
proof
from closed [of "inv x"]
show "inv x ⊗ n ⊗ x ∈ N" by (simp add: x n)
show "n ⊗ x ∈ {x ⊗ (inv x ⊗ n ⊗ x)}"
by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
qed
qed
next
show "(⋃h∈N. {x ⊗ h}) ⊆ (⋃h∈N. {h ⊗ x})"
proof clarify
fix n
assume n: "n ∈ N"
show "x ⊗ n ∈ (⋃h∈N. {h ⊗ x})"
proof
show "x ⊗ n ⊗ inv x ∈ N" by (simp add: x n closed)
show "x ⊗ n ∈ {x ⊗ n ⊗ inv x ⊗ x}"
by (simp add: x n m_assoc sb [THEN subsetD])
qed
qed
qed
qed
qed

corollary (in group) normal_invI:
assumes "subgroup N G" and "⋀x h. ⟦ x ∈ carrier G; h ∈ N ⟧ ⟹ x ⊗ h ⊗ inv x ∈ N"
shows "N ⊲ G"
using assms normal_inv_iff by blast

corollary (in group) normal_invE:
assumes "N ⊲ G"
shows "subgroup N G" and "⋀x h. ⟦ x ∈ carrier G; h ∈ N ⟧ ⟹ x ⊗ h ⊗ inv x ∈ N"
using assms normal_inv_iff apply blast
by (simp add: assms normal.inv_op_closed2)

lemma (in group) one_is_normal: "{𝟭} ⊲ G"
using normal_invI triv_subgroup by force

text ‹The intersection of two normal subgroups is, again, a normal subgroup.›
lemma (in group) normal_subgroup_intersect:
assumes "M ⊲ G" and "N ⊲ G" shows "M ∩ N ⊲ G"
using  assms normal_inv_iff subgroups_Inter_pair by force

text ‹Being a normal subgroup is preserved by surjective homomorphisms.›

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

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

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

subsection‹More Properties of Left Cosets›

lemma (in group) l_repr_independence:
assumes "y ∈ x <# H" "x ∈ carrier G" and HG: "subgroup H G"
shows "x <# H = y <# H"
proof -
obtain h' where h': "h' ∈ H" "y = x ⊗ h'"
using assms(1) unfolding l_coset_def by blast
hence "x ⊗ h = y ⊗ ((inv h') ⊗ h)" if "h ∈ H" for h
proof -
have "h' ∈ carrier G"
by (meson HG h'(1) subgroup.mem_carrier)
moreover have "h ∈ carrier G"
by (meson HG subgroup.mem_carrier that)
ultimately show ?thesis
by (metis assms(2) h'(2) inv_closed inv_solve_right m_assoc m_closed)
qed
hence "⋀xh. xh ∈ x <# H ⟹ xh ∈ y <# H"
unfolding l_coset_def by (metis (no_types, lifting) UN_iff HG h'(1) subgroup_def)
moreover have "⋀h. h ∈ H ⟹ y ⊗ h = x ⊗ (h' ⊗ h)"
using h' by (meson assms(2) HG m_assoc subgroup.mem_carrier)
hence "⋀yh. yh ∈ y <# H ⟹ yh ∈ x <# H"
unfolding l_coset_def using subgroup.m_closed[OF HG h'(1)] by blast
ultimately show ?thesis by blast
qed

lemma (in group) lcos_m_assoc:
"⟦ M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G ⟧ ⟹ g <# (h <# M) = (g ⊗ h) <# M"
by (force simp add: l_coset_def m_assoc)

lemma (in group) lcos_mult_one: "M ⊆ carrier G ⟹ 𝟭 <# M = M"
by (force simp add: l_coset_def)

lemma (in group) l_coset_subset_G:
"⟦ H ⊆ carrier G; x ∈ carrier G ⟧ ⟹ x <# H ⊆ carrier G"
by (auto simp add: l_coset_def subsetD)

lemma (in group) l_coset_carrier:
"⟦ y ∈ x <# H; x ∈ carrier G; subgroup H G ⟧ ⟹ y ∈ carrier G"
by (auto simp add: l_coset_def m_assoc  subgroup.subset [THEN subsetD] subgroup.m_closed)

lemma (in group) l_coset_swap:
assumes "y ∈ x <# H" "x ∈ carrier G" "subgroup H G"
shows "x ∈ y <# H"
using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
unfolding l_coset_def by fastforce

lemma (in group) subgroup_mult_id:
assumes "subgroup H G"
shows "H <#> H = H"
proof
show "H <#> H ⊆ H"
unfolding set_mult_def using subgroup.m_closed[OF assms] by (simp add: UN_subset_iff)
show "H ⊆ H <#> H"
proof
fix x assume x: "x ∈ H" thus "x ∈ H <#> H" unfolding set_mult_def
using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms]
using assms subgroup.mem_carrier by force
qed
qed

subsubsection ‹Set of Inverses of an ‹r_coset›.›

lemma (in normal) rcos_inv:
assumes x:     "x ∈ carrier G"
shows "set_inv (H #> x) = H #> (inv x)"
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
fix h
assume h: "h ∈ H"
show "inv x ⊗ inv h ∈ (⋃j∈H. {j ⊗ inv x})"
proof
show "inv x ⊗ inv h ⊗ x ∈ H"
by (simp add: inv_op_closed1 h x)
show "inv x ⊗ inv h ∈ {inv x ⊗ inv h ⊗ x ⊗ inv x}"
by (simp add: h x m_assoc)
qed
show "h ⊗ inv x ∈ (⋃j∈H. {inv x ⊗ inv j})"
proof
show "x ⊗ inv h ⊗ inv x ∈ H"
by (simp add: inv_op_closed2 h x)
show "h ⊗ inv x ∈ {inv x ⊗ inv (x ⊗ inv h ⊗ inv x)}"
by (simp add: h x m_assoc [symmetric] inv_mult_group)
qed
qed

subsubsection ‹Theorems for ‹<#>› with ‹#>› or ‹<#›.›

lemma (in group) setmult_rcos_assoc:
"⟦H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G⟧ ⟹
H <#> (K #> x) = (H <#> K) #> x"
using set_mult_assoc[of H K "{x}"] by (simp add: r_coset_eq_set_mult)

lemma (in group) rcos_assoc_lcos:
"⟦H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G⟧ ⟹
(H #> x) <#> K = H <#> (x <# K)"
using set_mult_assoc[of H "{x}" K]
by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)

lemma (in normal) rcos_mult_step1:
"⟦x ∈ carrier G; y ∈ carrier G⟧ ⟹
(H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
by (simp add: setmult_rcos_assoc r_coset_subset_G
subset l_coset_subset_G rcos_assoc_lcos)

lemma (in normal) rcos_mult_step2:
"⟦x ∈ carrier G; y ∈ carrier G⟧
⟹ (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
by (insert coset_eq, simp add: normal_def)

lemma (in normal) rcos_mult_step3:
"⟦x ∈ carrier G; y ∈ carrier G⟧
⟹ (H <#> (H #> x)) #> y = H #> (x ⊗ y)"
by (simp add: setmult_rcos_assoc coset_mult_assoc
subgroup_mult_id normal.axioms subset normal_axioms)

lemma (in normal) rcos_sum:
"⟦x ∈ carrier G; y ∈ carrier G⟧
⟹ (H #> x) <#> (H #> y) = H #> (x ⊗ y)"
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)

lemma (in normal) rcosets_mult_eq: "M ∈ rcosets H ⟹ H <#> M = M"
― ‹generalizes ‹subgroup_mult_id››
by (auto simp add: RCOSETS_def subset
setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)

subsubsection‹An Equivalence Relation›

definition
r_congruent :: "[('a,'b)monoid_scheme, 'a set] ⇒ ('a*'a)set"  ("rcongı _")
where "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)
have "rcong H ⊆ carrier G × carrier G"
by (auto simp add: r_congruent_def)
thus "refl_on (carrier G) (rcong H)"
by (auto simp add: r_congruent_def refl_on_def)
next
show "sym (rcong H)"
proof (simp add: r_congruent_def sym_def, clarify)
fix x y
assume [simp]: "x ∈ carrier G" "y ∈ carrier G"
and "inv x ⊗ y ∈ H"
hence "inv (inv x ⊗ y) ∈ H" by simp
thus "inv y ⊗ x ∈ H" by (simp add: inv_mult_group)
qed
next
show "trans (rcong H)"
proof (simp add: r_congruent_def trans_def, clarify)
fix x y z
assume [simp]: "x ∈ carrier G" "y ∈ carrier G" "z ∈ carrier G"
and "inv x ⊗ y ∈ H" and "inv y ⊗ z ∈ H"
hence "(inv x ⊗ y) ⊗ (inv y ⊗ z) ∈ H" by simp
hence "inv x ⊗ (y ⊗ inv y) ⊗ z ∈ H"
by (simp add: m_assoc del: r_inv Units_r_inv)
thus "inv x ⊗ z ∈ H" by simp
qed
qed
qed

text‹Equivalence classes of ‹rcong› correspond to left cosets.
Was there a mistake in the definitions? I'd have expected them to
correspond to right cosets.›

(* CB: This is correct, but subtle.
We call H #> a the right coset of a relative to H.  According to
Jacobson, this is what the majority of group theory literature does.
He then defines the notion of congruence relation ~ over monoids as
equivalence relation with a ~ a' & b ~ b' ⟹ a*b ~ a'*b'.
Our notion of right congruence induced by K: rcong K appears only in
the context where K is a normal subgroup.  Jacobson doesn't name it.
But in this context left and right cosets are identical.
*)

lemma (in subgroup) l_coset_eq_rcong:
assumes "group G"
assumes a: "a ∈ carrier G"
shows "a <# H = (rcong H) `` {a}"
proof -
interpret group G by fact
show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
qed

subsubsection‹Two Distinct Right Cosets are Disjoint›

lemma (in group) rcos_equation:
assumes "subgroup H G"
assumes p: "ha ⊗ a = h ⊗ b" "a ∈ carrier G" "b ∈ carrier G" "h ∈ H" "ha ∈ H" "hb ∈ H"
shows "hb ⊗ a ∈ (⋃h∈H. {h ⊗ b})"
proof -
interpret subgroup H G by fact
from p show ?thesis
by (rule_tac UN_I [of "hb ⊗ ((inv ha) ⊗ h)"]) (auto simp: inv_solve_left m_assoc)
qed

lemma (in group) rcos_disjoint:
assumes "subgroup H G"
shows "pairwise disjnt (rcosets H)"
proof -
interpret subgroup H G by fact
show ?thesis
unfolding RCOSETS_def r_coset_def pairwise_def disjnt_def
by (blast intro: rcos_equation assms sym)
qed

subsection ‹Further lemmas for ‹r_congruent››

text ‹The relation is a congruence›

lemma (in normal) congruent_rcong:
shows "congruent2 (rcong H) (rcong H) (λa b. a ⊗ b <# H)"
proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
fix a b c
assume abrcong: "(a, b) ∈ rcong H"
and ccarr: "c ∈ carrier G"

from abrcong
have acarr: "a ∈ carrier G"
and bcarr: "b ∈ carrier G"
and abH: "inv a ⊗ b ∈ H"
unfolding r_congruent_def
by fast+

note carr = acarr bcarr ccarr

from ccarr and abH
have "inv c ⊗ (inv a ⊗ b) ⊗ c ∈ H" by (rule inv_op_closed1)
moreover
from carr and inv_closed
have "inv c ⊗ (inv a ⊗ b) ⊗ c = (inv c ⊗ inv a) ⊗ (b ⊗ c)"
by (force cong: m_assoc)
moreover
from carr and inv_closed
have "… = (inv (a ⊗ c)) ⊗ (b ⊗ c)"
by (simp add: inv_mult_group)
ultimately
have "(inv (a ⊗ c)) ⊗ (b ⊗ c) ∈ H" by simp
from carr and this
have "(b ⊗ c) ∈ (a ⊗ c) <# H"
by (simp add: lcos_module_rev[OF is_group])
from carr and this and is_subgroup
show "(a ⊗ c) <# H = (b ⊗ c) <# H" by (intro l_repr_independence, simp+)
next
fix a b c
assume abrcong: "(a, b) ∈ rcong H"
and ccarr: "c ∈ carrier G"

from ccarr have "c ∈ Units G" by simp
hence cinvc_one: "inv c ⊗ c = 𝟭" by (rule Units_l_inv)

from abrcong
have acarr: "a ∈ carrier G"
and bcarr: "b ∈ carrier G"
and abH: "inv a ⊗ b ∈ H"
by (unfold r_congruent_def, fast+)

note carr = acarr bcarr ccarr

from carr and inv_closed
have "inv a ⊗ b = inv a ⊗ (𝟭 ⊗ b)" by simp
also from carr and inv_closed
have "… = inv a ⊗ (inv c ⊗ c) ⊗ b" by simp
also from carr and inv_closed
have "… = (inv a ⊗ inv c) ⊗ (c ⊗ b)" by (force cong: m_assoc)
also from carr and inv_closed
have "… = inv (c ⊗ a) ⊗ (c ⊗ b)" by (simp add: inv_mult_group)
finally
have "inv a ⊗ b = inv (c ⊗ a) ⊗ (c ⊗ b)" .
from abH and this
have "inv (c ⊗ a) ⊗ (c ⊗ b) ∈ H" by simp

from carr and this
have "(c ⊗ b) ∈ (c ⊗ a) <# H"
by (simp add: lcos_module_rev[OF is_group])
from carr and this and is_subgroup
show "(c ⊗ a) <# H = (c ⊗ b) <# H" by (intro l_repr_independence, simp+)
qed

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

definition
order :: "('a, 'b) monoid_scheme ⇒ nat"
where "order S = card (carrier S)"

lemma iso_same_order:
assumes "φ ∈ iso G H"
shows "order G = order H"
by (metis assms is_isoI iso_same_card order_def order_def)

lemma (in monoid) order_gt_0_iff_finite: "0 < order G ⟷ finite (carrier G)"
by(auto simp add: order_def card_gt_0_iff)

lemma (in group) order_one_triv_iff:
shows "(order G = 1) = (carrier G = {𝟭})"
by (metis One_nat_def card.empty card_Suc_eq empty_iff one_closed order_def singleton_iff)

lemma (in group) rcosets_part_G:
assumes "subgroup H G"
shows "⋃(rcosets H) = carrier G"
proof -
interpret subgroup H G by fact
show ?thesis
unfolding RCOSETS_def r_coset_def by auto
qed

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

text‹The next two lemmas support the proof of ‹card_cosets_equal›.›
lemma (in group) inj_on_f:
assumes "H ⊆ carrier G" and a: "a ∈ carrier G"
shows "inj_on (λy. y ⊗ inv a) (H #> a)"
proof
fix x y
assume "x ∈ H #> a" "y ∈ H #> a" and xy: "x ⊗ inv a = y ⊗ inv a"
then have "x ∈ carrier G" "y ∈ carrier G"
using assms r_coset_subset_G by blast+
with xy a show "x = y"
by auto
qed

lemma (in group) inj_on_g:
"⟦H ⊆ carrier G;  a ∈ carrier G⟧ ⟹ inj_on (λy. y ⊗ a) H"
by (force simp add: inj_on_def subsetD)

(* ************************************************************************** *)

lemma (in group) card_cosets_equal:
assumes "R ∈ rcosets H" "H ⊆ carrier G"
shows "∃f. bij_betw f H R"
proof -
obtain g where g: "g ∈ carrier G" "R = H #> g"
using assms(1) unfolding RCOSETS_def by blast

let ?f = "λh. h ⊗ g"
have "⋀r. r ∈ R ⟹ ∃h ∈ H. ?f h = r"
proof -
fix r assume "r ∈ R"
then obtain h where "h ∈ H" "r = h ⊗ g"
using g unfolding r_coset_def by blast
thus "∃h ∈ H. ?f h = r" by blast
qed
hence "R ⊆ ?f ` H" by blast
moreover have "?f ` H ⊆ R"
using g unfolding r_coset_def by blast
ultimately show ?thesis using inj_on_g unfolding bij_betw_def
using assms(2) g(1) by auto
qed

corollary (in group) card_rcosets_equal:
assumes "R ∈ rcosets H" "H ⊆ carrier G"
shows "card H = card R"
using card_cosets_equal assms bij_betw_same_card by blast

corollary (in group) rcosets_finite:
assumes "R ∈ rcosets H" "H ⊆ carrier G" "finite H"
shows "finite R"
using card_cosets_equal assms bij_betw_finite is_group by blast

(* ************************************************************************** *)

lemma (in group) rcosets_subset_PowG:
"subgroup H G  ⟹ rcosets H ⊆ Pow(carrier G)"
using rcosets_part_G by auto

proposition (in group) lagrange_finite:
assumes "finite(carrier G)" and HG: "subgroup H G"
shows "card(rcosets H) * card(H) = order(G)"
proof -
have "card H * card (rcosets H) = card (⋃(rcosets H))"
proof (rule card_partition)
show "⋀c1 c2. ⟦c1 ∈ rcosets H; c2 ∈ rcosets H; c1 ≠ c2⟧ ⟹ c1 ∩ c2 = {}"
using HG rcos_disjoint by (auto simp: pairwise_def disjnt_def)
qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
then show ?thesis
by (simp add: HG mult.commute order_def rcosets_part_G)
qed

theorem (in group) lagrange:
assumes "subgroup H G"
shows "card (rcosets H) * card H = order G"
proof (cases "finite (carrier G)")
case True thus ?thesis using lagrange_finite assms by simp
next
case False
thus ?thesis
proof (cases "finite H")
case False thus ?thesis using ‹infinite (carrier G)›  by (simp add: order_def)
next
case True
have "infinite (rcosets H)"
proof
assume "finite (rcosets H)"
hence finite_rcos: "finite (rcosets H)" by simp
hence "card (⋃(rcosets H)) = (∑R∈(rcosets H). card R)"
using card_Union_disjoint[of "rcosets H"] ‹finite H› rcos_disjoint[OF assms(1)]
rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
hence "order G = (∑R∈(rcosets H). card R)"
by (simp add: assms order_def rcosets_part_G)
hence "order G = (∑R∈(rcosets H). card H)"
using card_rcosets_equal by (simp add: assms subgroup.subset)
hence "order G = (card H) * (card (rcosets H))" by simp
hence "order G ≠ 0" using finite_rcos ‹finite H› assms ex_in_conv
rcosets_part_G subgroup.one_closed by fastforce
thus False using ‹infinite (carrier G)› order_gt_0_iff_finite by blast
qed
thus ?thesis using ‹infinite (carrier G)› by (simp add: order_def)
qed
qed

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

subsection ‹Quotient Groups: Factorization of a Group›

definition
FactGroup :: "[('a,'b) monoid_scheme, 'a set] ⇒ ('a set) monoid" (infixl "Mod" 65)
― ‹Actually defined for groups rather than monoids›
where "FactGroup G H = ⦇carrier = 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 (simp add: group.set_mult_assoc is_group rcosets_carrier)

lemma (in subgroup) subgroup_in_rcosets:
assumes "group G"
shows "H ∈ rcosets H"
proof -
interpret group G by fact
from _ subgroup_axioms have "H #> 𝟭 = H"
by (rule coset_join2) auto
then show ?thesis
by (auto simp add: RCOSETS_def)
qed

lemma (in normal) rcosets_inv_mult_group_eq:
"M ∈ rcosets H ⟹ set_inv M <#> M = H"
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)

theorem (in normal) factorgroup_is_group: "group (G Mod H)"
proof -
have "⋀x. x ∈ rcosets H ⟹ ∃y∈rcosets H. y <#> x = H"
using rcosets_inv_mult_group_eq setinv_closed by blast
then show ?thesis
unfolding FactGroup_def
by (intro groupI)
(auto simp: setmult_closed subgroup_in_rcosets rcosets_assoc rcosets_mult_eq)
qed

lemma carrier_FactGroup: "carrier(G Mod N) = (λx. r_coset G N x) ` carrier G"
by (auto simp: FactGroup_def RCOSETS_def)

lemma one_FactGroup [simp]: "one(G Mod N) = N"
by (auto simp: FactGroup_def)

lemma mult_FactGroup [simp]: "monoid.mult (G Mod N) = set_mult G"
by (auto simp: FactGroup_def)

lemma (in normal) inv_FactGroup:
assumes "X ∈ carrier (G Mod H)"
shows "inv⇘G Mod H⇙ X = set_inv X"
proof -
have X: "X ∈ rcosets H"
using assms by (simp add: FactGroup_def)
moreover have "set_inv X <#> X = H"
using X by (simp add: normal.rcosets_inv_mult_group_eq normal_axioms)
moreover have "Group.group (G Mod H)"
using normal.factorgroup_is_group normal_axioms by blast
ultimately show ?thesis
by (simp add: FactGroup_def group.inv_equality normal.setinv_closed normal_axioms)
qed

text‹The coset map is a homomorphism from \<^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)

lemma (in comm_group) set_mult_commute:
assumes "N ⊆ carrier G" "x ∈ rcosets N" "y ∈ rcosets N"
shows "x <#> y = y <#> x"
using assms unfolding set_mult_def RCOSETS_def
by auto (metis m_comm r_coset_subset_G subsetCE)+

lemma (in comm_group) abelian_FactGroup:
assumes "subgroup N G" shows "comm_group(G Mod N)"
proof (rule group.group_comm_groupI)
have "N ⊲ G"
by (simp add: assms normal_iff_subgroup)
then show "Group.group (G Mod N)"
by (simp add: normal.factorgroup_is_group)
fix x :: "'a set" and y :: "'a set"
assume "x ∈ carrier (G Mod N)" "y ∈ carrier (G Mod N)"
then show "x ⊗⇘G Mod N⇙ y = y ⊗⇘G Mod N⇙ x"
by (metis FactGroup_def assms mult_FactGroup partial_object.simps(1) set_mult_commute subgroup_def)
qed

lemma FactGroup_universal:
assumes "h ∈ hom G H" "N ⊲ G"
and h: "⋀x y. ⟦x ∈ carrier G; y ∈ carrier G; r_coset G N x = r_coset G N y⟧ ⟹ h x = h y"
obtains g
where "g ∈ hom (G Mod N) H" "⋀x. x ∈ carrier G ⟹ g(r_coset G N x) = h x"
proof -
obtain g where g: "⋀x. x ∈ carrier G ⟹ h x = g(r_coset G N x)"
using h function_factors_left_gen [of "λx. x ∈ carrier G" "r_coset G N" h] by blast
show thesis
proof
show "g ∈ hom (G Mod N) H"
proof (rule homI)
show "g (u ⊗⇘G Mod N⇙ v) = g u ⊗⇘H⇙ g v"
if "u ∈ carrier (G Mod N)" "v ∈ carrier (G Mod N)" for u v
proof -
from that
obtain x y where xy: "x ∈ carrier G" "u = r_coset G N x" "y ∈ carrier G"  "v = r_coset G N y"
by (auto simp: carrier_FactGroup)
then have "h (x ⊗⇘G⇙ y) = h x ⊗⇘H⇙ h y"
by (metis hom_mult [OF ‹h ∈ hom G H›])
then show ?thesis
by (metis Coset.mult_FactGroup xy ‹N ⊲ G› g group.subgroup_self normal.axioms(2) normal.rcos_sum subgroup_def)
qed
qed (use ‹h ∈ hom G H› in ‹auto simp: carrier_FactGroup Pi_iff hom_def simp flip: g›)
qed (auto simp flip: g)
qed

lemma (in normal) FactGroup_pow:
fixes k::nat
assumes "a ∈ carrier G"
shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
proof (induction k)
case 0
then show ?case
by (simp add: r_coset_def)
next
case (Suc k)
then show ?case
by (simp add: assms rcos_sum)
qed

lemma (in normal) FactGroup_int_pow:
fixes k::int
assumes "a ∈ carrier G"
shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
by (metis Group.group.axioms(1) image_eqI is_group monoid.nat_pow_closed int_pow_def2 assms
FactGroup_pow carrier_FactGroup inv_FactGroup rcos_inv)

subsection‹The First Isomorphism Theorem›

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

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

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

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

lemma iso_kernel_image:
assumes "group G" "group H"
shows "f ∈ iso G H ⟷ f ∈ hom G H ∧ kernel G H f = {𝟭⇘G⇙} ∧ f ` carrier G = carrier H"
(is "?lhs = ?rhs")
proof (intro iffI conjI)
assume f: ?lhs
show "f ∈ hom G H"
using Group.iso_iff f by blast
show "kernel G H f = {𝟭⇘G⇙}"
using assms f Group.group_def hom_one
by (fastforce simp add: kernel_def iso_iff_mon_epi mon_iff_hom_one set_eq_iff)
show "f ` carrier G = carrier H"
by (meson Group.iso_iff f)
next
assume ?rhs
with assms show ?lhs
by (auto simp: kernel_def iso_def bij_betw_def inj_on_one_iff')
qed

lemma (in group_hom) FactGroup_nonempty:
assumes "X ∈ carrier (G Mod kernel G H h)"
shows "X ≠ {}"
using assms unfolding FactGroup_def
by (metis group_hom.subgroup_kernel group_hom_axioms partial_object.simps(1) subgroup.rcosets_non_empty)

lemma (in group_hom) FactGroup_universal_kernel:
assumes "N ⊲ G" and h: "N ⊆ kernel G H h"
obtains g where "g ∈ hom (G Mod N) H" "⋀x. x ∈ carrier G ⟹ g(r_coset G N x) = h x"
proof -
have "h x = h y"
if "x ∈ carrier G" "y ∈ carrier G" "r_coset G N x = r_coset G N y" for x y
proof -
have "x ⊗⇘G⇙ inv⇘G⇙ y ∈ N"
using ‹N ⊲ G› group.rcos_self normal.axioms(2) normal_imp_subgroup
subgroup.rcos_module_imp that by metis
with h have xy: "x ⊗⇘G⇙ inv⇘G⇙ y ∈ kernel G H h"
by blast
have "h x ⊗⇘H⇙ inv⇘H⇙(h y) = h (x ⊗⇘G⇙ inv⇘G⇙ y)"
by (simp add: that)
also have "… = 𝟭⇘H⇙"
using xy by (simp add: kernel_def)
finally have "h x ⊗⇘H⇙ inv⇘H⇙(h y) = 𝟭⇘H⇙" .
then show ?thesis
using H.inv_equality that by fastforce
qed
with FactGroup_universal [OF homh ‹N ⊲ G›] that show thesis
by metis
qed

lemma (in group_hom) FactGroup_the_elem_mem:
assumes X: "X ∈ carrier (G Mod (kernel G H h))"
shows "the_elem (h`X) ∈ carrier H"
proof -
from X
obtain g where g: "g ∈ carrier G"
and "X = kernel G H h #> g"
by (auto simp add: FactGroup_def RCOSETS_def)
hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
thus ?thesis by (auto simp add: g)
qed

lemma (in group_hom) FactGroup_hom:
"(λX. the_elem (h`X)) ∈ hom (G Mod (kernel G H h)) H"
proof -
have "the_elem (h ` (X <#> X')) = the_elem (h ` X) ⊗⇘H⇙ the_elem (h ` X')"
if X: "X  ∈ carrier (G Mod kernel G H h)" and X': "X' ∈ carrier (G Mod kernel G H h)" for X X'
proof -
obtain g and g'
where "g ∈ carrier G" and "g' ∈ carrier G"
and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
using X X' by (auto simp add: FactGroup_def RCOSETS_def)
hence all: "∀x∈X. h x = h g" "∀x∈X'. h x = h g'"
and Xsub: "X ⊆ carrier G" and X'sub: "X' ⊆ carrier G"
by (force simp add: kernel_def r_coset_def image_def)+
hence "h ` (X <#> X') = {h g ⊗⇘H⇙ h g'}" using X X'
by (auto dest!: FactGroup_nonempty intro!: image_eqI
simp add: set_mult_def
subsetD [OF Xsub] subsetD [OF X'sub])
then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) ⊗⇘H⇙ the_elem (h ` X')"
by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
qed
then show ?thesis
by (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
qed

text‹Lemma for the following injectivity result›
lemma (in group_hom) FactGroup_subset:
assumes "g ∈ carrier G" "g' ∈ carrier G" "h g = h g'"
shows "kernel G H h #> g ⊆ kernel G H h #> g'"
unfolding kernel_def r_coset_def
proof clarsimp
fix y
assume "y ∈ carrier G" "h y = 𝟭⇘H⇙"
with assms show "∃x. x ∈ carrier G ∧ h x = 𝟭⇘H⇙ ∧ y ⊗ g = x ⊗ g'"
by (rule_tac x="y ⊗ g ⊗ inv g'" in exI) (auto simp: G.m_assoc)
qed

lemma (in group_hom) FactGroup_inj_on:
"inj_on (λX. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
proof (simp add: inj_on_def, clarify)
fix X and X'
assume X:  "X  ∈ carrier (G Mod kernel G H h)"
and X': "X' ∈ carrier (G Mod kernel G H h)"
then
obtain g and g'
where gX: "g ∈ carrier G"  "g' ∈ carrier G"
"X = kernel G H h #> g" "X' = kernel G H h #> g'"
by (auto simp add: FactGroup_def RCOSETS_def)
hence all: "∀x∈X. h x = h g" "∀x∈X'. h x = h g'"
by (force simp add: kernel_def r_coset_def image_def)+
assume "the_elem (h ` X) = the_elem (h ` X')"
hence h: "h g = h g'"
by (simp add: all FactGroup_nonempty X X' the_elem_image_unique)
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
qed

text‹If the homomorphism \<^term>‹h› is onto \<^term>‹H›, then so is the
homomorphism from the quotient group›
lemma (in group_hom) FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
shows "(λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
proof
show "(λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h) ⊆ carrier H"
by (auto simp add: FactGroup_the_elem_mem)
show "carrier H ⊆ (λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
proof
fix y
assume y: "y ∈ carrier H"
with h obtain g where g: "g ∈ carrier G" "h g = y"
by (blast elim: equalityE)
hence "(⋃x∈kernel G H h #> g. {h x}) = {y}"
by (auto simp add: y kernel_def r_coset_def)
with g show "y ∈ (λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
apply (subst the_elem_image_unique)
apply auto
done
qed
qed

text‹If \<^term>‹h› is a homomorphism from \<^term>‹G› onto \<^term>‹H›, then the
quotient group \<^term>‹G Mod (kernel G H h)› is isomorphic to \<^term>‹H›.›
theorem (in group_hom) FactGroup_iso_set:
"h ` carrier G = carrier H
⟹ (λX. the_elem (h`X)) ∈ iso (G Mod (kernel G H h)) H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)

corollary (in group_hom) FactGroup_iso :
"h ` carrier G = carrier H
⟹ (G Mod (kernel G H h))≅ H"
using FactGroup_iso_set unfolding is_iso_def by auto

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

lemma (in group_hom) trivial_ker_imp_inj: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "kernel G H h = { 𝟭 }"
shows "inj_on h (carrier G)"
proof (rule inj_onI)
fix g1 g2 assume A: "g1 ∈ carrier G" "g2 ∈ carrier G" "h g1 = h g2"
hence "h (g1 ⊗ (inv g2)) = 𝟭⇘H⇙" by simp
hence "g1 ⊗ (inv g2) = 𝟭"
using A assms unfolding kernel_def by blast
thus "g1 = g2"
using A G.inv_equality G.inv_inv by blast
qed

lemma (in group_hom) inj_iff_trivial_ker:
shows "inj_on h (carrier G) ⟷ kernel G H h = { 𝟭 }"
proof
assume inj: "inj_on h (carrier G)" show "kernel G H h = { 𝟭 }"
unfolding kernel_def
proof (auto)
fix a assume "a ∈ carrier G" "h a = 𝟭⇘H⇙" thus "a = 𝟭"
using inj hom_one unfolding inj_on_def by force
qed
next
show "kernel G H h = { 𝟭 } ⟹ inj_on h (carrier G)"
using trivial_ker_imp_inj by simp
qed

lemma (in group_hom) induced_group_hom':
assumes "subgroup I G" shows "group_hom (G ⦇ carrier := I ⦈) H h"
proof -
have "h ∈ hom (G ⦇ carrier := I ⦈) H"
using homh subgroup.subset[OF assms] unfolding hom_def by (auto, meson hom_mult subsetCE)
thus ?thesis
using subgroup.subgroup_is_group[OF assms G.group_axioms] group_axioms
unfolding group_hom_def group_hom_axioms_def by auto
qed

lemma (in group_hom) inj_on_subgroup_iff_trivial_ker:
assumes "subgroup I G"
shows "inj_on h I ⟷ kernel (G ⦇ carrier := I ⦈) H h = { 𝟭 }"
using group_hom.inj_iff_trivial_ker[OF induced_group_hom'[OF assms]] by simp

lemma set_mult_hom:
assumes "h ∈ hom G H" "I ⊆ carrier G" and "J ⊆ carrier G"
shows "h ` (I <#>⇘G⇙ J) = (h ` I) <#>⇘H⇙ (h ` J)"
proof
show "h ` (I <#>⇘G⇙ J) ⊆ (h ` I) <#>⇘H⇙ (h ` J)"
proof
fix a assume "a ∈ h ` (I <#>⇘G⇙ J)"
then obtain i j where i: "i ∈ I" and j: "j ∈ J" and "a = h (i ⊗⇘G⇙ j)"
unfolding set_mult_def by auto
hence "a = (h i) ⊗⇘H⇙ (h j)"
using assms unfolding hom_def by blast
thus "a ∈ (h ` I) <#>⇘H⇙ (h ` J)"
using i and j unfolding set_mult_def by auto
qed
next
show "(h ` I) <#>⇘H⇙ (h ` J) ⊆ h ` (I <#>⇘G⇙ J)"
proof
fix a assume "a ∈ (h ` I) <#>⇘H⇙ (h ` J)"
then obtain i j where i: "i ∈ I" and j: "j ∈ J" and "a = (h i) ⊗⇘H⇙ (h j)"
unfolding set_mult_def by auto
hence "a = h (i ⊗⇘G⇙ j)"
using assms unfolding hom_def by fastforce
thus "a ∈ h ` (I <#>⇘G⇙ J)"
using i and j unfolding set_mult_def by auto
qed
qed

corollary coset_hom:
assumes "h ∈ hom G H" "I ⊆ carrier G" "a ∈ carrier G"
shows "h ` (a <#⇘G⇙ I) = h a <#⇘H⇙ (h ` I)" and "h ` (I #>⇘G⇙ a) = (h ` I) #>⇘H⇙ h a"
unfolding l_coset_eq_set_mult r_coset_eq_set_mult using assms set_mult_hom[OF assms(1)] by auto

corollary (in group_hom) set_mult_ker_hom:
assumes "I ⊆ carrier G"
shows "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
proof -
have ker_in_carrier: "kernel G H h ⊆ carrier G"
unfolding kernel_def by auto

have "h ` (kernel G H h) = { 𝟭⇘H⇙ }"
unfolding kernel_def by force
moreover have "h ` I ⊆ carrier H"
using assms by auto
hence "(h ` I) <#>⇘H⇙ { 𝟭⇘H⇙ } = h ` I" and "{ 𝟭⇘H⇙ } <#>⇘H⇙ (h ` I) = h ` I"
unfolding set_mult_def by force+
ultimately show "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+
qed

subsubsection‹Trivial homomorphisms›

definition trivial_homomorphism where
"trivial_homomorphism G H f ≡ f ∈ hom G H ∧ (∀x ∈ carrier G. f x = one H)"

lemma trivial_homomorphism_kernel:
"trivial_homomorphism G H f ⟷ f ∈ hom G H ∧ kernel G H f = carrier G"
by (auto simp: trivial_homomorphism_def kernel_def)

lemma (in group) trivial_homomorphism_image:
"trivial_homomorphism G H f ⟷ f ∈ hom G H ∧ f ` carrier G = {one H}"
by (auto simp: trivial_homomorphism_def) (metis one_closed rev_image_eqI)

subsection ‹Image kernel theorems›

lemma group_Int_image_ker:
assumes f: "f ∈ hom G H" and g: "g ∈ hom H K"
and "inj_on (g ∘ f) (carrier G)" "group G" "group H" "group K"
shows "(f ` carrier G) ∩ (kernel H K g) = {𝟭⇘H⇙}"
proof -
have "(f ` carrier G) ∩ (kernel H K g) ⊆ {𝟭⇘H⇙}"
using assms
apply (clarsimp simp: kernel_def o_def)
by (metis group.is_monoid hom_one inj_on_eq_iff monoid.one_closed)
moreover have "one H ∈ f ` carrier G"
by (metis f ‹group G› ‹group H› group.is_monoid hom_one image_iff monoid.one_closed)
moreover have "one H ∈ kernel H K g"
unfolding kernel_def using Group.group_def ‹group H› ‹group K› g hom_one by blast
ultimately show ?thesis
by blast
qed

lemma group_sum_image_ker:
assumes f: "f ∈ hom G H" and g: "g ∈ hom H K" and eq: "(g ∘ f) ` (carrier G) = carrier K"
and "group G" "group H" "group K"
shows "set_mult H (f ` carrier G) (kernel H K g) = carrier H" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
apply (clarsimp simp: kernel_def set_mult_def)
by (meson ‹group H› f group.is_monoid hom_in_carrier monoid.m_closed)
have "∃x∈carrier G. ∃z. z ∈ carrier H ∧ g z = 𝟭⇘K⇙ ∧ y = f x ⊗⇘H⇙ z"
if y: "y ∈ carrier H" for y
proof -
have "g y ∈ carrier K"
using g hom_carrier that by blast
with assms obtain x where x: "x ∈ carrier G" "(g ∘ f) x = g y"
by (metis image_iff)
with assms have invf: "inv⇘H⇙ f x ⊗⇘H⇙ y ∈ carrier H"
by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
moreover
have "g (inv⇘H⇙ f x ⊗⇘H⇙ y) = 𝟭⇘K⇙"
proof -
have "inv⇘H⇙ f x ∈ carrier H"
by (meson ‹group H› f group.inv_closed hom_carrier image_subset_iff x(1))
then have "g (inv⇘H⇙ f x ⊗⇘H⇙ y) = g (inv⇘H⇙ f x) ⊗⇘K⇙ g y"
by (simp add: hom_mult [OF g] y)
also have "… = inv⇘K⇙ (g (f x)) ⊗⇘K⇙ g y"
using assms x(1)
by (metis (mono_tags, lifting) group_hom.hom_inv group_hom.intro group_hom_axioms.intro hom_carrier image_subset_iff)
also have "… = 𝟭⇘K⇙"
using ‹g y ∈ carrier K› assms(6) group.l_inv x(2) by fastforce
finally show ?thesis .
qed
moreover
have "y = f x ⊗⇘H⇙ (inv⇘H⇙ f x ⊗⇘H⇙ y)"
using x y
by (meson ‹group H› invf f group.inv_solve_left' hom_in_carrier)
ultimately
show ?thesis
using x y by force
qed
then show "?rhs ⊆ ?lhs"
by (auto simp: kernel_def set_mult_def)
qed

lemma group_sum_ker_image:
assumes f: "f ∈ hom G H" and g: "g ∈ hom H K" and eq: "(g ∘ f) ` (carrier G) = carrier K"
and "group G" "group H" "group K"
shows "set_mult H (kernel H K g) (f ` carrier G) = carrier H" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
apply (clarsimp simp: kernel_def set_mult_def)
by (meson ‹group H› f group.is_monoid hom_in_carrier monoid.m_closed)
have "∃w∈carrier H. ∃x ∈ carrier G. g w = 𝟭⇘K⇙ ∧ y = w ⊗⇘H⇙ f x"
if y: "y ∈ carrier H" for y
proof -
have "g y ∈ carrier K"
using g hom_carrier that by blast
with assms obtain x where x: "x ∈ carrier G" "(g ∘ f) x = g y"
by (metis image_iff)
with assms have carr: "(y ⊗⇘H⇙ inv⇘H⇙ f x) ∈ carrier H"
by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
moreover
have "g (y ⊗⇘H⇙ inv⇘H⇙ f x) = 𝟭⇘K⇙"
proof -
have "inv⇘H⇙ f x ∈ carrier H"
by (meson ‹group H› f group.inv_closed hom_carrier image_subset_iff x(1))
then have "g (y ⊗⇘H⇙ inv⇘H⇙ f x) = g y ⊗⇘K⇙ g (inv⇘H⇙ f x)"
by (simp add: hom_mult [OF g] y)
also have "… = g y ⊗⇘K⇙ inv⇘K⇙ (g (f x))"
using assms x(1)
by (metis group_hom.hom_inv group_hom_axioms.intro group_hom_def hom_in_carrier)
also have "… = 𝟭⇘K⇙"
using ‹g y ∈ carrier K› assms(6) group.l_inv x(2)
by (simp add: group.r_inv)
finally show ?thesis .
qed
moreover
have "y = (y ⊗⇘H⇙ inv⇘H⇙ f x) ⊗⇘H⇙ f x"
using x y by (meson ‹group H› carr f group.inv_solve_right hom_carrier image_subset_iff)
ultimately
show ?thesis
using x y by force
qed
then show "?rhs ⊆ ?lhs"
by (force simp: kernel_def set_mult_def)
qed

lemma group_semidirect_sum_ker_image:
assumes "(g ∘ f) ∈ iso G K" "f ∈ hom G H" "g ∈ hom H K" "group G" "group H" "group K"
shows "(kernel H K g) ∩ (f ` carrier G) = {𝟭⇘H⇙}"
"kernel H K g <#>⇘H⇙ (f ` carrier G) = carrier H"
using assms
by (simp_all add: iso_iff_mon_epi group_Int_image_ker group_sum_ker_image epi_def mon_def Int_commute [of "kernel H K g"])

lemma group_semidirect_sum_image_ker:
assumes f: "f ∈ hom G H" and g: "g ∈ hom H K" and iso: "(g ∘ f) ∈ iso G K"
and "group G" "group H" "group K"
shows "(f ` carrier G) ∩ (kernel H K g) = {𝟭⇘H⇙}"
"f ` carrier G <#>⇘H⇙ (kernel H K g) = carrier H"
using group_Int_image_ker [OF f g] group_sum_image_ker [OF f g] assms
by (simp_all add: iso_def bij_betw_def)

subsection ‹Factor Groups and Direct product›

lemma (in group) DirProd_normal : ✐‹contributor ‹Martin Baillon››
assumes "group K"
and "H ⊲ G"
and "N ⊲ K"
shows "H × N ⊲ G ×× K"
proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]])
show sub : "subgroup (H × N) (G ×× K)"
using DirProd_subgroups[OF group_axioms normal_imp_subgroup[OF assms(2)]assms(1)
normal_imp_subgroup[OF assms(3)]].
show "⋀x h. x ∈ carrier (G××K) ⟹ h ∈ H×N ⟹ x ⊗⇘G××K⇙ h ⊗⇘G××K⇙ inv⇘G××K⇙ x ∈ H×N"
proof-
fix x h assume xGK : "x ∈ carrier (G ×× K)" and hHN : " h ∈ H × N"
hence hGK : "h ∈ carrier (G ×× K)" using subgroup.subset[OF sub] by auto
from xGK obtain x1 x2 where x1x2 :"x1 ∈ carrier G" "x2 ∈ carrier K" "x = (x1,x2)"
unfolding DirProd_def by fastforce
from hHN obtain h1 h2 where h1h2 : "h1 ∈ H" "h2 ∈ N" "h = (h1,h2)"
unfolding DirProd_def by fastforce
hence h1h2GK : "h1 ∈ carrier G" "h2 ∈ carrier K"
using normal_imp_subgroup subgroup.subset assms by blast+
have "inv⇘G ×× K⇙ x = (inv⇘G⇙ x1,inv⇘K⇙ x2)"
using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
hence "x ⊗⇘G ×× K⇙ h ⊗⇘G ×× K⇙ inv⇘G ×× K⇙ x = (x1 ⊗ h1 ⊗ inv x1,x2 ⊗⇘K⇙ h2 ⊗⇘K⇙ inv⇘K⇙ x2)"
using h1h2 x1x2 ```