Theory HOL-Algebra.Coset
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:
fixes G (structure)
shows "x <# H = {x} <#> H"
unfolding l_coset_def set_mult_def by simp
lemma r_coset_eq_set_mult:
fixes G (structure)
shows "H #> x = H <#> {x}"
unfolding r_coset_def set_mult_def by simp
lemma (in subgroup) rcosets_non_empty:
assumes "R ∈ rcosets H"
shows "R ≠ {}"
proof -
obtain g where "g ∈ carrier G" "R = H #> g"
using assms unfolding RCOSETS_def by blast
hence "𝟭 ⊗ g ∈ R"
using one_closed unfolding r_coset_def by blast
thus ?thesis by blast
qed
lemma (in group) diff_neutralizes:
assumes "subgroup H G" "R ∈ rcosets H"
shows "⋀r1 r2. ⟦ r1 ∈ R; r2 ∈ R ⟧ ⟹ r1 ⊗ (inv r2) ∈ H"
proof -
fix r1 r2 assume r1: "r1 ∈ R" and r2: "r2 ∈ R"
obtain g where g: "g ∈ carrier G" "R = H #> g"
using assms unfolding RCOSETS_def by blast
then obtain h1 h2 where h1: "h1 ∈ H" "r1 = h1 ⊗ g"
and h2: "h2 ∈ H" "r2 = h2 ⊗ g"
using r1 r2 unfolding r_coset_def by blast
hence "r1 ⊗ (inv r2) = (h1 ⊗ g) ⊗ ((inv g) ⊗ (inv h2))"
using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
also have " ... = (h1 ⊗ (g ⊗ inv g) ⊗ inv h2)"
using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
monoid_axioms subgroup.mem_carrier
proof -
have "h1 ∈ carrier G"
by (meson subgroup.mem_carrier assms(1) h1(1))
moreover have "h2 ∈ carrier G"
by (meson subgroup.mem_carrier assms(1) h2(1))
ultimately show ?thesis
using g(1) inv_closed m_assoc m_closed by presburger
qed
finally have "r1 ⊗ inv r2 = h1 ⊗ inv h2"
using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
thus "r1 ⊗ inv r2 ∈ H" by (metis assms(1) h1(1) h2(1) subgroup_def)
qed
lemma mono_set_mult: "⟦ H ⊆ H'; K ⊆ K' ⟧ ⟹ H <#>⇘G⇙ K ⊆ H' <#>⇘G⇙ K'"
unfolding set_mult_def by (simp add: UN_mono)
subsection ‹Stable Operations for Subgroups›
lemma set_mult_consistent [simp]:
"N <#>⇘(G ⦇ carrier := H ⦈)⇙ K = N <#>⇘G⇙ K"
unfolding set_mult_def by simp
lemma r_coset_consistent [simp]:
"I #>⇘G ⦇ carrier := H ⦈⇙ h = I #>⇘G⇙ h"
unfolding r_coset_def by simp
lemma l_coset_consistent [simp]:
"h <#⇘G ⦇ carrier := H ⦈⇙ I = h <#⇘G⇙ I"
unfolding l_coset_def by simp
subsection ‹Basic Properties of set multiplication›
lemma (in group) setmult_subset_G:
assumes "H ⊆ carrier G" "K ⊆ carrier G"
shows "H <#> K ⊆ carrier G" using assms
by (auto simp add: set_mult_def subsetD)
lemma (in monoid) set_mult_closed:
assumes "H ⊆ carrier G" "K ⊆ carrier G"
shows "H <#> K ⊆ carrier G"
using assms by (auto simp add: set_mult_def subsetD)
lemma (in group) set_mult_assoc:
assumes "M ⊆ carrier G" "H ⊆ carrier G" "K ⊆ carrier G"
shows "(M <#> H) <#> K = M <#> (H <#> K)"
proof
show "(M <#> H) <#> K ⊆ M <#> (H <#> K)"
proof
fix x assume "x ∈ (M <#> H) <#> K"
then obtain m h k where x: "m ∈ M" "h ∈ H" "k ∈ K" "x = (m ⊗ h) ⊗ k"
unfolding set_mult_def by blast
hence "x = m ⊗ (h ⊗ k)"
using assms m_assoc by blast
thus "x ∈ M <#> (H <#> K)"
unfolding set_mult_def using x by blast
qed
next
show "M <#> (H <#> K) ⊆ (M <#> H) <#> K"
proof
fix x assume "x ∈ M <#> (H <#> K)"
then obtain m h k where x: "m ∈ M" "h ∈ H" "k ∈ K" "x = m ⊗ (h ⊗ k)"
unfolding set_mult_def by blast
hence "x = (m ⊗ h) ⊗ k"
using assms m_assoc rev_subsetD by metis
thus "x ∈ (M <#> H) <#> K"
unfolding set_mult_def using x by blast
qed
qed
subsection ‹Basic Properties of Cosets›
lemma (in group) coset_mult_assoc:
assumes "M ⊆ carrier G" "g ∈ carrier G" "h ∈ carrier G"
shows "(M #> g) #> h = M #> (g ⊗ h)"
using assms by (force simp add: r_coset_def m_assoc)
lemma (in group) coset_assoc:
assumes "x ∈ carrier G" "y ∈ carrier G" "H ⊆ carrier G"
shows "x <# (H #> y) = (x <# H) #> y"
using set_mult_assoc[of "{x}" H "{y}"]
by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms)
lemma (in group) coset_mult_one [simp]: "M ⊆ carrier G ==> M #> 𝟭 = M"
by (force simp add: r_coset_def)
lemma (in group) coset_mult_inv1:
assumes "M #> (x ⊗ (inv y)) = M"
and "x ∈ carrier G" "y ∈ carrier G" "M ⊆ carrier G"
shows "M #> x = M #> y" using assms
by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self)
lemma (in group) coset_mult_inv2:
assumes "M #> x = M #> y"
and "x ∈ carrier G" "y ∈ carrier G" "M ⊆ carrier G"
shows "M #> (x ⊗ (inv y)) = M " using assms
by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)
lemma (in group) coset_join1:
assumes "H #> x = H"
and "x ∈ carrier G" "subgroup H G"
shows "x ∈ H"
using assms r_coset_def l_one subgroup.one_closed sym by fastforce
lemma (in group) solve_equation:
assumes "subgroup H G" "x ∈ H" "y ∈ H"
shows "∃h ∈ H. y = h ⊗ x"
proof -
have "y = (y ⊗ (inv x)) ⊗ x" using assms
by (simp add: m_assoc subgroup.mem_carrier)
moreover have "y ⊗ (inv x) ∈ H" using assms
by (simp add: subgroup_def)
ultimately show ?thesis by blast
qed
lemma (in group_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
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"
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.›
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)
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"
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:
"h ` (carrier G) = { 𝟭⇘H⇙ } ⟷ kernel G H h = carrier G"
unfolding kernel_def using one_closed by force
lemma (in group_hom) trivial_ker_imp_inj:
assumes "kernel G H h = { 𝟭 }"
shows "inj_on h (carrier G)"
proof (rule inj_onI)
fix g1 g2 assume A: "g1 ∈ carrier G" "g2 ∈ carrier G" "h g1 = h g2"
hence "h (g1 ⊗ (inv g2)) = 𝟭⇘H⇙" by simp
hence "g1 ⊗ (inv g2) = 𝟭"
using A assms unfolding kernel_def by blast
thus "g1 = g2"
using A G.inv_equality G.inv_inv by blast
qed
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 :
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 h1h2GK by auto
moreover have "x1 ⊗ h1 ⊗ inv x1 ∈ H" "x2 ⊗⇘K⇙ h2 ⊗⇘K⇙ inv⇘K⇙ x2 ∈ N"
using assms x1x2 h1h2 assms by (simp_all add: normal.inv_op_closed2)
hence "(x1 ⊗ h1 ⊗ inv x1, x2 ⊗⇘K⇙ h2 ⊗⇘K⇙ inv⇘K⇙ x2)∈ H × N" by auto
ultimately show " x ⊗⇘G ×× K⇙ h ⊗⇘G ×× K⇙ inv⇘G ×× K⇙ x ∈ H × N" by auto
qed
qed
lemma (in group) FactGroup_DirProd_multiplication_iso_set :
assumes "group K"
and "H ⊲ G"
and "N ⊲ K"
shows "(λ (X, Y). X × Y) ∈ iso ((G Mod H) ×× (K Mod N)) (G ×× K Mod H × N)"
proof-
have R :"(λ(X, Y). X × Y) ∈ carrier (G Mod H) × carrier (K Mod N) → carrier (G ×× K Mod H × N)"
unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def by force
moreover have "(∀x∈carrier (G Mod H). ∀y∈carrier (K Mod N). ∀xa∈carrier (G Mod H).
∀ya∈carrier (K Mod N). (x <#> xa) × (y <#>⇘K⇙ ya) = x × y <#>⇘G ×× K⇙ xa × ya)"
unfolding set_mult_def by force
moreover have "(∀x∈carrier (G Mod H). ∀y∈carrier (K Mod N). ∀xa∈carrier (G Mod H).
∀ya∈carrier (K Mod N). x × y = xa × ya ⟶ x = xa ∧ y = ya)"
unfolding FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
moreover have "(λ(X, Y). X × Y) ` (carrier (G Mod H) × carrier (K Mod N)) =
carrier (G ×× K Mod H × N)"
proof -
have 1: "⋀x a b. ⟦a ∈ carrier (G Mod H); b ∈ carrier (K Mod N)⟧ ⟹ a × b ∈ carrier (G ×× K Mod H × N)"
using R by force
have 2: "⋀z. z ∈ carrier (G ×× K Mod H × N) ⟹ ∃x∈carrier (G Mod H). ∃y∈carrier (K Mod N). z = x × y"
unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
show ?thesis
unfolding image_def by (auto simp: intro: 1 2)
qed
ultimately show ?thesis
unfolding iso_def hom_def bij_betw_def inj_on_def by simp
qed
corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
assumes "group K"
and "H ⊲ G"
and "N ⊲ K"
shows " ((G Mod H) ×× (K Mod N)) ≅ (G ×× K Mod H × N)"
unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto
corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
assumes "group K"
and "H ⊲ G"
and "N ⊲ K"
shows "(G ×× K Mod H × N) ≅ ((G Mod H) ×× (K Mod N))"
using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms
DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
by blast
subsubsection "More Lemmas about set multiplication"
text ‹A group multiplied by a subgroup stays the same›
lemma (in group) set_mult_carrier_idem:
assumes "subgroup H G"
shows "(carrier G) <#> H = carrier G"
proof
show "(carrier G)<#>H ⊆ carrier G"
unfolding set_mult_def using subgroup.subset assms by blast
next
have " (carrier G) #> 𝟭 = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
moreover have "(carrier G) #> 𝟭 ⊆ (carrier G) <#> H" unfolding set_mult_def r_coset_def
using assms subgroup.one_closed[OF assms] by blast
ultimately show "carrier G ⊆ (carrier G) <#> H" by simp
qed
text ‹Same lemma as above, but everything is included in a subgroup›
lemma (in group) set_mult_subgroup_idem:
assumes HG: "subgroup H G" and NG: "subgroup N (G ⦇ carrier := H ⦈)"
shows "H <#> N = H"
using group.set_mult_carrier_idem[OF subgroup.subgroup_is_group[OF HG group_axioms] NG] by simp
text ‹A normal subgroup is commutative with set multiplication›
lemma (in group) commut_normal:
assumes "subgroup H G" and "N⊲G"
shows "H<#>N = N<#>H"
proof-
have aux1: "{H <#> N} = {⋃h∈H. h <# N }" unfolding set_mult_def l_coset_def by auto
also have "... = {⋃h∈H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
moreover have aux2: "{N <#> H} = {⋃h∈H. N #> h }"unfolding set_mult_def r_coset_def by auto
ultimately show "H<#>N = N<#>H" by simp
qed
text ‹Same lemma as above, but everything is included in a subgroup›
lemma (in group) commut_normal_subgroup:
assumes "subgroup H G" and "N ⊲ (G⦇ carrier := H ⦈)"
and "subgroup K (G ⦇ carrier := H ⦈)"
shows "K <#> N = N <#> K"
by (metis assms(2) assms(3) group.commut_normal normal.axioms(2) set_mult_consistent)
subsubsection "Lemmas about intersection and normal subgroups"
text ‹Mostly by Jakob von Raumer›
lemma (in group) normal_inter:
assumes "subgroup H G"
and "subgroup K G"
and "H1⊲G⦇carrier := H⦈"
shows "(H1∩K)⊲(G⦇carrier:= (H∩K)⦈)"
proof-
define HK and H1K and GH and GHK
where "HK = H∩K" and "H1K=H1∩K" and "GH =G⦇carrier := H⦈" and "GHK = (G⦇carrier:= (H∩K)⦈)"
show "H1K⊲GHK"
proof (intro group.normal_invI[of GHK H1K])
show "Group.group GHK"
using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
next
have H1K_incl:"subgroup H1K (G⦇carrier:= (H∩K)⦈)"
proof(intro subgroup_incl)
show "subgroup H1K G"
using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
next
show "subgroup (H∩K) G" using HK_def subgroups_Inter_pair assms by auto
next
have "H1 ⊆ (carrier (G⦇carrier:=H⦈))"
using assms(3) normal_imp_subgroup subgroup.subset by blast
also have "... ⊆ H" by simp
thus "H1K ⊆H∩K"
using H1K_def calculation by auto
qed
thus "subgroup H1K GHK" using GHK_def by simp
next
show "⋀ x h. x∈carrier GHK ⟹ h∈H1K ⟹ x ⊗⇘GHK⇙ h ⊗⇘GHK⇙ inv⇘GHK⇙ x∈ H1K"
proof-
have invHK: "⟦y∈HK⟧ ⟹ inv⇘GHK⇙ y = inv⇘GH⇙ y"
using m_inv_consistent assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
have multHK : "⟦x∈HK;y∈HK⟧ ⟹ x ⊗⇘(G⦇carrier:=HK⦈)⇙ y = x ⊗ y"
using HK_def by simp
fix x assume p: "x∈carrier GHK"
fix h assume p2 : "h:H1K"
have "carrier(GHK)⊆HK"
using GHK_def HK_def by simp
hence xHK:"x∈HK" using p by auto
hence invx:"inv⇘GHK⇙ x = inv⇘GH⇙ x"
using invHK assms GHK_def HK_def GH_def m_inv_consistent subgroups_Inter_pair by simp
have "H1⊆carrier(GH)"
using assms GH_def normal_imp_subgroup subgroup.subset by blast
hence hHK:"h∈HK"
using p2 H1K_def HK_def GH_def by auto
hence xhx_egal : "x ⊗⇘GHK⇙ h ⊗⇘GHK⇙ inv⇘GHK⇙x = x ⊗⇘GH⇙ h ⊗⇘GH⇙ inv⇘GH⇙ x"
using invx invHK multHK GHK_def GH_def by auto
have xH:"x∈carrier(GH)"
using xHK HK_def GH_def by auto
have hH:"h∈carrier(GH)"
using hHK HK_def GH_def by auto
have "(∀x∈carrier (GH). ∀h∈H1. x ⊗⇘GH⇙ h ⊗⇘GH⇙ inv⇘GH⇙ x ∈ H1)"
using assms GH_def normal.inv_op_closed2 by fastforce
hence INCL_1 : "x ⊗⇘GH⇙ h ⊗⇘GH⇙ inv⇘GH⇙ x ∈ H1"
using xH H1K_def p2 by blast
have " x ⊗⇘GH⇙ h ⊗⇘GH⇙ inv⇘GH⇙ x ∈ HK"
using assms HK_def subgroups_Inter_pair hHK xHK
by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
hence " x ⊗⇘GH⇙ h ⊗⇘GH⇙ inv⇘GH⇙ x ∈ K" using HK_def by simp
hence " x ⊗⇘GH⇙ h ⊗⇘GH⇙ inv⇘GH⇙ x ∈ H1K" using INCL_1 H1K_def by auto
thus "x ⊗⇘GHK⇙ h ⊗⇘GHK⇙ inv⇘GHK⇙ x ∈ H1K" using xhx_egal by simp
qed
qed
qed
lemma (in group) normal_Int_subgroup:
assumes "subgroup H G"
and "N ⊲ G"
shows "(N∩H) ⊲ (G⦇carrier := H⦈)"
proof -
define K where "K = carrier G"
have "G⦇carrier := K⦈ = G" using K_def by auto
moreover have "subgroup K G" using K_def subgroup_self by blast
moreover have "normal N (G ⦇carrier :=K⦈)" using assms K_def by simp
ultimately have "N ∩ H ⊲ G⦇carrier := K ∩ H⦈"
using normal_inter[of K H N] assms(1) by blast
moreover have "K ∩ H = H" using K_def assms subgroup.subset by blast
ultimately show "normal (N∩H) (G⦇carrier := H⦈)"
by auto
qed
lemma (in group) normal_restrict_supergroup:
assumes "subgroup S G" "N ⊲ G" "N ⊆ S"
shows "N ⊲ (G⦇carrier := S⦈)"
by (metis assms inf.absorb_iff1 normal_Int_subgroup)
text ‹A subgroup relation survives factoring by a normal subgroup.›
lemma (in group) normal_subgroup_factorize:
assumes "N ⊲ G" and "N ⊆ H" and "subgroup H G"
shows "subgroup (rcosets⇘G⦇carrier := H⦈⇙ N) (G Mod N)"
proof -
interpret GModN: group "G Mod N"
using assms(1) by (rule normal.factorgroup_is_group)
have "N ⊲ G⦇carrier := H⦈"
using assms by (metis normal_restrict_supergroup)
hence grpHN: "group (G⦇carrier := H⦈ Mod N)"
by (rule normal.factorgroup_is_group)
have "(<#>⇘G⦇carrier:=H⦈⇙) = (λU K. (⋃h∈U. ⋃k∈K. {h ⊗⇘G⦇carrier := H⦈⇙ k}))"
using set_mult_def by metis
moreover have "… = (λU K. (⋃h∈U. ⋃k∈K. {h ⊗⇘G⇙ k}))"
by auto
moreover have "(<#>) = (λU K. (⋃h∈U. ⋃k∈K. {h ⊗ k}))"
using set_mult_def by metis
ultimately have "(<#>⇘G⦇carrier:=H⦈⇙) = (<#>⇘G⇙)"
by simp
with grpHN have "group ((G Mod N)⦇carrier := (rcosets⇘G⦇carrier := H⦈⇙ N)⦈)"
unfolding FactGroup_def by auto
moreover have "rcosets⇘G⦇carrier := H⦈⇙ N ⊆ carrier (G Mod N)"
unfolding FactGroup_def RCOSETS_def r_coset_def using assms(3) subgroup.subset
by fastforce
ultimately show ?thesis
using GModN.group_incl_imp_subgroup by blast
qed
text ‹A normality relation survives factoring by a normal subgroup.›
lemma (in group) normality_factorization:
assumes NG: "N ⊲ G" and NH: "N ⊆ H" and HG: "H ⊲ G"
shows "(rcosets⇘G⦇carrier := H⦈⇙ N) ⊲ (G Mod N)"
proof -
from assms(1) interpret GModN: group "G Mod N" by (metis normal.factorgroup_is_group)
show ?thesis
unfolding GModN.normal_inv_iff
proof (intro conjI strip)
show "subgroup (rcosets⇘G⦇carrier := H⦈⇙ N) (G Mod N)"
using assms normal_imp_subgroup normal_subgroup_factorize by force
next
fix U V
assume U: "U ∈ carrier (G Mod N)" and V: "V ∈ rcosets⇘G⦇carrier := H⦈⇙ N"
then obtain g where g: "g ∈ carrier G" "U = N #> g"
unfolding FactGroup_def RCOSETS_def by auto
from V obtain h where h: "h ∈ H" "V = N #> h"
unfolding FactGroup_def RCOSETS_def r_coset_def by auto
hence hG: "h ∈ carrier G"
using HG normal_imp_subgroup subgroup.mem_carrier by force
hence ghG: "g ⊗ h ∈ carrier G"
using g m_closed by auto
from g h have "g ⊗ h ⊗ inv g ∈ H"
using HG normal_inv_iff by auto
moreover have "U <#> V <#> inv⇘G Mod N⇙ U = N #> (g ⊗ h ⊗ inv g)"
proof -
from g U have "inv⇘G Mod N⇙ U = N #> inv g"
using NG normal.inv_FactGroup normal.rcos_inv by fastforce
hence "U <#> V <#> inv⇘G Mod N⇙ U = (N #> g) <#> (N #> h) <#> (N #> inv g)"
using g h by simp
also have "… = N #> (g ⊗ h ⊗ inv g)"
using g hG NG inv_closed ghG normal.rcos_sum by force
finally show ?thesis .
qed
ultimately show "U ⊗⇘G Mod N⇙ V ⊗⇘G Mod N⇙ inv⇘G Mod N⇙ U ∈ rcosets⇘G⦇carrier := H⦈⇙ N"
unfolding RCOSETS_def r_coset_def by auto
qed
qed
text ‹Factorizing by the trivial subgroup is an isomorphism.›
lemma (in group) trivial_factor_iso:
shows "the_elem ∈ iso (G Mod {𝟭}) G"
proof -
have "group_hom G G (λx. x)"
unfolding group_hom_def group_hom_axioms_def hom_def using is_group by simp
moreover have "(λx. x) ` carrier G = carrier G"
by simp
moreover have "kernel G G (λx. x) = {𝟭}"
unfolding kernel_def by auto
ultimately show ?thesis using group_hom.FactGroup_iso_set
by force
qed
text ‹And the dual theorem to the previous one: Factorizing by the group itself gives the trivial group›
lemma (in group) self_factor_iso:
shows "(λX. the_elem ((λx. 𝟭) ` X)) ∈ iso (G Mod (carrier G)) (G⦇ carrier := {𝟭} ⦈)"
proof -
have "group (G⦇carrier := {𝟭}⦈)"
by (metis subgroup_imp_group triv_subgroup)
hence "group_hom G (G⦇carrier := {𝟭}⦈) (λx. 𝟭)"
unfolding group_hom_def group_hom_axioms_def hom_def using is_group by auto
moreover have "(λx. 𝟭) ` carrier G = carrier (G⦇carrier := {𝟭}⦈)"
by auto
moreover have "kernel G (G⦇carrier := {𝟭}⦈) (λx. 𝟭) = carrier G"
unfolding kernel_def by auto
ultimately show ?thesis using group_hom.FactGroup_iso_set
by force
qed
text ‹Factoring by a normal subgroups yields the trivial group iff the subgroup is the whole group.›
lemma (in normal) fact_group_trivial_iff:
assumes "finite (carrier G)"
shows "(carrier (G Mod H) = {𝟭⇘G Mod H⇙}) ⟷ (H = carrier G)"
proof
assume "carrier (G Mod H) = {𝟭⇘G Mod H⇙}"
moreover have "order (G Mod H) * card H = order G"
by (simp add: FactGroup_def lagrange order_def subgroup_axioms)
ultimately have "card H = order G" unfolding order_def by auto
thus "H = carrier G"
by (simp add: assms card_subset_eq order_def subset)
next
assume "H = carrier G"
with assms is_subgroup lagrange
have "card (rcosets H) * order G = order G"
by (simp add: order_def)
then have "card (rcosets H) = 1"
using assms order_gt_0_iff_finite by auto
hence "order (G Mod H) = 1"
unfolding order_def FactGroup_def by auto
thus "carrier (G Mod H) = {𝟭⇘G Mod H⇙}"
using factorgroup_is_group by (metis group.order_one_triv_iff)
qed
text ‹The union of all the cosets contained in a subgroup of a quotient group acts as a represenation for that subgroup.›
lemma (in normal) factgroup_subgroup_union_char:
assumes "subgroup A (G Mod H)"
shows "(⋃A) = {x ∈ carrier G. H #> x ∈ A}"
proof
show "⋃A ⊆ {x ∈ carrier G. H #> x ∈ A}"
proof
fix x
assume x: "x ∈ ⋃A"
then obtain a where a: "a ∈ A" "x ∈ a" and xx: "x ∈ carrier G"
using subgroup.subset assms by (force simp add: FactGroup_def RCOSETS_def r_coset_def)
from assms a obtain y where y: "y ∈ carrier G" "a = H #> y"
using subgroup.subset unfolding FactGroup_def RCOSETS_def by force
with a have "x ∈ H #> y" by simp
hence "H #> y = H #> x" using y is_subgroup repr_independence by auto
with y(2) a(1) have "H #> x ∈ A"
by auto
with xx show "x ∈ {x ∈ carrier G. H #> x ∈ A}" by simp
qed
next
show "{x ∈ carrier G. H #> x ∈ A} ⊆ ⋃A"
using rcos_self subgroup_axioms by auto
qed
lemma (in normal) factgroup_subgroup_union_subgroup:
assumes "subgroup A (G Mod H)"
shows "subgroup (⋃A) G"
proof -
have "subgroup {x ∈ carrier G. H #> x ∈ A} G"
proof
show "{x ∈ carrier G. H #> x ∈ A} ⊆ carrier G" by auto
next
fix x y
assume xy: "x ∈ {x ∈ carrier G. H #> x ∈ A}" "y ∈ {x ∈ carrier G. H #> x ∈ A}"
then have "(H #> x) <#> (H #> y) ∈ A"
using subgroup.m_closed assms unfolding FactGroup_def by fastforce
hence "H #> (x ⊗ y) ∈ A"
using xy rcos_sum by force
with xy show "x ⊗ y ∈ {x ∈ carrier G. H #> x ∈ A}" by blast
next
have "H #> 𝟭 ∈ A"
using assms subgroup.one_closed subset by fastforce
with assms one_closed show "𝟭 ∈ {x ∈ carrier G. H #> x ∈ A}" by simp
next
fix x
assume x: "x ∈ {x ∈ carrier G. H #> x ∈ A}"
hence invx: "inv x ∈ carrier G" using inv_closed by simp
from assms x have "set_inv (H #> x) ∈ A" using subgroup.m_inv_closed
using inv_FactGroup subgroup.mem_carrier by fastforce
with invx show "inv x ∈ {x ∈ carrier G. H #> x ∈ A}"
using rcos_inv x by force
qed
with assms factgroup_subgroup_union_char show ?thesis by auto
qed
lemma (in normal) factgroup_subgroup_union_normal:
assumes "A ⊲ (G Mod H)"
shows "⋃A ⊲ G"
proof -
have "{x ∈ carrier G. H #> x ∈ A} ⊲ G"
unfolding normal_def normal_axioms_def
proof (intro conjI strip)
from assms show "subgroup {x ∈ carrier G. H #> x ∈ A} G"
by (metis (full_types) factgroup_subgroup_union_char factgroup_subgroup_union_subgroup normal_imp_subgroup)
next
interpret Anormal: normal A "(G Mod H)" using assms by simp
show "{x ∈ carrier G. H #> x ∈ A} #> x = x <# {x ∈ carrier G. H #> x ∈ A}" if x: "x ∈ carrier G" for x
proof -
{ fix y
assume y: "y ∈ {x ∈ carrier G. H #> x ∈ A} #> x"
then obtain x' where x': "x' ∈ carrier G" "H #> x' ∈ A" "y = x' ⊗ x"
unfolding r_coset_def by auto
from x(1) have Hx: "H #> x ∈ carrier (G Mod H)"
unfolding FactGroup_def RCOSETS_def by force
with x' have "(inv⇘G Mod H⇙ (H #> x)) ⊗⇘G Mod H⇙ (H #> x') ⊗⇘G Mod H⇙ (H #> x) ∈ A"
using Anormal.inv_op_closed1 by auto
hence "(set_inv (H #> x)) <#> (H #> x') <#> (H #> x) ∈ A"
using inv_FactGroup Hx unfolding FactGroup_def by auto
hence "(H #> (inv x)) <#> (H #> x') <#> (H #> x) ∈ A"
using x(1) by (metis rcos_inv)
hence "H #> (inv x ⊗ x' ⊗ x) ∈ A"
by (metis inv_closed m_closed rcos_sum x'(1) x(1))
moreover have "inv x ⊗ x' ⊗ x ∈ carrier G"
using x x' by (metis inv_closed m_closed)
ultimately have xcoset: "x ⊗ (inv x ⊗ x' ⊗ x) ∈ x <# {x ∈ carrier G. H #> x ∈ A}"
unfolding l_coset_def using x(1) by auto
have "x ⊗ (inv x ⊗ x' ⊗ x) = (x ⊗ inv x) ⊗ x' ⊗ x"
by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
also have "… = y"
by (simp add: x x')
finally have "x ⊗ (inv x ⊗ x' ⊗ x) = y" .
with xcoset have "y ∈ x <# {x ∈ carrier G. H #> x ∈ A}" by auto}
moreover
{ fix y
assume y: "y ∈ x <# {x ∈ carrier G. H #> x ∈ A}"
then obtain x' where x': "x' ∈ carrier G" "H #> x' ∈ A" "y = x ⊗ x'" unfolding l_coset_def by auto
from x(1) have invx: "inv x ∈ carrier G"
by (rule inv_closed)
hence Hinvx: "H #> (inv x) ∈ carrier (G Mod H)"
unfolding FactGroup_def RCOSETS_def by force
with x' have "(inv⇘G Mod H⇙ (H #> inv x)) ⊗⇘G Mod H⇙ (H #> x') ⊗⇘G Mod H⇙ (H #> inv x) ∈ A"
using invx Anormal.inv_op_closed1 by auto
hence "(set_inv (H #> inv x)) <#> (H #> x') <#> (H #> inv x) ∈ A"
using inv_FactGroup Hinvx unfolding FactGroup_def by auto
hence "H #> (x ⊗ x' ⊗ inv x) ∈ A"
by (simp add: rcos_inv rcos_sum x x'(1))
moreover have "x ⊗ x' ⊗ inv x ∈ carrier G" using x x' by (metis inv_closed m_closed)
ultimately have xcoset: "(x ⊗ x' ⊗ inv x) ⊗ x ∈ {x ∈ carrier G. H #> x ∈ A} #> x"
unfolding r_coset_def using invx by auto
have "(x ⊗ x' ⊗ inv x) ⊗ x = (x ⊗ x') ⊗ (inv x ⊗ x)"
by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
also have "… = y"
by (simp add: x x')
finally have "x ⊗ x' ⊗ inv x ⊗ x = y".
with xcoset have "y ∈ {x ∈ carrier G. H #> x ∈ A} #> x" by auto }
ultimately show ?thesis
by auto
qed
qed auto
with assms show ?thesis
by (metis (full_types) factgroup_subgroup_union_char normal_imp_subgroup)
qed
lemma (in normal) factgroup_subgroup_union_factor:
assumes "subgroup A (G Mod H)"
shows "A = rcosets⇘G⦇carrier := ⋃A⦈⇙ H"
using assms subgroup.mem_carrier factgroup_subgroup_union_char by (fastforce simp: RCOSETS_def FactGroup_def)
section ‹Flattening the type of group carriers›
text ‹Flattening here means to convert the type of group elements from 'a set to 'a.
This is possible whenever the empty set is not an element of the group. By Jakob von Raumer›
definition flatten where
"flatten (G::('a set, 'b) monoid_scheme) rep = ⦇carrier=(rep ` (carrier G)),
monoid.mult=(λ x y. rep ((the_inv_into (carrier G) rep x) ⊗⇘G⇙ (the_inv_into (carrier G) rep y))),
one=rep 𝟭⇘G⇙ ⦈"
lemma flatten_set_group_hom:
assumes group: "group G"
assumes inj: "inj_on rep (carrier G)"
shows "rep ∈ hom G (flatten G rep)"
by (force simp add: hom_def flatten_def inj the_inv_into_f_f)
lemma flatten_set_group:
assumes "group G" "inj_on rep (carrier G)"
shows "group (flatten G rep)"
proof (rule groupI)
fix x y
assume "x ∈ carrier (flatten G rep)" and "y ∈ carrier (flatten G rep)"
then show "x ⊗⇘flatten G rep⇙ y ∈ carrier (flatten G rep)"
using assms group.surj_const_mult the_inv_into_f_f by (fastforce simp: flatten_def)
next
show "𝟭⇘flatten G rep⇙ ∈ carrier (flatten G rep)"
unfolding flatten_def by (simp add: assms group.is_monoid)
next
fix x y z
assume "x ∈ carrier (flatten G rep)" "y ∈ carrier (flatten G rep)" "z ∈ carrier (flatten G rep)"
then show "x ⊗⇘flatten G rep⇙ y ⊗⇘flatten G rep⇙ z = x ⊗⇘flatten G rep⇙ (y ⊗⇘flatten G rep⇙ z)"
by (auto simp: assms flatten_def group.is_monoid monoid.m_assoc monoid.m_closed the_inv_into_f_f)
next
fix x
assume x: "x ∈ carrier (flatten G rep)"
then show "𝟭⇘flatten G rep⇙ ⊗⇘flatten G rep⇙ x = x"
by (auto simp: assms group.is_monoid the_inv_into_f_f flatten_def)
then have "∃y∈carrier G. rep (y ⊗⇘G⇙ z) = rep 𝟭⇘G⇙" if "z ∈ carrier G" for z
by (metis ‹group G› group.l_inv_ex that)
with assms x show "∃y∈carrier (flatten G rep). y ⊗⇘flatten G rep⇙ x = 𝟭⇘flatten G rep⇙"
by (auto simp: flatten_def the_inv_into_f_f)
qed
lemma (in normal) flatten_set_group_mod_inj:
shows "inj_on (λU. SOME g. g ∈ U) (carrier (G Mod H))"
proof (rule inj_onI)
fix U V
assume U: "U ∈ carrier (G Mod H)" and V: "V ∈ carrier (G Mod H)"
then obtain g h where g: "U = H #> g" "g ∈ carrier G" and h: "V = H #> h" "h ∈ carrier G"
unfolding FactGroup_def RCOSETS_def by auto
hence notempty: "U ≠ {}" "V ≠ {}"
by (metis empty_iff is_subgroup rcos_self)+
assume "(SOME g. g ∈ U) = (SOME g. g ∈ V)"
with notempty have "(SOME g. g ∈ U) ∈ U ∩ V"
by (metis IntI ex_in_conv someI)
thus "U = V"
by (metis Int_iff g h is_subgroup repr_independence)
qed
lemma (in normal) flatten_set_group_mod:
shows "group (flatten (G Mod H) (λU. SOME g. g ∈ U))"
by (simp add: factorgroup_is_group flatten_set_group flatten_set_group_mod_inj)
lemma (in normal) flatten_set_group_mod_iso:
shows "(λU. SOME g. g ∈ U) ∈ iso (G Mod H) (flatten (G Mod H) (λU. SOME g. g ∈ U))"
proof -
have "(λU. SOME g. g ∈ U) ∈ hom (G Mod H) (flatten (G Mod H) (λU. SOME g. g ∈ U))"
using factorgroup_is_group flatten_set_group_hom flatten_set_group_mod_inj by blast
moreover
have "inj_on (λU. SOME g. g ∈ U) (carrier (G Mod H))"
using flatten_set_group_mod_inj by blast
ultimately show ?thesis
by (simp add: iso_def bij_betw_def flatten_def)
qed
end