--- a/src/HOL/Algebra/Coset.thy Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Coset.thy Wed Apr 03 12:55:27 2019 +0100
@@ -1061,6 +1061,26 @@
apply (simp add: kernel_def)
done
+lemma iso_kernel_image:
+ assumes "group G" "group H"
+ shows "f \<in> iso G H \<longleftrightarrow> f \<in> hom G H \<and> kernel G H f = {\<one>\<^bsub>G\<^esub>} \<and> f ` carrier G = carrier H"
+ (is "?lhs = ?rhs")
+proof (intro iffI conjI)
+ assume f: ?lhs
+ show "f \<in> hom G H"
+ using Group.iso_iff f by blast
+ show "kernel G H f = {\<one>\<^bsub>G\<^esub>}"
+ 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: "X \<in> carrier (G Mod kernel G H h)"
shows "X \<noteq> {}"
@@ -1083,7 +1103,7 @@
proof -
have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> N"
using \<open>N \<lhd> G\<close> group.rcos_self normal.axioms(2) normal_imp_subgroup
- subgroup.rcos_module_imp that by fastforce
+ subgroup.rcos_module_imp that by metis
with h have xy: "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> kernel G H h"
by blast
have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = h (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
@@ -1221,7 +1241,6 @@
using A G.inv_equality G.inv_inv by blast
qed
-(* NEW ========================================================================== *)
lemma (in group_hom) inj_iff_trivial_ker:
shows "inj_on h (carrier G) \<longleftrightarrow> kernel G H h = { \<one> }"
proof
@@ -1236,7 +1255,6 @@
using trivial_ker_imp_inj by simp
qed
-(* NEW ========================================================================== *)
lemma (in group_hom) induced_group_hom':
assumes "subgroup I G" shows "group_hom (G \<lparr> carrier := I \<rparr>) H h"
proof -
@@ -1247,13 +1265,11 @@
unfolding group_hom_def group_hom_axioms_def by auto
qed
-(* NEW ========================================================================== *)
lemma (in group_hom) inj_on_subgroup_iff_trivial_ker:
assumes "subgroup I G"
shows "inj_on h I \<longleftrightarrow> kernel (G \<lparr> carrier := I \<rparr>) H h = { \<one> }"
using group_hom.inj_iff_trivial_ker[OF induced_group_hom'[OF assms]] by simp
-(* NEW ========================================================================== *)
lemma set_mult_hom:
assumes "h \<in> hom G H" "I \<subseteq> carrier G" and "J \<subseteq> carrier G"
shows "h ` (I <#>\<^bsub>G\<^esub> J) = (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
@@ -1281,13 +1297,11 @@
qed
qed
-(* NEW ========================================================================== *)
corollary coset_hom:
assumes "h \<in> hom G H" "I \<subseteq> carrier G" "a \<in> carrier G"
shows "h ` (a <#\<^bsub>G\<^esub> I) = h a <#\<^bsub>H\<^esub> (h ` I)" and "h ` (I #>\<^bsub>G\<^esub> a) = (h ` I) #>\<^bsub>H\<^esub> h a"
unfolding l_coset_eq_set_mult r_coset_eq_set_mult using assms set_mult_hom[OF assms(1)] by auto
-(* NEW ========================================================================== *)
corollary (in group_hom) set_mult_ker_hom:
assumes "I \<subseteq> carrier G"
shows "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
@@ -1305,8 +1319,145 @@
using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+
qed
+subsubsection\<open>Trivial homomorphisms\<close>
-subsection \<open>Theorems about Factor Groups and Direct product\<close>
+definition trivial_homomorphism where
+ "trivial_homomorphism G H f \<equiv> f \<in> hom G H \<and> (\<forall>x \<in> carrier G. f x = one H)"
+
+lemma trivial_homomorphism_kernel:
+ "trivial_homomorphism G H f \<longleftrightarrow> f \<in> hom G H \<and> 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 \<longleftrightarrow> f \<in> hom G H \<and> f ` carrier G = {one H}"
+ by (auto simp: trivial_homomorphism_def) (metis one_closed rev_image_eqI)
+
+
+subsection \<open>Image kernel theorems\<close>
+
+lemma group_Int_image_ker:
+ assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and "inj_on (g \<circ> f) (carrier G)" "group G" "group H" "group K"
+ shows "(f ` carrier G) \<inter> (kernel H K g) = {\<one>\<^bsub>H\<^esub>}"
+proof -
+ have "(f ` carrier G) \<inter> (kernel H K g) \<subseteq> {\<one>\<^bsub>H\<^esub>}"
+ 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 \<in> f ` carrier G"
+ by (metis f \<open>group G\<close> \<open>group H\<close> group.is_monoid hom_one image_iff monoid.one_closed)
+ moreover have "one H \<in> kernel H K g"
+ apply (simp add: kernel_def)
+ using g group.is_monoid hom_one \<open>group H\<close> \<open>group K\<close> by blast
+ ultimately show ?thesis
+ by blast
+qed
+
+
+lemma group_sum_image_ker:
+ assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and eq: "(g \<circ> 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 \<subseteq> ?rhs"
+ apply (auto simp: kernel_def set_mult_def)
+ by (meson Group.group_def assms(5) f hom_carrier image_eqI monoid.m_closed subset_iff)
+ have "\<exists>x\<in>carrier G. \<exists>z. z \<in> carrier H \<and> g z = \<one>\<^bsub>K\<^esub> \<and> y = f x \<otimes>\<^bsub>H\<^esub> z"
+ if y: "y \<in> carrier H" for y
+ proof -
+ have "g y \<in> carrier K"
+ using g hom_carrier that by blast
+ with assms obtain x where x: "x \<in> carrier G" "(g \<circ> f) x = g y"
+ by (metis image_iff)
+ with assms have "inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y \<in> carrier H"
+ by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
+ moreover
+ have "g (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y) = \<one>\<^bsub>K\<^esub>"
+ proof -
+ have "inv\<^bsub>H\<^esub> f x \<in> carrier H"
+ by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
+ then have "g (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y) = g (inv\<^bsub>H\<^esub> f x) \<otimes>\<^bsub>K\<^esub> g y"
+ by (simp add: hom_mult [OF g] y)
+ also have "\<dots> = inv\<^bsub>K\<^esub> (g (f x)) \<otimes>\<^bsub>K\<^esub> 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 "\<dots> = \<one>\<^bsub>K\<^esub>"
+ using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2) by fastforce
+ finally show ?thesis .
+ qed
+ moreover
+ have "y = f x \<otimes>\<^bsub>H\<^esub> (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y)"
+ using x y
+ by (metis (no_types, hide_lams) assms(5) f group.inv_solve_left group.subgroup_self hom_carrier image_subset_iff subgroup_def that)
+ ultimately
+ show ?thesis
+ using x y by force
+ qed
+ then show "?rhs \<subseteq> ?lhs"
+ by (auto simp: kernel_def set_mult_def)
+qed
+
+
+lemma group_sum_ker_image:
+ assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and eq: "(g \<circ> 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 \<subseteq> ?rhs"
+ apply (auto simp: kernel_def set_mult_def)
+ by (meson Group.group_def \<open>group H\<close> f hom_carrier image_eqI monoid.m_closed subset_iff)
+ have "\<exists>w\<in>carrier H. \<exists>x \<in> carrier G. g w = \<one>\<^bsub>K\<^esub> \<and> y = w \<otimes>\<^bsub>H\<^esub> f x"
+ if y: "y \<in> carrier H" for y
+ proof -
+ have "g y \<in> carrier K"
+ using g hom_carrier that by blast
+ with assms obtain x where x: "x \<in> carrier G" "(g \<circ> f) x = g y"
+ by (metis image_iff)
+ with assms have carr: "(y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \<in> carrier H"
+ by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
+ moreover
+ have "g (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = \<one>\<^bsub>K\<^esub>"
+ proof -
+ have "inv\<^bsub>H\<^esub> f x \<in> carrier H"
+ by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
+ then have "g (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = g y \<otimes>\<^bsub>K\<^esub> g (inv\<^bsub>H\<^esub> f x)"
+ by (simp add: hom_mult [OF g] y)
+ also have "\<dots> = g y \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> (g (f x))"
+ 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 "\<dots> = \<one>\<^bsub>K\<^esub>"
+ using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2)
+ by (simp add: group.r_inv)
+ finally show ?thesis .
+ qed
+ moreover
+ have "y = (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \<otimes>\<^bsub>H\<^esub> f x"
+ using x y by (meson \<open>group H\<close> carr f group.inv_solve_right hom_carrier image_subset_iff)
+ ultimately
+ show ?thesis
+ using x y by force
+ qed
+ then show "?rhs \<subseteq> ?lhs"
+ by (force simp: kernel_def set_mult_def)
+qed
+
+lemma group_semidirect_sum_ker_image:
+ assumes "(g \<circ> f) \<in> iso G K" "f \<in> hom G H" "g \<in> hom H K" "group G" "group H" "group K"
+ shows "(kernel H K g) \<inter> (f ` carrier G) = {\<one>\<^bsub>H\<^esub>}"
+ "kernel H K g <#>\<^bsub>H\<^esub> (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 \<in> hom G H" and g: "g \<in> hom H K" and iso: "(g \<circ> f) \<in> iso G K"
+ and "group G" "group H" "group K"
+ shows "(f ` carrier G) \<inter> (kernel H K g) = {\<one>\<^bsub>H\<^esub>}"
+ "f ` carrier G <#>\<^bsub>H\<^esub> (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 \<open>Factor Groups and Direct product\<close>
lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
assumes "group K"
--- a/src/HOL/Algebra/Elementary_Groups.thy Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Elementary_Groups.thy Wed Apr 03 12:55:27 2019 +0100
@@ -5,7 +5,7 @@
*)
theory Elementary_Groups
-imports Generated_Groups
+imports Generated_Groups Multiplicative_Group "HOL-Library.Infinite_Set"
begin
subsection\<open>Direct sum/product lemmas\<close>
@@ -379,4 +379,289 @@
"x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G"
by (rule homI) (auto simp: int_pow_mult)
+subsection\<open>Additive group of integers modulo n (n = 0 gives just the integers)\<close>
+
+definition integer_mod_group :: "nat \<Rightarrow> int monoid"
+ where
+ "integer_mod_group n \<equiv>
+ if n = 0 then integer_group
+ else \<lparr>carrier = {0..<int n}, monoid.mult = (\<lambda>x y. (x+y) mod int n), one = 0\<rparr>"
+
+lemma carrier_integer_mod_group:
+ "carrier(integer_mod_group n) = (if n=0 then UNIV else {0..<int n})"
+ by (simp add: integer_mod_group_def)
+
+lemma one_integer_mod_group[simp]: "one(integer_mod_group n) = 0"
+ by (simp add: integer_mod_group_def)
+
+lemma mult_integer_mod_group[simp]: "monoid.mult(integer_mod_group n) = (\<lambda>x y. (x + y) mod int n)"
+ by (simp add: integer_mod_group_def integer_group_def)
+
+lemma group_integer_mod_group [simp]: "group (integer_mod_group n)"
+proof -
+ have *: "\<exists>y\<ge>0. y < int n \<and> (y + x) mod int n = 0" if "x < int n" "0 \<le> x" for x
+ proof (cases "x=0")
+ case False
+ with that show ?thesis
+ by (rule_tac x="int n - x" in exI) auto
+ qed (use that in auto)
+ show ?thesis
+ apply (rule groupI)
+ apply (auto simp: integer_mod_group_def Bex_def *, presburger+)
+ done
+qed
+
+lemma inv_integer_mod_group[simp]:
+ "x \<in> carrier (integer_mod_group n) \<Longrightarrow> m_inv(integer_mod_group n) x = (-x) mod int n"
+ by (rule group.inv_equality [OF group_integer_mod_group]) (auto simp: integer_mod_group_def add.commute mod_add_right_eq)
+
+
+lemma pow_integer_mod_group [simp]:
+ fixes m::nat
+ shows "pow (integer_mod_group n) x m = (int m * x) mod int n"
+proof (cases "n=0")
+ case False
+ show ?thesis
+ by (induction m) (auto simp: add.commute mod_add_right_eq distrib_left mult.commute)
+qed (simp add: integer_mod_group_def)
+
+lemma int_pow_integer_mod_group:
+ "pow (integer_mod_group n) x m = (m * x) mod int n"
+proof -
+ have "inv\<^bsub>integer_mod_group n\<^esub> (- (m * x) mod int n) = m * x mod int n"
+ by (simp add: carrier_integer_mod_group mod_minus_eq)
+ then show ?thesis
+ by (simp add: int_pow_def2)
+qed
+
+lemma abelian_integer_mod_group [simp]: "comm_group(integer_mod_group n)"
+ by (simp add: add.commute group.group_comm_groupI)
+
+lemma integer_mod_group_0 [simp]: "0 \<in> carrier(integer_mod_group n)"
+ by (simp add: integer_mod_group_def)
+
+lemma integer_mod_group_1 [simp]: "1 \<in> carrier(integer_mod_group n) \<longleftrightarrow> (n \<noteq> 1)"
+ by (auto simp: integer_mod_group_def)
+
+lemma trivial_integer_mod_group: "trivial_group(integer_mod_group n) \<longleftrightarrow> n = 1"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (simp add: trivial_group_def carrier_integer_mod_group set_eq_iff split: if_split_asm) (presburger+)
+next
+ assume ?rhs
+ then show ?lhs
+ by (force simp: trivial_group_def carrier_integer_mod_group)
+qed
+
+
+subsection\<open>Cyclic groups\<close>
+
+lemma (in group) subgroup_of_powers:
+ "x \<in> carrier G \<Longrightarrow> subgroup (range (\<lambda>n::int. x [^] n)) G"
+ apply (auto simp: subgroup_def image_iff simp flip: int_pow_mult int_pow_neg)
+ apply (metis group.int_pow_diff int_pow_closed is_group r_inv)
+ done
+
+lemma (in group) carrier_subgroup_generated_by_singleton:
+ assumes "x \<in> carrier G"
+ shows "carrier(subgroup_generated G {x}) = (range (\<lambda>n::int. x [^] n))"
+proof
+ show "carrier (subgroup_generated G {x}) \<subseteq> range (\<lambda>n::int. x [^] n)"
+ proof (rule subgroup_generated_minimal)
+ show "subgroup (range (\<lambda>n::int. x [^] n)) G"
+ using assms subgroup_of_powers by blast
+ show "{x} \<subseteq> range (\<lambda>n::int. x [^] n)"
+ by clarify (metis assms int_pow_1 range_eqI)
+ qed
+ have x: "x \<in> carrier (subgroup_generated G {x})"
+ using assms subgroup_generated_subset_carrier_subset by auto
+ show "range (\<lambda>n::int. x [^] n) \<subseteq> carrier (subgroup_generated G {x})"
+ proof clarify
+ fix n :: "int"
+ show "x [^] n \<in> carrier (subgroup_generated G {x})"
+ by (simp add: x subgroup_int_pow_closed subgroup_subgroup_generated)
+ qed
+qed
+
+
+definition cyclic_group
+ where "cyclic_group G \<equiv> \<exists>x \<in> carrier G. subgroup_generated G {x} = G"
+
+lemma (in group) cyclic_group:
+ "cyclic_group G \<longleftrightarrow> (\<exists>x \<in> carrier G. carrier G = range (\<lambda>n::int. x [^] n))"
+proof -
+ have "\<And>x. \<lbrakk>x \<in> carrier G; carrier G = range (\<lambda>n::int. x [^] n)\<rbrakk>
+ \<Longrightarrow> \<exists>x\<in>carrier G. subgroup_generated G {x} = G"
+ by (rule_tac x=x in bexI) (auto simp: generate_pow subgroup_generated_def intro!: monoid.equality)
+ then show ?thesis
+ unfolding cyclic_group_def
+ using carrier_subgroup_generated_by_singleton by fastforce
+qed
+
+lemma cyclic_integer_group [simp]: "cyclic_group integer_group"
+proof -
+ have *: "int n \<in> generate integer_group {1}" for n
+ proof (induction n)
+ case 0
+ then show ?case
+ using generate.simps by force
+ next
+ case (Suc n)
+ then show ?case
+ by simp (metis generate.simps insert_subset integer_group_def monoid.simps(1) subsetI)
+ qed
+ have **: "i \<in> generate integer_group {1}" for i
+ proof (cases i rule: int_cases)
+ case (nonneg n)
+ then show ?thesis
+ by (simp add: *)
+ next
+ case (neg n)
+ then have "-i \<in> generate integer_group {1}"
+ by (metis "*" add.inverse_inverse)
+ then have "- (-i) \<in> generate integer_group {1}"
+ by (metis UNIV_I group.generate_m_inv_closed group_integer_group integer_group_def inv_integer_group partial_object.select_convs(1) subsetI)
+ then show ?thesis
+ by simp
+ qed
+ show ?thesis
+ unfolding cyclic_group_def
+ by (rule_tac x=1 in bexI)
+ (auto simp: carrier_subgroup_generated ** intro: monoid.equality)
+qed
+
+lemma nontrivial_integer_group [simp]: "\<not> trivial_group integer_group"
+ using integer_mod_group_def trivial_integer_mod_group by presburger
+
+
+lemma (in group) cyclic_imp_abelian_group:
+ "cyclic_group G \<Longrightarrow> comm_group G"
+ apply (auto simp: cyclic_group comm_group_def is_group intro!: monoid_comm_monoidI)
+ apply (metis add.commute int_pow_mult rangeI)
+ done
+
+lemma trivial_imp_cyclic_group:
+ "trivial_group G \<Longrightarrow> cyclic_group G"
+ by (metis cyclic_group_def group.subgroup_generated_group_carrier insertI1 trivial_group_def)
+
+lemma (in group) cyclic_group_alt:
+ "cyclic_group G \<longleftrightarrow> (\<exists>x. subgroup_generated G {x} = G)"
+proof safe
+ fix x
+ assume *: "subgroup_generated G {x} = G"
+ show "cyclic_group G"
+ proof (cases "x \<in> carrier G")
+ case True
+ then show ?thesis
+ using \<open>subgroup_generated G {x} = G\<close> cyclic_group_def by blast
+ next
+ case False
+ then show ?thesis
+ by (metis "*" Int_empty_right Int_insert_right_if0 carrier_subgroup_generated generate_empty trivial_group trivial_imp_cyclic_group)
+ qed
+qed (auto simp: cyclic_group_def)
+
+lemma (in group) cyclic_group_generated:
+ "cyclic_group (subgroup_generated G {x})"
+ using group.cyclic_group_alt group_subgroup_generated subgroup_generated2 by blast
+
+lemma (in group) cyclic_group_epimorphic_image:
+ assumes "h \<in> epi G H" "cyclic_group G" "group H"
+ shows "cyclic_group H"
+proof -
+ interpret h: group_hom
+ using assms
+ by (simp add: group_hom_def group_hom_axioms_def is_group epi_def)
+ obtain x where "x \<in> carrier G" and x: "carrier G = range (\<lambda>n::int. x [^] n)" and eq: "carrier H = h ` carrier G"
+ using assms by (auto simp: cyclic_group epi_def)
+ have "h ` carrier G = range (\<lambda>n::int. h x [^]\<^bsub>H\<^esub> n)"
+ by (metis (no_types, lifting) \<open>x \<in> carrier G\<close> h.hom_int_pow image_cong image_image x)
+ then show ?thesis
+ using \<open>x \<in> carrier G\<close> eq h.cyclic_group by blast
+qed
+
+lemma isomorphic_group_cyclicity:
+ "\<lbrakk>G \<cong> H; group G; group H\<rbrakk> \<Longrightarrow> cyclic_group G \<longleftrightarrow> cyclic_group H"
+ by (meson ex_in_conv group.cyclic_group_epimorphic_image group.iso_sym is_iso_def iso_iff_mon_epi)
+
+
+lemma (in group)
+ assumes "x \<in> carrier G"
+ shows finite_cyclic_subgroup:
+ "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> x [^] n = \<one>)" (is "?fin \<longleftrightarrow> ?nat1")
+ and infinite_cyclic_subgroup:
+ "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>m n::nat. x [^] m = x [^] n \<longrightarrow> m = n)" (is "\<not> ?fin \<longleftrightarrow> ?nateq")
+ and finite_cyclic_subgroup_int:
+ "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>i::int. i \<noteq> 0 \<and> x [^] i = \<one>)" (is "?fin \<longleftrightarrow> ?int1")
+ and infinite_cyclic_subgroup_int:
+ "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>i j::int. x [^] i = x [^] j \<longrightarrow> i = j)" (is "\<not> ?fin \<longleftrightarrow> ?inteq")
+proof -
+ have 1: "\<not> ?fin" if ?nateq
+ proof -
+ have "infinite (range (\<lambda>n::nat. x [^] n))"
+ using that range_inj_infinite [of "(\<lambda>n::nat. x [^] n)"] by (auto simp: inj_on_def)
+ moreover have "range (\<lambda>n::nat. x [^] n) \<subseteq> range (\<lambda>i::int. x [^] i)"
+ apply clarify
+ by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
+ ultimately show ?thesis
+ using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
+ qed
+ have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
+ using eq [of "int m" "int n"]
+ by (simp add: int_pow_int mn)
+ have 3: ?nat1 if non: "\<not> ?inteq"
+ proof -
+ obtain i j::int where eq: "x [^] i = x [^] j" and "i \<noteq> j"
+ using non by auto
+ show ?thesis
+ proof (cases i j rule: linorder_cases)
+ case less
+ then have [simp]: "x [^] (j - i) = \<one>"
+ by (simp add: eq assms int_pow_diff)
+ show ?thesis
+ using less by (rule_tac x="nat (j-i)" in exI) auto
+ next
+ case greater
+ then have [simp]: "x [^] (i - j) = \<one>"
+ by (simp add: eq assms int_pow_diff)
+ then show ?thesis
+ using greater by (rule_tac x="nat (i-j)" in exI) auto
+ qed (use \<open>i \<noteq> j\<close> in auto)
+ qed
+ have 4: "\<exists>i::int. (i \<noteq> 0) \<and> x [^] i = \<one>" if "n \<noteq> 0" "x [^] n = \<one>" for n::nat
+ apply (rule_tac x="int n" in exI)
+ by (simp add: int_pow_int that)
+ have 5: "finite (carrier (subgroup_generated G {x}))" if "i \<noteq> 0" and 1: "x [^] i = \<one>" for i::int
+ proof -
+ obtain n::nat where n: "n > 0" "x [^] n = \<one>"
+ using "1" "3" \<open>i \<noteq> 0\<close> by fastforce
+ have "x [^] a \<in> ([^]) x ` {0..<n}" for a::int
+ proof
+ show "x [^] a = x [^] nat (a mod int n)"
+ using n
+ by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
+ show "nat (a mod int n) \<in> {0..<n}"
+ using n apply (simp add: split: split_nat)
+ using Euclidean_Division.pos_mod_bound by presburger
+ qed
+ then have "carrier (subgroup_generated G {x}) \<subseteq> ([^]) x ` {0..<n}"
+ using carrier_subgroup_generated_by_singleton [OF assms] by auto
+ then show ?thesis
+ using finite_surj by blast
+ qed
+ show "?fin \<longleftrightarrow> ?nat1" "\<not> ?fin \<longleftrightarrow> ?nateq" "?fin \<longleftrightarrow> ?int1" "\<not> ?fin \<longleftrightarrow> ?inteq"
+ using 1 2 3 4 5 by meson+
+qed
+
+lemma (in group) finite_cyclic_subgroup_order:
+ "x \<in> carrier G \<Longrightarrow> finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x \<noteq> 0"
+ by (simp add: finite_cyclic_subgroup ord_eq_0)
+
+lemma (in group) infinite_cyclic_subgroup_order:
+ "x \<in> carrier G \<Longrightarrow> infinite (carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x = 0"
+ by (simp add: finite_cyclic_subgroup_order)
+
+
end
--- a/src/HOL/Algebra/Generated_Groups.thy Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy Wed Apr 03 12:55:27 2019 +0100
@@ -2,12 +2,14 @@
Author: Paulo Emílio de Vilhena
*)
+section \<open>Generated Groups\<close>
+
theory Generated_Groups
imports Group Coset
begin
-section \<open>Generated Groups\<close>
+subsection \<open>Generated Groups\<close>
inductive_set generate :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
for G and H where
@@ -17,7 +19,7 @@
| eng: "h1 \<in> generate G H \<Longrightarrow> h2 \<in> generate G H \<Longrightarrow> h1 \<otimes>\<^bsub>G\<^esub> h2 \<in> generate G H"
-subsection \<open>Basic Properties\<close>
+subsubsection \<open>Basic Properties\<close>
lemma (in group) generate_consistent:
assumes "K \<subseteq> H" "subgroup H G" shows "generate (G \<lparr> carrier := H \<rparr>) K = generate G K"
@@ -195,9 +197,9 @@
qed
-section \<open>Derived Subgroup\<close>
+subsection \<open>Derived Subgroup\<close>
-subsection \<open>Definitions\<close>
+subsubsection \<open>Definitions\<close>
abbreviation derived_set :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
where "derived_set G H \<equiv>
@@ -207,7 +209,7 @@
"derived G H = generate G (derived_set G H)"
-subsection \<open>Basic Properties\<close>
+subsubsection \<open>Basic Properties\<close>
lemma (in group) derived_set_incl:
assumes "K \<subseteq> H" "subgroup H G" shows "derived_set G K \<subseteq> H"
@@ -444,7 +446,7 @@
using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto)
-subsection \<open>Generated subgroup of a group\<close>
+subsubsection \<open>Generated subgroup of a group\<close>
definition subgroup_generated :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> ('a, 'b) monoid_scheme"
where "subgroup_generated G S = G\<lparr>carrier := generate G (carrier G \<inter> S)\<rparr>"
@@ -600,4 +602,114 @@
"kernel G (subgroup_generated H S) f = kernel G H f"
by (simp add: kernel_def)
+subsection \<open>And homomorphisms\<close>
+
+lemma (in group) hom_from_subgroup_generated:
+ "h \<in> hom G H \<Longrightarrow> h \<in> hom(subgroup_generated G A) H"
+ apply (simp add: hom_def carrier_subgroup_generated Pi_iff)
+ apply (metis group.generate_in_carrier inf_le1 is_group)
+ done
+
+lemma hom_into_subgroup:
+ "\<lbrakk>h \<in> hom G G'; h ` (carrier G) \<subseteq> H\<rbrakk> \<Longrightarrow> h \<in> hom G (subgroup_generated G' H)"
+ by (auto simp: hom_def carrier_subgroup_generated Pi_iff generate.incl image_subset_iff)
+
+lemma hom_into_subgroup_eq_gen:
+ "group G \<Longrightarrow>
+ h \<in> hom K (subgroup_generated G H)
+ \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> carrier(subgroup_generated G H)"
+ using group.carrier_subgroup_generated_subset [of G H] by (auto simp: hom_def)
+
+lemma hom_into_subgroup_eq:
+ "\<lbrakk>subgroup H G; group G\<rbrakk>
+ \<Longrightarrow> (h \<in> hom K (subgroup_generated G H) \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> H)"
+ by (simp add: hom_into_subgroup_eq_gen image_subset_iff subgroup.carrier_subgroup_generated_subgroup)
+
+lemma (in group_hom) hom_between_subgroups:
+ assumes "h ` A \<subseteq> B"
+ shows "h \<in> hom (subgroup_generated G A) (subgroup_generated H B)"
+proof -
+ have [simp]: "group G" "group H"
+ by (simp_all add: G.is_group H.is_group)
+ have "x \<in> generate G (carrier G \<inter> A) \<Longrightarrow> h x \<in> generate H (carrier H \<inter> B)" for x
+ proof (induction x rule: generate.induct)
+ case (incl h)
+ then show ?case
+ by (meson IntE IntI assms generate.incl hom_closed image_subset_iff)
+ next
+ case (inv h)
+ then show ?case
+ by (metis G.inv_closed G.inv_inv IntE IntI assms generate.simps hom_inv image_subset_iff local.inv_closed)
+ next
+ case (eng h1 h2)
+ then show ?case
+ by (metis G.generate_in_carrier generate.simps inf.cobounded1 local.hom_mult)
+ qed (auto simp: generate.intros)
+ then have "h ` carrier (subgroup_generated G A) \<subseteq> carrier (subgroup_generated H B)"
+ using group.carrier_subgroup_generated_subset [of G A]
+ by (auto simp: carrier_subgroup_generated)
+ then show ?thesis
+ by (simp add: hom_into_subgroup_eq_gen group.hom_from_subgroup_generated homh)
+qed
+
+lemma (in group_hom) subgroup_generated_by_image:
+ assumes "S \<subseteq> carrier G"
+ shows "carrier (subgroup_generated H (h ` S)) = h ` (carrier(subgroup_generated G S))"
+proof
+ have "x \<in> generate H (carrier H \<inter> h ` S) \<Longrightarrow> x \<in> h ` generate G (carrier G \<inter> S)" for x
+ proof (erule generate.induct)
+ show "\<one>\<^bsub>H\<^esub> \<in> h ` generate G (carrier G \<inter> S)"
+ using generate.one by force
+ next
+ fix f
+ assume "f \<in> carrier H \<inter> h ` S"
+ with assms show "f \<in> h ` generate G (carrier G \<inter> S)" "inv\<^bsub>H\<^esub> f \<in> h ` generate G (carrier G \<inter> S)"
+ apply (auto simp: Int_absorb1 generate.incl)
+ apply (metis generate.simps hom_inv imageI subsetCE)
+ done
+ next
+ fix h1 h2
+ assume
+ "h1 \<in> generate H (carrier H \<inter> h ` S)" "h1 \<in> h ` generate G (carrier G \<inter> S)"
+ "h2 \<in> generate H (carrier H \<inter> h ` S)" "h2 \<in> h ` generate G (carrier G \<inter> S)"
+ then show "h1 \<otimes>\<^bsub>H\<^esub> h2 \<in> h ` generate G (carrier G \<inter> S)"
+ using H.subgroupE(4) group.generate_is_subgroup subgroup_img_is_subgroup
+ by (simp add: G.generate_is_subgroup)
+ qed
+ then
+ show "carrier (subgroup_generated H (h ` S)) \<subseteq> h ` carrier (subgroup_generated G S)"
+ by (auto simp: carrier_subgroup_generated)
+next
+ have "h ` S \<subseteq> carrier H"
+ by (metis (no_types) assms hom_closed image_subset_iff subsetCE)
+ then show "h ` carrier (subgroup_generated G S) \<subseteq> carrier (subgroup_generated H (h ` S))"
+ apply (clarsimp simp: carrier_subgroup_generated)
+ by (metis Int_absorb1 assms generate_img imageI)
+qed
+
+lemma (in group_hom) iso_between_subgroups:
+ assumes "h \<in> iso G H" "S \<subseteq> carrier G" "h ` S = T"
+ shows "h \<in> iso (subgroup_generated G S) (subgroup_generated H T)"
+ using assms
+ by (metis G.carrier_subgroup_generated_subset Group.iso_iff hom_between_subgroups inj_on_subset subgroup_generated_by_image subsetI)
+
+lemma (in group) subgroup_generated_group_carrier:
+ "subgroup_generated G (carrier G) = G"
+proof (rule monoid.equality)
+ show "carrier (subgroup_generated G (carrier G)) = carrier G"
+ by (simp add: subgroup.carrier_subgroup_generated_subgroup subgroup_self)
+qed (auto simp: subgroup_generated_def)
+
+lemma iso_onto_image:
+ assumes "group G" "group H"
+ shows
+ "f \<in> iso G (subgroup_generated H (f ` carrier G)) \<longleftrightarrow> f \<in> hom G H \<and> inj_on f (carrier G)"
+ using assms
+ apply (auto simp: iso_def bij_betw_def hom_into_subgroup_eq_gen carrier_subgroup_generated hom_carrier generate.incl Int_absorb1 Int_absorb2)
+ by (metis group.generateI group.subgroupE(1) group.subgroup_self group_hom.generate_img group_hom.intro group_hom_axioms.intro)
+
+lemma (in group) iso_onto_image:
+ "group H \<Longrightarrow> f \<in> iso G (subgroup_generated H (f ` carrier G)) \<longleftrightarrow> f \<in> mon G H"
+ by (simp add: mon_def epi_def hom_into_subgroup_eq_gen iso_onto_image)
+
end
\ No newline at end of file
--- a/src/HOL/Algebra/Group.thy Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Group.thy Wed Apr 03 12:55:27 2019 +0100
@@ -186,7 +186,10 @@
locale group = monoid +
assumes Units: "carrier G <= Units G"
-lemma (in group) is_group: "group G" by (rule group_axioms)
+lemma (in group) is_group [iff]: "group G" by (rule group_axioms)
+
+lemma (in group) is_monoid [iff]: "monoid G"
+ by (rule monoid_axioms)
theorem groupI:
fixes G (structure)
@@ -825,6 +828,9 @@
lemma mult_DirProd [simp]: "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
by (simp add: DirProd_def)
+lemma mult_DirProd': "x \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> y = (fst x \<otimes>\<^bsub>G\<^esub> fst y, snd x \<otimes>\<^bsub>H\<^esub> snd y)"
+ by (subst mult_DirProd [symmetric]) simp
+
lemma DirProd_assoc: "(G \<times>\<times> H \<times>\<times> I) = (G \<times>\<times> (H \<times>\<times> I))"
by auto
@@ -858,7 +864,7 @@
ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
qed
-subsection \<open>Homomorphisms and Isomorphisms\<close>
+subsection \<open>Homomorphisms (mono and epi) and Isomorphisms\<close>
definition
hom :: "_ => _ => ('a => 'b) set" where
@@ -923,6 +929,14 @@
corollary iso_refl [simp]: "G \<cong> G"
using iso_set_refl unfolding is_iso_def by auto
+lemma iso_iff:
+ "h \<in> iso G H \<longleftrightarrow> h \<in> hom G H \<and> h ` (carrier G) = carrier H \<and> inj_on h (carrier G)"
+ by (auto simp: iso_def hom_def bij_betw_def)
+
+lemma iso_imp_homomorphism:
+ "h \<in> iso G H \<Longrightarrow> h \<in> hom G H"
+ by (simp add: iso_iff)
+
lemma trivial_hom:
"group H \<Longrightarrow> (\<lambda>x. one H) \<in> hom G H"
by (auto simp: hom_def Group.group_def)
@@ -965,7 +979,6 @@
by (simp add: Group.iso_def bij_betw_inv_into h)
qed
-
corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
using iso_set_sym unfolding is_iso_def by auto
@@ -979,6 +992,50 @@
lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
using bij_betw_same_card unfolding is_iso_def iso_def by auto
+lemma iso_finite: "G \<cong> H \<Longrightarrow> finite(carrier G) \<longleftrightarrow> finite(carrier H)"
+ by (auto simp: is_iso_def iso_def bij_betw_finite)
+
+lemma mon_compose:
+ "\<lbrakk>f \<in> mon G H; g \<in> mon H K\<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> mon G K"
+ by (auto simp: mon_def intro: hom_compose comp_inj_on inj_on_subset [OF _ hom_carrier])
+
+lemma mon_compose_rev:
+ "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> mon G K\<rbrakk> \<Longrightarrow> f \<in> mon G H"
+ using inj_on_imageI2 by (auto simp: mon_def)
+
+lemma epi_compose:
+ "\<lbrakk>f \<in> epi G H; g \<in> epi H K\<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> epi G K"
+ using hom_compose by (force simp: epi_def hom_compose simp flip: image_image)
+
+lemma epi_compose_rev:
+ "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> epi G K\<rbrakk> \<Longrightarrow> g \<in> epi H K"
+ by (fastforce simp: epi_def hom_def Pi_iff image_def set_eq_iff)
+
+lemma iso_compose_rev:
+ "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> iso G K\<rbrakk> \<Longrightarrow> f \<in> mon G H \<and> g \<in> epi H K"
+ unfolding iso_iff_mon_epi using mon_compose_rev epi_compose_rev by blast
+
+lemma epi_iso_compose_rev:
+ assumes "f \<in> epi G H" "g \<in> hom H K" "(g \<circ> f) \<in> iso G K"
+ shows "f \<in> iso G H \<and> g \<in> iso H K"
+proof
+ show "f \<in> iso G H"
+ by (metis (no_types, lifting) assms epi_def iso_compose_rev iso_iff_mon_epi mem_Collect_eq)
+ then have "f \<in> hom G H \<and> bij_betw f (carrier G) (carrier H)"
+ using Group.iso_def \<open>f \<in> Group.iso G H\<close> by blast
+ then have "bij_betw g (carrier H) (carrier K)"
+ using Group.iso_def assms(3) bij_betw_comp_iff by blast
+ then show "g \<in> iso H K"
+ using Group.iso_def assms(2) by blast
+qed
+
+lemma mon_left_invertible:
+ "\<lbrakk>f \<in> hom G H; \<And>x. x \<in> carrier G \<Longrightarrow> g(f x) = x\<rbrakk> \<Longrightarrow> f \<in> mon G H"
+ by (simp add: mon_def inj_on_def) metis
+
+lemma epi_right_invertible:
+ "\<lbrakk>g \<in> hom H G; f \<in> carrier G \<rightarrow> carrier H; \<And>x. x \<in> carrier G \<Longrightarrow> g(f x) = x\<rbrakk> \<Longrightarrow> g \<in> epi H G"
+ by (force simp: Pi_iff epi_iff_subset image_subset_iff_funcset subset_iff)
lemma (in monoid) hom_imp_img_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "h \<in> hom G H"
@@ -1109,6 +1166,43 @@
ultimately show ?thesis by simp
qed
+subsubsection \<open>HOL Light's concept of an isomorphism pair\<close>
+
+definition group_isomorphisms
+ where
+ "group_isomorphisms G H f g \<equiv>
+ f \<in> hom G H \<and> g \<in> hom H G \<and>
+ (\<forall>x \<in> carrier G. g(f x) = x) \<and>
+ (\<forall>y \<in> carrier H. f(g y) = y)"
+
+lemma group_isomorphisms_sym: "group_isomorphisms G H f g \<Longrightarrow> group_isomorphisms H G g f"
+ by (auto simp: group_isomorphisms_def)
+
+lemma group_isomorphisms_imp_iso: "group_isomorphisms G H f g \<Longrightarrow> f \<in> iso G H"
+by (auto simp: iso_def inj_on_def image_def group_isomorphisms_def hom_def bij_betw_def Pi_iff, metis+)
+
+lemma (in group) iso_iff_group_isomorphisms:
+ "f \<in> iso G H \<longleftrightarrow> (\<exists>g. group_isomorphisms G H f g)"
+proof safe
+ show "\<exists>g. group_isomorphisms G H f g" if "f \<in> Group.iso G H"
+ unfolding group_isomorphisms_def
+ proof (intro exI conjI)
+ let ?g = "inv_into (carrier G) f"
+ show "\<forall>x\<in>carrier G. ?g (f x) = x"
+ by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_left mem_Collect_eq that)
+ show "\<forall>y\<in>carrier H. f (?g y) = y"
+ by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_right mem_Collect_eq that)
+ qed (use Group.iso_def iso_set_sym that in \<open>blast+\<close>)
+next
+ fix g
+ assume "group_isomorphisms G H f g"
+ then show "f \<in> Group.iso G H"
+ by (auto simp: iso_def group_isomorphisms_def hom_in_carrier intro: bij_betw_byWitness)
+qed
+
+
+subsubsection \<open>Involving direct products\<close>
+
lemma DirProd_commute_iso_set:
shows "(\<lambda>(x,y). (y,x)) \<in> iso (G \<times>\<times> H) (H \<times>\<times> G)"
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
@@ -1141,6 +1235,53 @@
shows "G \<times>\<times> H \<cong> G2 \<times>\<times> I"
using DirProd_iso_set_trans assms unfolding is_iso_def by blast
+lemma hom_pairwise: "f \<in> hom G (DirProd H K) \<longleftrightarrow> (fst \<circ> f) \<in> hom G H \<and> (snd \<circ> f) \<in> hom G K"
+ apply (auto simp: hom_def mult_DirProd' dest: Pi_mem)
+ apply (metis Product_Type.mem_Times_iff comp_eq_dest_lhs funcset_mem)
+ by (metis mult_DirProd prod.collapse)
+
+lemma hom_paired:
+ "(\<lambda>x. (f x,g x)) \<in> hom G (DirProd H K) \<longleftrightarrow> f \<in> hom G H \<and> g \<in> hom G K"
+ by (simp add: hom_pairwise o_def)
+
+lemma hom_paired2:
+ assumes "group G" "group H"
+ shows "(\<lambda>(x,y). (f x,g y)) \<in> hom (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> hom G G' \<and> g \<in> hom H H'"
+ using assms
+ by (fastforce simp: hom_def Pi_def dest!: group.is_monoid)
+
+lemma image_paired_Times:
+ "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+ by auto
+
+lemma iso_paired2:
+ assumes "group G" "group H"
+ shows "(\<lambda>(x,y). (f x,g y)) \<in> iso (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> iso G G' \<and> g \<in> iso H H'"
+ using assms
+ by (fastforce simp add: iso_def inj_on_def bij_betw_def hom_paired2 image_paired_Times
+ times_eq_iff group_def monoid.carrier_not_empty)
+
+lemma hom_of_fst:
+ assumes "group H"
+ shows "(f \<circ> fst) \<in> hom (DirProd G H) K \<longleftrightarrow> f \<in> hom G K"
+proof -
+ interpret group H
+ by (rule assms)
+ show ?thesis
+ using one_closed by (auto simp: hom_def Pi_def)
+qed
+
+lemma hom_of_snd:
+ assumes "group G"
+ shows "(f \<circ> snd) \<in> hom (DirProd G H) K \<longleftrightarrow> f \<in> hom H K"
+proof -
+ interpret group G
+ by (rule assms)
+ show ?thesis
+ using one_closed by (auto simp: hom_def Pi_def)
+qed
+
+
subsection\<open>The locale for a homomorphism between two groups\<close>
text\<open>Basis for homomorphism proofs: we assume two groups \<^term>\<open>G\<close> and
@@ -1172,7 +1313,8 @@
proof -
have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
by (simp add: hom_mult [symmetric] del: hom_mult)
- then show ?thesis by (simp del: r_one)
+ then show ?thesis
+ by (metis H.Units_eq H.Units_l_cancel H.one_closed local.one_closed)
qed
lemma hom_one:
@@ -1383,6 +1525,11 @@
finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
qed
+lemma (in comm_group) hom_group_mult:
+ assumes "f \<in> hom H G" "g \<in> hom H G"
+ shows "(\<lambda>x. f x \<otimes>\<^bsub>G\<^esub> g x) \<in> hom H G"
+ using assms by (auto simp: hom_def Pi_def m_ac)
+
lemma (in comm_group) hom_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "h \<in> hom G H"
shows "comm_group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
@@ -1465,10 +1612,6 @@
"subgroup H G ==> group (G\<lparr>carrier := H\<rparr>)"
by (erule subgroup.subgroup_is_group) (rule group_axioms)
-lemma (in group) is_monoid [intro, simp]:
- "monoid G"
- by (auto intro: monoid.intro m_assoc)
-
lemma (in group) subgroup_mult_equality:
"\<lbrakk> subgroup H G; h1 \<in> H; h2 \<in> H \<rbrakk> \<Longrightarrow> h1 \<otimes>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h2 = h1 \<otimes> h2"
unfolding subgroup_def by simp