--- a/src/HOL/Algebra/Coset.thy Mon Jan 28 18:36:50 2019 -0500
+++ b/src/HOL/Algebra/Coset.thy Tue Jan 29 15:26:43 2019 +0000
@@ -38,6 +38,9 @@
normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) where
"H \<lhd> G \<equiv> normal H G"
+lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G"
+ by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+
(*Next two lemmas contributed by Martin Baillon.*)
lemma l_coset_eq_set_mult:
@@ -196,6 +199,17 @@
ultimately show ?thesis by blast
qed
+lemma (in group_hom) inj_on_one_iff:
+ "inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
+using G.solve_equation G.subgroup_self by (force simp: inj_on_def)
+
+lemma inj_on_one_iff':
+ "\<lbrakk>h \<in> hom G H; group G; group H\<rbrakk> \<Longrightarrow> inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
+ using group_hom.inj_on_one_iff group_hom.intro group_hom_axioms.intro by blast
+
+lemma (in group_hom) iso_iff: "h \<in> iso G H \<longleftrightarrow> carrier H \<subseteq> h ` carrier G \<and> (\<forall>x\<in>carrier G. h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)"
+ by (auto simp: iso_def bij_betw_def inj_on_one_iff)
+
lemma (in group) repr_independence:
assumes "y \<in> H #> x" "x \<in> carrier G" "subgroup H G"
shows "H #> x = H #> y" using assms
--- a/src/HOL/Algebra/Generated_Groups.thy Mon Jan 28 18:36:50 2019 -0500
+++ b/src/HOL/Algebra/Generated_Groups.thy Tue Jan 29 15:26:43 2019 +0000
@@ -137,17 +137,24 @@
show "generate G { a } \<subseteq> { a [^] (k :: int) | k. k \<in> UNIV }"
proof
fix h assume "h \<in> generate G { a }" hence "\<exists>k :: int. h = a [^] k"
- proof (induction, metis int_pow_0[of a], metis singletonD int_pow_1[OF assms])
+ proof (induction)
+ case one
+ then show ?case
+ using int_pow_0 [of G] by metis
+ next
+ case (incl h)
+ then show ?case
+ by (metis assms int_pow_1 singletonD)
+ next
case (inv h)
- hence "inv h = a [^] ((- 1) :: int)"
- using assms unfolding int_pow_def2 by simp
- thus ?case
- by blast
+ then show ?case
+ by (metis assms int_pow_1 int_pow_neg singletonD)
next
- case eng thus ?case
+ case (eng h1 h2)
+ then show ?case
using assms by (metis int_pow_mult)
qed
- thus "h \<in> { a [^] (k :: int) | k. k \<in> UNIV }"
+ then show "h \<in> { a [^] (k :: int) | k. k \<in> UNIV }"
by blast
qed
qed
@@ -436,4 +443,124 @@
assumes "K \<subseteq> carrier G" shows "(derived H ^^ n) (h ` K) = h ` ((derived G ^^ n) K)"
using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto)
+
+subsection \<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>"
+
+lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \<inter> S)"
+ by (auto simp: subgroup_generated_def)
+
+lemma (in group) group_subgroup_generated [simp]: "group (subgroup_generated G S)"
+ unfolding subgroup_generated_def
+ by (simp add: generate_is_subgroup subgroup_imp_group)
+
+lemma (in group) abelian_subgroup_generated:
+ assumes "comm_group G"
+ shows "comm_group (subgroup_generated G S)" (is "comm_group ?GS")
+proof (rule group.group_comm_groupI)
+ show "Group.group ?GS"
+ by simp
+next
+ fix x y
+ assume "x \<in> carrier ?GS" "y \<in> carrier ?GS"
+ with assms show "x \<otimes>\<^bsub>?GS\<^esub> y = y \<otimes>\<^bsub>?GS\<^esub> x"
+ apply (simp add: subgroup_generated_def)
+ by (meson Int_lower1 comm_groupE(4) generate_in_carrier)
+qed
+
+lemma (in group) subgroup_of_subgroup_generated:
+ assumes "H \<subseteq> B" "subgroup H G"
+ shows "subgroup H (subgroup_generated G B)"
+proof unfold_locales
+ fix x
+ assume "x \<in> H"
+ with assms show "inv\<^bsub>subgroup_generated G B\<^esub> x \<in> H"
+ unfolding subgroup_generated_def
+ by (metis IntI Int_commute Int_lower2 generate.incl generate_is_subgroup m_inv_consistent subgroup_def subsetCE)
+next
+ show "H \<subseteq> carrier (subgroup_generated G B)"
+ using assms apply (auto simp: carrier_subgroup_generated)
+ by (metis Int_iff generate.incl inf.orderE subgroup.mem_carrier)
+qed (use assms in \<open>auto simp: subgroup_generated_def subgroup_def\<close>)
+
+lemma carrier_subgroup_generated_alt:
+ assumes "Group.group G" "S \<subseteq> carrier G"
+ shows "carrier (subgroup_generated G S) = \<Inter>{H. subgroup H G \<and> carrier G \<inter> S \<subseteq> H}"
+ using assms by (auto simp: group.generate_minimal subgroup_generated_def)
+
+lemma one_subgroup_generated [simp]: "\<one>\<^bsub>subgroup_generated G S\<^esub> = \<one>\<^bsub>G\<^esub>"
+ by (auto simp: subgroup_generated_def)
+
+lemma mult_subgroup_generated [simp]: "mult (subgroup_generated G S) = mult G"
+ by (auto simp: subgroup_generated_def)
+
+lemma (in group) inv_subgroup_generated [simp]:
+ assumes "f \<in> carrier (subgroup_generated G S)"
+ shows "inv\<^bsub>subgroup_generated G S\<^esub> f = inv f"
+proof (rule group.inv_equality)
+ show "Group.group (subgroup_generated G S)"
+ by simp
+ have [simp]: "f \<in> carrier G"
+ by (metis Int_lower1 assms carrier_subgroup_generated generate_in_carrier)
+ show "inv f \<otimes>\<^bsub>subgroup_generated G S\<^esub> f = \<one>\<^bsub>subgroup_generated G S\<^esub>"
+ by (simp add: assms)
+ show "f \<in> carrier (subgroup_generated G S)"
+ using assms by (simp add: generate.incl subgroup_generated_def)
+ show "inv f \<in> carrier (subgroup_generated G S)"
+ using assms by (simp add: subgroup_generated_def generate_m_inv_closed)
+qed
+
+lemma subgroup_generated_restrict [simp]:
+ "subgroup_generated G (carrier G \<inter> S) = subgroup_generated G S"
+ by (simp add: subgroup_generated_def)
+
+lemma (in subgroup) carrier_subgroup_generated_subgroup [simp]:
+ "carrier (subgroup_generated G H) = H"
+ by (auto simp: generate.incl carrier_subgroup_generated elim: generate.induct)
+
+
+lemma (in group) subgroup_subgroup_generated_iff:
+ "subgroup H (subgroup_generated G B) \<longleftrightarrow> subgroup H G \<and> H \<subseteq> carrier(subgroup_generated G B)"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ then have Hsub: "H \<subseteq> generate G (carrier G \<inter> B)"
+ by (simp add: subgroup_def subgroup_generated_def)
+ then have H: "H \<subseteq> carrier G" "H \<subseteq> carrier(subgroup_generated G B)"
+ unfolding carrier_subgroup_generated
+ using generate_incl by blast+
+ with Hsub have "subgroup H G"
+ by (metis Int_commute Int_lower2 L carrier_subgroup_generated generate_consistent
+ generate_is_subgroup inf.orderE subgroup.carrier_subgroup_generated_subgroup subgroup_generated_def)
+ with H show ?rhs
+ by blast
+next
+ assume ?rhs
+ then show ?lhs
+ by (simp add: generate_is_subgroup subgroup_generated_def subgroup_incl)
+qed
+
+
+lemma pow_subgroup_generated:
+ "pow (subgroup_generated G S) = (pow G :: 'a \<Rightarrow> nat \<Rightarrow> 'a)"
+proof -
+ have "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n" for x and n::nat
+ by (induction n) auto
+ then show ?thesis
+ by force
+qed
+
+lemma (in group) int_pow_subgroup_generated:
+ fixes n::int
+ assumes "x \<in> carrier (subgroup_generated G S)"
+ shows "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n"
+proof -
+ have "x [^] nat (- n) \<in> carrier (subgroup_generated G S)"
+ by (metis assms group.is_monoid group_subgroup_generated monoid.nat_pow_closed pow_subgroup_generated)
+ then show ?thesis
+ by (simp add: int_pow_def2 pow_subgroup_generated)
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Algebra/Group.thy Mon Jan 28 18:36:50 2019 -0500
+++ b/src/HOL/Algebra/Group.thy Tue Jan 29 15:26:43 2019 +0000
@@ -30,24 +30,6 @@
\<comment> \<open>The set of invertible elements\<close>
where "Units G = {y. y \<in> carrier G \<and> (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
-consts
- pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a" (infixr "[^]\<index>" 75)
-
-overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
-begin
- definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
-end
-
-overloading int_pow == "pow :: [_, 'a, int] => 'a"
-begin
- definition "int_pow G a z =
- (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
- in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
-end
-
-lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
-by(simp add: int_pow_def nat_pow_def)
-
locale monoid =
fixes G (structure)
assumes m_closed [intro, simp]:
@@ -191,46 +173,6 @@
lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
by auto
-text \<open>Power\<close>
-
-lemma (in monoid) nat_pow_closed [intro, simp]:
- "x \<in> carrier G ==> x [^] (n::nat) \<in> carrier G"
- by (induct n) (simp_all add: nat_pow_def)
-
-lemma (in monoid) nat_pow_0 [simp]:
- "x [^] (0::nat) = \<one>"
- by (simp add: nat_pow_def)
-
-lemma (in monoid) nat_pow_Suc [simp]:
- "x [^] (Suc n) = x [^] n \<otimes> x"
- by (simp add: nat_pow_def)
-
-lemma (in monoid) nat_pow_one [simp]:
- "\<one> [^] (n::nat) = \<one>"
- by (induct n) simp_all
-
-lemma (in monoid) nat_pow_mult:
- "x \<in> carrier G ==> x [^] (n::nat) \<otimes> x [^] m = x [^] (n + m)"
- by (induct m) (simp_all add: m_assoc [THEN sym])
-
-lemma (in monoid) nat_pow_comm:
- "x \<in> carrier G \<Longrightarrow> (x [^] (n::nat)) \<otimes> (x [^] (m :: nat)) = (x [^] m) \<otimes> (x [^] n)"
- using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)
-
-lemma (in monoid) nat_pow_Suc2:
- "x \<in> carrier G \<Longrightarrow> x [^] (Suc n) = x \<otimes> (x [^] n)"
- using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
- by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)
-
-lemma (in monoid) nat_pow_pow:
- "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
- by (induct m) (simp, simp add: nat_pow_mult add.commute)
-
-lemma (in monoid) nat_pow_consistent:
- "x [^] (n :: nat) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
- unfolding nat_pow_def by simp
-
-
(* Jacobson defines submonoid here. *)
(* Jacobson defines the order of a monoid here. *)
@@ -340,6 +282,20 @@
subsection \<open>Cancellation Laws and Basic Properties\<close>
+lemma (in group) inv_eq_1_iff [simp]:
+ assumes "x \<in> carrier G" shows "inv\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> \<longleftrightarrow> x = \<one>\<^bsub>G\<^esub>"
+proof -
+ have "x = \<one>" if "inv x = \<one>"
+ proof -
+ have "inv x \<otimes> x = \<one>"
+ using assms l_inv by blast
+ then show "x = \<one>"
+ using that assms by simp
+ qed
+ then show ?thesis
+ by auto
+qed
+
lemma (in group) r_inv [simp]:
"x \<in> carrier G ==> x \<otimes> inv x = \<one>"
by simp
@@ -374,30 +330,114 @@
"[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
using inv_unique r_inv by blast
-(* Contributed by Joachim Breitner *)
lemma (in group) inv_solve_left:
"\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = inv b \<otimes> c \<longleftrightarrow> c = b \<otimes> a"
by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
+
+lemma (in group) inv_solve_left':
+ "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> inv b \<otimes> c = a \<longleftrightarrow> c = b \<otimes> a"
+ by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
+
lemma (in group) inv_solve_right:
"\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c"
by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
-text \<open>Power\<close>
+lemma (in group) inv_solve_right':
+ "\<lbrakk>a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> b \<otimes> inv c = a \<longleftrightarrow> b = a \<otimes> c"
+ by (auto simp: m_assoc)
+
+
+subsection \<open>Power\<close>
+
+consts
+ pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a" (infixr "[^]\<index>" 75)
+
+overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
+begin
+ definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
+end
+
+lemma (in monoid) nat_pow_closed [intro, simp]:
+ "x \<in> carrier G ==> x [^] (n::nat) \<in> carrier G"
+ by (induct n) (simp_all add: nat_pow_def)
+
+lemma (in monoid) nat_pow_0 [simp]:
+ "x [^] (0::nat) = \<one>"
+ by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_Suc [simp]:
+ "x [^] (Suc n) = x [^] n \<otimes> x"
+ by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_one [simp]:
+ "\<one> [^] (n::nat) = \<one>"
+ by (induct n) simp_all
+
+lemma (in monoid) nat_pow_mult:
+ "x \<in> carrier G ==> x [^] (n::nat) \<otimes> x [^] m = x [^] (n + m)"
+ by (induct m) (simp_all add: m_assoc [THEN sym])
+
+lemma (in monoid) nat_pow_comm:
+ "x \<in> carrier G \<Longrightarrow> (x [^] (n::nat)) \<otimes> (x [^] (m :: nat)) = (x [^] m) \<otimes> (x [^] n)"
+ using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)
+
+lemma (in monoid) nat_pow_Suc2:
+ "x \<in> carrier G \<Longrightarrow> x [^] (Suc n) = x \<otimes> (x [^] n)"
+ using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
+ by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)
-lemma (in group) int_pow_def2:
- "a [^] (z::int) = (if z < 0 then inv (a [^] (nat (-z))) else a [^] (nat z))"
- by (simp add: int_pow_def nat_pow_def Let_def)
+lemma (in monoid) nat_pow_pow:
+ "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
+ by (induct m) (simp, simp add: nat_pow_mult add.commute)
+
+lemma (in monoid) nat_pow_consistent:
+ "x [^] (n :: nat) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
+ unfolding nat_pow_def by simp
+
+lemma nat_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::nat) = \<one>\<^bsub>G\<^esub>"
+ by (simp add: nat_pow_def)
+
+lemma nat_pow_Suc [simp]: "x [^]\<^bsub>G\<^esub> (Suc n) = (x [^]\<^bsub>G\<^esub> n)\<otimes>\<^bsub>G\<^esub> x"
+ by (simp add: nat_pow_def)
-lemma (in group) int_pow_0 [simp]:
- "x [^] (0::int) = \<one>"
- by (simp add: int_pow_def2)
+lemma (in group) nat_pow_inv:
+ assumes "x \<in> carrier G" shows "(inv x) [^] (i :: nat) = inv (x [^] i)"
+proof (induction i)
+ case 0 thus ?case by simp
+next
+ case (Suc i)
+ have "(inv x) [^] Suc i = ((inv x) [^] i) \<otimes> inv x"
+ by simp
+ also have " ... = (inv (x [^] i)) \<otimes> inv x"
+ by (simp add: Suc.IH Suc.prems)
+ also have " ... = inv (x \<otimes> (x [^] i))"
+ by (simp add: assms inv_mult_group)
+ also have " ... = inv (x [^] (Suc i))"
+ using assms nat_pow_Suc2 by auto
+ finally show ?case .
+qed
+
+overloading int_pow == "pow :: [_, 'a, int] => 'a"
+begin
+ definition "int_pow G a z =
+ (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
+ in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
+end
+
+lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
+by(simp add: int_pow_def nat_pow_def)
+
+lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \<one>\<^bsub>G\<^esub>"
+ by (simp add: int_pow_def)
+
+lemma int_pow_def2: "a [^]\<^bsub>G\<^esub> z =
+ (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> (nat (-z))) else a [^]\<^bsub>G\<^esub> (nat z))"
+ by (simp add: int_pow_def nat_pow_def)
lemma (in group) int_pow_one [simp]:
"\<one> [^] (z::int) = \<one>"
by (simp add: int_pow_def2)
-(* The following are contributed by Joachim Breitner *)
-
lemma (in group) int_pow_closed [intro, simp]:
"x \<in> carrier G ==> x [^] (i::int) \<in> carrier G"
by (simp add: int_pow_def2)
@@ -418,23 +458,6 @@
by (auto simp add: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
qed
-lemma (in group) nat_pow_inv:
- assumes "x \<in> carrier G" shows "(inv x) [^] (i :: nat) = inv (x [^] i)"
-proof (induction i)
- case 0 thus ?case by simp
-next
- case (Suc i)
- have "(inv x) [^] Suc i = ((inv x) [^] i) \<otimes> inv x"
- by simp
- also have " ... = (inv (x [^] i)) \<otimes> inv x"
- by (simp add: Suc.IH Suc.prems)
- also have " ... = inv (x \<otimes> (x [^] i))"
- by (simp add: assms inv_mult_group)
- also have " ... = inv (x [^] (Suc i))"
- using assms nat_pow_Suc2 by auto
- finally show ?case .
-qed
-
lemma (in group) int_pow_inv:
"x \<in> carrier G \<Longrightarrow> (inv x) [^] (i :: int) = inv (x [^] i)"
by (simp add: nat_pow_inv int_pow_def2)
@@ -446,7 +469,7 @@
assume n_ge: "n \<ge> 0" thus ?thesis
proof (cases)
assume m_ge: "m \<ge> 0" thus ?thesis
- using n_ge nat_pow_pow[OF assms, of "nat n" "nat m"] int_pow_def2
+ using n_ge nat_pow_pow[OF assms, of "nat n" "nat m"] int_pow_def2 [where G=G]
by (simp add: mult_less_0_iff nat_mult_distrib)
next
assume m_lt: "\<not> m \<ge> 0"
@@ -592,7 +615,7 @@
assumes "subgroup H G" shows "H \<subseteq> Units (G \<lparr> carrier := H \<rparr>)"
using group.Units[OF subgroup.subgroup_is_group[OF assms group_axioms]] by simp
-lemma (in group) m_inv_consistent:
+lemma (in group) m_inv_consistent [simp]:
assumes "subgroup H G" "x \<in> H"
shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
@@ -603,16 +626,16 @@
proof (cases)
assume ge: "n \<ge> 0"
hence "x [^] n = x [^] (nat n)"
- using int_pow_def2 by auto
+ using int_pow_def2 [of G] by auto
also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat n)"
using nat_pow_consistent by simp
also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
- using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] ge by auto
+ by (metis ge int_nat_eq int_pow_int)
finally show ?thesis .
next
assume "\<not> n \<ge> 0" hence lt: "n < 0" by simp
hence "x [^] n = inv (x [^] (nat (- n)))"
- using int_pow_def2 by auto
+ using int_pow_def2 [of G] by auto
also have " ... = (inv x) [^] (nat (- n))"
by (metis assms nat_pow_inv subgroup.mem_carrier)
also have " ... = (inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x) [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n))"
@@ -620,7 +643,7 @@
also have " ... = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n)))"
using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
- using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] lt by auto
+ by (simp add: int_pow_def2 lt)
finally show ?thesis .
qed
@@ -781,6 +804,17 @@
{h. h \<in> carrier G \<rightarrow> carrier H \<and>
(\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
+lemma homI:
+ "\<lbrakk>\<And>x. x \<in> carrier G \<Longrightarrow> h x \<in> carrier H;
+ \<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y\<rbrakk> \<Longrightarrow> h \<in> hom G H"
+ by (auto simp: hom_def)
+
+lemma hom_carrier: "h \<in> hom G H \<Longrightarrow> h ` carrier G \<subseteq> carrier H"
+ by (auto simp: hom_def)
+
+lemma hom_in_carrier: "\<lbrakk>h \<in> hom G H; x \<in> carrier G\<rbrakk> \<Longrightarrow> h x \<in> carrier H"
+ by (auto simp: hom_def)
+
lemma hom_compose:
"\<lbrakk> f \<in> hom G H; g \<in> hom H I \<rbrakk> \<Longrightarrow> g \<circ> f \<in> hom G I"
unfolding hom_def by (auto simp add: Pi_iff)
@@ -793,20 +827,50 @@
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
by (fastforce simp add: hom_def compose_def)
-definition
- iso :: "_ => _ => ('a => 'b) set"
+definition iso :: "_ => _ => ('a => 'b) set"
where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
-definition
- is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
+definition is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
where "G \<cong> H = (iso G H \<noteq> {})"
+definition mon where "mon G H = {f \<in> hom G H. inj_on f (carrier G)}"
+
+definition epi where "epi G H = {f \<in> hom G H. f ` (carrier G) = carrier H}"
+
+lemma isoI:
+ "\<lbrakk>h \<in> hom G H; bij_betw h (carrier G) (carrier H)\<rbrakk> \<Longrightarrow> h \<in> iso G H"
+ by (auto simp: iso_def)
+
+lemma epi_iff_subset:
+ "f \<in> epi G G' \<longleftrightarrow> f \<in> hom G G' \<and> carrier G' \<subseteq> f ` carrier G"
+ by (auto simp: epi_def hom_def)
+
+lemma iso_iff_mon_epi: "f \<in> iso G H \<longleftrightarrow> f \<in> mon G H \<and> f \<in> epi G H"
+ by (auto simp: iso_def mon_def epi_def bij_betw_def)
+
lemma iso_set_refl: "(\<lambda>x. x) \<in> iso G G"
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+lemma id_iso: "id \<in> iso G G"
+ by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+
corollary iso_refl : "G \<cong> G"
using iso_set_refl unfolding is_iso_def by auto
+lemma trivial_hom:
+ "group H \<Longrightarrow> (\<lambda>x. one H) \<in> hom G H"
+ by (auto simp: hom_def Group.group_def)
+
+lemma (in group) hom_eq:
+ assumes "f \<in> hom G H" "\<And>x. x \<in> carrier G \<Longrightarrow> f' x = f x"
+ shows "f' \<in> hom G H"
+ using assms by (auto simp: hom_def)
+
+lemma (in group) iso_eq:
+ assumes "f \<in> iso G H" "\<And>x. x \<in> carrier G \<Longrightarrow> f' x = f x"
+ shows "f' \<in> iso G H"
+ using assms by (fastforce simp: iso_def inj_on_def bij_betw_def hom_eq image_iff)
+
lemma (in group) iso_set_sym:
assumes "h \<in> iso G H"
shows "inv_into (carrier G) h \<in> iso H G"
@@ -846,10 +910,8 @@
corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
using iso_set_trans unfolding is_iso_def by blast
-(* NEW ====================================================================== *)
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
-(* ========================================================================== *)
(* Next four lemmas contributed by Paulo. *)
@@ -1015,12 +1077,13 @@
shows "G \<times>\<times> H \<cong> G2 \<times>\<times> I"
using DirProd_iso_set_trans assms unfolding is_iso_def by blast
+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
\<^term>\<open>H\<close>, with a homomorphism \<^term>\<open>h\<close> between them\<close>
locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +
fixes h
- assumes homh: "h \<in> hom G H"
+ assumes homh [simp]: "h \<in> hom G H"
lemma (in group_hom) hom_mult [simp]:
"[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
@@ -1036,7 +1099,7 @@
with homh [unfolded hom_def] show ?thesis by auto
qed
-lemma (in group_hom) one_closed [simp]: "h \<one> \<in> carrier H"
+lemma (in group_hom) one_closed: "h \<one> \<in> carrier H"
by simp
lemma (in group_hom) hom_one [simp]: "h \<one> = \<one>\<^bsub>H\<^esub>"
@@ -1046,6 +1109,16 @@
then show ?thesis by (simp del: r_one)
qed
+lemma hom_one:
+ assumes "h \<in> hom G H" "group G" "group H"
+ shows "h (one G) = one H"
+ apply (rule group_hom.hom_one)
+ by (simp add: assms group_hom_axioms_def group_hom_def)
+
+lemma hom_mult:
+ "\<lbrakk>h \<in> hom G H; x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+ by (auto simp: hom_def)
+
lemma (in group_hom) inv_closed [simp]:
"x \<in> carrier G ==> h (inv x) \<in> carrier H"
by simp
@@ -1110,7 +1183,7 @@
lemma (in group_hom) int_pow_hom:
"x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
- using int_pow_def2 nat_pow_hom by (simp add: G.int_pow_def2)
+ using nat_pow_hom by (simp add: int_pow_def2)
subsection \<open>Commutative Structures\<close>
--- a/src/HOL/Algebra/Multiplicative_Group.thy Mon Jan 28 18:36:50 2019 -0500
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Tue Jan 29 15:26:43 2019 +0000
@@ -433,7 +433,7 @@
fix b assume "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
then obtain k :: nat where "b = a [^] k" by blast
hence "b = a [^] (int k)"
- using int_pow_def2 by auto
+ by (simp add: int_pow_int)
thus "b \<in> generate G { a }"
unfolding generate_pow[OF assms(2)] by blast
qed
@@ -447,12 +447,12 @@
proof (cases "k < 0")
assume "\<not> k < 0"
hence "b = a [^] (nat k)"
- using k int_pow_def2 by auto
+ by (simp add: int_pow_def2 k)
thus ?thesis by blast
next
assume "k < 0"
hence b: "b = inv (a [^] (nat (- k)))"
- using k int_pow_def2 by auto
+ using k int_pow_def2[of G] by auto
obtain m where m: "ord a * m \<ge> nat (- k)"
by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)